About VERACITY

VERACITY is a tool-supported iterative approach for the efficient and accurate verification of nonfunctional requirements under epistemic parameter uncertainty. It supports both the verification of new system designs, and the verification of planned updates to existing systems.

VERACITY integrates confidence-interval quantitative verification with a new adaptive uncertainty reduction heuristic that collects additional data about the parameters of the verified model by unit-testing specific system components over a series of verification iterations. VERACITY supports the quantitative verification of Markov chains, deciding the components to be tested at each iteration based on factors that include the sensitivity of the model to variations in the parameters of different components, and the overheads (e.g., time or cost) of unit-testing each of these components.

Each iteration (or round) of the VERACITY verification process comprises four steps:

  1. In the first step, formal verification with confidence intervals is used to compute confidence intervals [l1, u1], [l2, u2], . . . , [ln, un] at confidence level ∝ and closed-form expressions expr1, expr2, . . . , exprn for the n properties from the nonfunctional requirements. The observations O used to compute the n confidence intervals include the initial observations O0 and, starting with the second iteration, all the additional observations O' obtained in the previous iterations of the process. If the observation set O is empty, then the confidence interval [li, ui] computed for the i-th property in the first iteration is [0, 1] or [0, ∞), depending on whether the system property propi is a probability or a quantity such as cost or energy use.

  2. In the second step, VERACITY checks whether the n confidence intervals are sufficiently narrow to allow the verification of the nonfunctional requirements, and, if necessary, plans additional testing of the m system components.

  3. In the third step of the VERACITY process, nobsj tests of component j are carried out for j = 1, 2, ..., m. These tests can be fully automated, or can be performed by a software engineer when requested by the VERACITY verification tool. The result of this testing is a set of additional observations O'.

  4. Finally, in the fourth and last step of VERACITY, the new observations O' are integrated with all the observations obtained in the previous rounds of the process and the initial observations O0, and the combined set of all available observations O is used in the next round of the verification process.

Downloading VERACITY

VERACITY is freely available under the GNU General Public Licence and may be downloaded from the getting started page.

Contacting us

If you wish to contact the corresponding authors, then please use the following email addresses:

Radu Calinescu: radu.calinescu@york.ac.uk
Naif Alasmari: nnma500@york.ac.uk
Colin Paterson: colin.paterson@york.ac.uk