Model Formal Analysis using Model Checking

Introduction

pmodelchecker is an application that facilitates the use of formal model analysis using Model Checking of spatio-temporal properties of P system models developed within the Infobiotics workbench. pmodelchecker receives as input a model developed as specified in section and a list of temporal logic formulas formalising some spatio-temporal properties to be checked against the dynamics of the model.

pmodelchecker uses two different stochastic model checkers, PRISM and MC2. When using PRISM it generates a model in the reactive modules language needed in PRISM in order to check the input logic formulas. When using MC2 it generates the needed simulation samples by running mcss, the multicomparmental simulator introduced in the previous section.

Installlation

For instructions on how to compile and install pmodelchecker, see the README file included with the pmodelchecker distribution.

Running pmodelchecker

In order to run pmodelchecker after its installation run the following command:

$ pmodelchecker PARAMETER_FILE

where PARAMETER_FILE is an xml file declaring the input parameters required to perform model checking using one of the two stochastic model checkers integrated in Infobiotics, PRISM or MC2. For example, in order to run the examples in the directory PRISMexamples/ browse to this directory provided in the directory examples/ of the pmodelchecker distribution and type one of the commands below depending on which example you want to run:

$ pmodelchecker NAR1.params

$ pmodelchecker NAR2.params

In a similar manner to run the examples for MC2 browse to the directory MC2examples/ inside the directory examples/ provided in the pmodelchecker distribution and type the command below:

$ pmodelchecker NAR_MC2.params

The output, probabilities or expected values for temporal logic formulas, is produced into the result file specified as in the parameter file as explained below.

pmodelchecker parameter files

The pmodelchecker parameter file provides information to determine which specific model checker to use, PRISM or MC2, and some parameters to control the application of these model checkers like the use of verification versus approximation or the number of samples to consider in the case of a simulative or approximative approach.

The parameter file is in an XML format which has the general form:

<parameters>
  <parameterSet name="SimulationParameters">
    <parameter name="PARAMETER NAME" value="PARAMETER VALUE"/>
    <parameter name="PARAMETER NAME" value="PARAMETER VALUE"/>
    ...
  </parameterSet>
</parameters>

The specific parameters are given in the table below:

PARAMETER NAME	DESCRIPTION	VALUE	RESTRICTIONS
model_specification	Name of the file containing the model specification as an LPP-system	String	None
temporal_formulas	Name of the file containing the temporal logic formulas formalising the properties to check	String	None
model-checker	Name of the model checker to use PRISM or MC2	String	None
PRISM_model	Name of the file where to output the translation of our model into the PRISM language	String	Only when using PRISM
task	Task to perform when using PRISM as model checker. Translate LPP-system into the PRISM languge, build the corresponding Markov chain, verify or approximate the input properties	Translate/ Build/ Verify/ Approximate	Only when using PRISM
model_parameters	A string stating the values of the parameters in the model as follows param=lb:ub:s,param=lb:ub:s, ... where lb is the lowe bound, up is the upper bound and s is the step	String	Only when using PRISM
formula_parameters	A string stating the values of the parameters in the formulas as follows param=lb:ub:s,param=lb:ub:s, ... where lb is the lowe bound, up is the upper bound and s is the step	String	Only when using PRISM
states_file	Name of the file where to output the states of the Markov chain generated from the LPP-system	String	Only when using PRISM with task Build or Verify
transitions_file	Name of the file where to output the transitions of the Markov chain generated from the LPP-system	String	Only when using PRISM with task Build or Verify
number_samples	Number of simulations to generate when taking an approximate or simulative approach to model checking	Integer	Only when using PRISM with task Approximate or whenever using MC2
precision	Precision to achieve whith respect to real value when generating an estimate using approximate or simulative model checking	Double	Only when using PRISM with task Approximate
confidence	Confidence to achieve whith respect to real value when generating an estimate using approximate or simulative model checking	Double	Only when using PRISM with task Approximate
pathMC2	Location of the executable file for MC2	String	Only when using MC2
simulations_generatedHDF5	Flag to determine if the simulations needed to run MC2 are available in HDF5 format	true/false	Only when using MC2
simulations_generatedMC2	Flag to determine if the simulations needed to run MC2 are available in MC2 format	true/false	Only when using MC2
simulations_file_hdf5	Name of the file containing the simulations in HDF5 format or where to write them when using mcss	String	Only when using MC2 and the flag simulations_generatedMC2 = false
simulations_file_MC2	Name of the file containing the simulations in MC2 format or where to write them	String	Only when using MC2
mcss_params_file	Name of the file containing the parameters to run mcss in order to generate the necessary simulations	String	Only when using MC2 and the flag simulations_generatedHDF5 = false and simulations_generatedMC=false
results_file	Name of the file where to write the answers to the temporal logic formulas generated by the model checker	String	None

License

The pmodelchecker distribution, including all source code, model examples, and documentation, are the copyright of of the Infobiotics Team (Hongqing Cao, Claudio Lima, Natalio Krasnogor, Francisco Romero-Campero, Jamie Twycross, and Jonathan Blakes) and is released under the GNU GPL version 3 license.

Credits

pmodelchecker was written by Francisco J. Romero-Campero and is being used on Systems/Synthetic Biology research projects in the University of Nottingham, U.K.

For further information or any questions please contact fxc AT cs.nott.ac.uk.

copyright 2009 Infobiotics Team, released under GNU GPL version 3.