Getting Started
Prerequisites
VERACITY has been tested on Mac OS and requires the following prerequisites to be installed:Matlab: Matlab is commerical application available from the Mathworks website. VERACITY has been tested with Version R2019a.
YALMIP: Yalmip is a free toolbox for MATLAB and is available from the authors website. VERACITY has been tested with release 20150918.
*Please note the YALMIP must be added to the Matlab path in order for VERACITY to work as anticipated.
PRISM PRISM is a Probabilistic Model Checkeravailable from the product website. VERACITY was tested with verion 4.4
* After installing PRISM on your own computer, please make a note of the bin directory (e.g., /Users/UserName/Applications/prism-4.4/bin).
Gurobi Optimizer Although optional we have found that the performance of VERACITY was improved with the Gurobi optimizer installed. At the time of writing Gurobi offer a free academic licence for the software. Gurobi optimizer is available from their website.
Installing VERACITY
Having downloaded the VERACITY zip file uncompress the file to a new directory on your computer. The new directory will now contain the following files and folders:
- Configuration.txt
- CaseStudies Folder
- Logs folder
- VERACITY.jar
The configuration file should be updated to include the PRISM bin folder location before VERACITY is executed. Parameters may also be amended in this file to adjust the whole budget, round budget, and analysis method (uniform or adaptive) required for verification.
Additionally an optional component testing script may be defined and its location recorded in the configuration file. Details concerning the construction of a testing script are provided in our research paper.
It contains the files related to Case Studies introduced in our paper with their experimental results.
When VERACITY is executed, log files are stored in this directory. Each log file contains the evaluated property, the confidence level chosen for the test, and the codes sent to Matlab. Although the log folder may be emptied, it should not be deleted as doing so will cause VERACITY to fail.
After the configuration file is saved, we can run our tool by using this jar file in the following syntax:
java -jar VERACITY.jar <model_Name.pm> <props.pctl>
<Confidence level (e.g., 90)>
Running VERACITY for the first time
The first step in running the VERACITY software is to download the VERACITY zip file. Next extract the contents to a local directory and edit the configuration for the desired experiment.
For all experiments you must point VERACITY to your local copy of the prism binary. Next set the testingBudget, testingRoundBudget and useUniform parameter. Below we show a configuration file for the TAS example using non-uniform testing, a round budget of 5,000 and a total testing budget of 700,000.
- PRISMLocation,/Applications/prism-4.6-osx64/bin/prism
- hillClimbingMax,0
- NewObservationScriptLocation,
- testingBudget,700000
- testingRoundBudget,5000
- useUniform,false
- skipSatisfiedReqs,true
Having edited the configuration file we now execute VERACITY using the command:
java -jar VERACITY.jar ./CaseStudies/TAS/TAS.pm ./CaseStudies/TAS/TAS.pctl 95
Where parameter 1 is the model to be evaluated, parameter 2 is the properties file and parameter 3 is the confidence level at which we wish to evaluate the model.
As the program executes it will return the results of the parameteric model checking. Since, in this case, we are not using an observation script, the program will ask us to enter the observations for each component as follows:
- ...
- ** Additional observations are required
- -- Additional observations required for component 1: 833
- -- Additional observations required for component 2: 1666
- -- Additional observations required for component 3: 1666
- >> Provide 833 additional observations for pAlarm (2 transitions) :
Since there are 2 transitions for pAlarm we must enter the number of observations for each transition, totalling 833, as a list with spaces as seperators. We will then be asked for each of the other components as follows:
- ...
- >> Provide 833 additional observations for pAlarm (2 transitions) : 795 38
- -- param pAlarm : observations = 796 39 ; component = 1 ; cost = 2.0 ;
- >> Provide 1666 additional observations for pPharmacy (2 transitions) : 1581 85
- -- param pPharmacy : observations = 1582 86 ; component = 2 ; cost = 1.0 ;
- >> Provide 1666 additional observations for pAnalysis (2 transitions) : 1651 15
- -- param pAnalysis : observations = 1652 16 ; component = 3 ; cost = 1.0 ;
Here we see that once the number of observations have been entered the current running total of observations will be reported. Once all observations have been provided VERACITY will continue to the next round of evaluation.