Verification

Infobiotics Workbench features verification capabilities for the models specified in Infobiotics Language, by using model checking techniques. Infobiotics Workbench integrates the Prism, MC2, NuSMV model checkers.

1. The different verification features can be accessed by activating the IBW Verification perspective.

2. Once the verification perspective is activated, a dedicated Verification view will appear and will be docked in the right side of the workbench.

3. The Verification view allows the configuration of various parameters and allows for the verification to be either triggered or the underlying generated files to be exported:

   • The location of underlying files generated in the verification process (translations from the IBL model to the actual model checking targets, verification results etc.);

   

   • Selecting between Quantitative and Qualitative analysis methods will automatically filter the actual set of suitable model checkers and the set of properties to be selected for verification;

   

   • By chosing to perform a qualitative analysis, the Prism, MC2 and NuSMV are displayed as suitable model checker options;

   

   • Selecting Prism for qualitative analysis requries the input of various configuration parameters, i.e. the confidence value, the path length and the number of samples to be generated. Moreover, the set of available properties to be selected for verification is filtered, according to their sutability to the current set of options;

   

   • Selecting MC2 for qualitative analysis requries the input of various configuration parameters, i.e. the max time, the interval and the number of runs and the actual Gillespie SSA to be used for generating the underlying simulation traces. Moreover, the set of available properties to be selected for verification is filtered, according to their sutability to the current set of options;

   

   • Selecting NuSMV for qualitative analysis requries no specific configuration parameters. However, the set of available properties to be selected for verification is filtered, according to their sutability to the current set of options;

   

   • By chosing to perform a quantitative analysis, the Prism and MC2 are displayed as suitable model checker options;

   

   • Selecting Prism for quantitative analysis requries the input of various configuration parameters, i.e. the confidence value, the path length and the number of samples to be generated. Moreover, the set of available properties to be selected for verification is filtered, according to their sutability to the current set of options;

   

   • Selecting MC2 for quantitative analysis requries the input of various configuration parameters, i.e. the max time, the interval and the number of runs and the actual Gillespie SSA to be used for generating the underlying simulation traces. Moreover, the set of available properties to be selected for verification is filtered, according to their sutability to the current set of options;

   

   • After performing the configuration using the above-described parameters, one or more properties can be selected for verification. triggering the verification can be done by clicking on the Verify button;

   

4. After the verification has been triggered and completed, the verification results are displayed in the Console view, docked at the bottom side of the workbench.