Difference between revisions of "Henshin State Space Tools"
|Line 215:||Line 215:|
=== Probabilistic model checking ===
=== Probabilistic model checking ===
Using PRISM, we can check CSL properties for state spaces generated by Henshin. You need to identify a set of target states for which you want to compute the probability for. We recommend to check out the very nice documentation in the [http://www.prismmodelchecker.org/manual/PropertySpecification/Introduction PRISM manual on property specification] for this. However, a standard state property supported by PRISM is "deadlock". You can compute the probability for eventually reaching a deadlock with:
Using PRISM, we can check CSL properties for state spaces generated by Henshin. You need to identify a set of target states for which you want to compute the probability for. We recommend to check out the very nice documentation in the [http://www.prismmodelchecker.org/manual/PropertySpecification/Introduction PRISM manual on property specification] for this. However, a standard state property supported by PRISM is "deadlock". You can compute the probability for eventually reaching a deadlock with :
P=? [ F "deadlock" ]
P=? [ F "deadlock" ]
Revision as of 08:55, 10 March 2011
To verify the correctness of transformations, Henshin provides a tool for generating and analyzing the state spaces of in-place model transformation. To some extent this can be compared to a debugger: starting from some initial state, the transformation is executed in a stepwise fashion and can be, thus, analyzed, e.g. to make sure that all intermediate states are correct fulfill some invariants. However, state space analysis is much more powerful than debugging, because instead of inspecting one particular execution path, the complete state space incuding all possible traces is generated. It goes without saying that the state space should be finite for this to work. However, abstraction techniques can be used to keep state spaces finite and small.
The state space tools in Henshin currently support the following features:
- Efficient (multi-threaded), resumable generation of explicit state spaces
- Various state-based abstractions:
- Graph vs. Ecore equality
- Optional node IDs
- Optional attributes
- Interactive state space visualization
- Extensible validation framework:
- Extensible export functionality:
- TikZ (*.tex)
- CADP (*.aut)
- PRISM (*.sm)
All these functionalities are integrated in Henshin's graphical state space explorer, shown on the right. However, they can be also invoked from the context menu for state space files or programmatically. For model checking, the state space explorer provides a uniform front-end to the above mentioned analysis tools.
State space generation
In this section, we explain how to generate a state space for a Henshin transformation.
Specifying the transformation
As a running example we consider the academic example of dining philosophers. To make it more interesting we include a rule for a dynamic reconfiguration, i.e. to allow to add a philosopher to the table during the execution. The rules can be specified using the either the graphical or tree-based transformation editor. The graphical versions of our rules are depicted below. We have the following rules:
- left and right for picking up forks (right is symmetric to left )
- release for putting them back on the table
- create for adding a new philosopher to the table (dynamic reconfiguration).
Adding philosophers without an upper limit would result in an infinite state space. Therefore, we include negative application conditions (NACs) in the rule create to make sure that we cannot add arbitrarily many philosophers. Here we chose an upper limit of at most 5 philosophers.
Creating an initial state model
To generate a state space from our transformation rules, we need to create an initial configuration for our dining philosopher system. We choose an initial configuration of 3 philosophers where all forks are lying on the table. We can define this either using a generated EMF editor for the philosophers model, or the sample reflective editor. Make sure though that the Ecore modeled is registered in the EMF package registry. In plain XMI, our initial state model looks like this:
<?xml version="1.0" encoding="UTF-8"?> <philosophers:Table xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:philosophers="http://www.eclipse.org/emf/2010/Henshin/Examples/Philosophers"> <plates left="//@forks.0" right="//@forks.1"/> <plates left="//@forks.1" right="//@forks.2"/> <plates left="//@forks.2" right="//@forks.0"/> <philosophers plate="//@plates.0"/> <philosophers plate="//@plates.1"/> <philosophers plate="//@plates.2"/> <forks/> <forks/> <forks/> </philosophers:Table>
Setting up the state space
Now we set up our state space file. Open the New... wizard and select Henshin State space in the Henshin category. After finishing the wizard a new file with the extension statespace is created and opened in the graphical state space explorer.
On the right-hand side you can find control panel for the explorer. On the top, the number of states, transitions and rules is displayed. Here you can also find some switches which influence the state space generation. These switches control the type of equality used in the state space generation and can, thus, used as abstractions:
- Ecore vs. Graph Equality: Whether to use the normal Ecore equality (defined in EcoreUtil.equals()) or graph isomorphism checking. The difference is that the order of multi-valued references is ignored in the graph equality. By default, this is set to graph equality and this is also the right choice for 95% percent of the cases. Using the graph equality the state space gets significantly smaller and yet is fully equivalent to the original one based on Ecore equality.
- Option node IDs: Whether to use node IDs or not. If this option is checked, every node created during a transformation gets an ID which is unique for the lifetime of this node. This option must be checked when using parameterized actions.
- Option attribute values: Whether to consider attribute values when comparing two state models. This makes sense in most cases.
Note that these options can be also changed later. However, the state space needs to be generated again.
Now, from the Tasks menu in the control panel, you need to do the following things:
- Import transformation rules to be used in the state space generation.
- Load one or more initial state models into the state space.
In our dining philosophers example, we import the rules left, right, release and create. As initial state, we load the file from above.
Building up the state space
The initial state appears as a green node in the state space explorer. You can click on Start layouter in the Tasks menu on the right-hand side of the explorer to enable automatic layouting. By double clicking on a state, you can unfold this state and thereby, manually explore the state space. States are depicted using different colors:
- Green: initial states
- Grey: explored states
- Blue: open states (can be explored by double clicking on them)
- Red: deadlock or terminal states (no rules are applicable here)
You can also let the tool do the work for you by clicking on Start explorer to automatically build up the state space. This can be combined with the automatic layouter.
After a number of steps, the state space for the philosophers example is fully generated. It should look more or less like in the screenshot on the right. Here we used graph equality without extra options.
Offline state space generation
State space can be also generated outside of the graphical explorer, which is, of course, much more efficient. The offline state space generation can be invoked by clicking on Explore State Space in the State Space submenu in the context menu of state space files. On multi-core machines, a multi-threade state space exploration scheme is used, which can increase the performance by a factor, depending on the number of cores and the available memory. Note that the speed is a tradeoff between memory consumption and used time.
You can also click on Properties in the context menu of state space files to see its details. Note that statespace files have a binary format and can get large, depending on the size of the state space. The generator is currently able to handle state spaces with millions of states and tens of millions of transitions. You can open such big files also in the graphical explorer, but they will not be visualized anymore.
Resetting the state space
Another often used functionality is to reset a state space. This removes all derived state space (all states which are not initial). You can do this also from the context menu of state space files, or in the Tasks menu in the graphical explorer.
In the basic version, transitions are labeled just with rule names, e.g. left and right in our simple example. A more powerful approach is also supported, which allow to parameterize the transition labels with identifiers of nodes.
For this purposes, you have to specify a list of rule nodes that should be the parameters the corresponding action in transitions. These nodes can be preserved, added or removed by the rule. We need to know which nodes shall be used. Therefore, you need to give them unique names in the rule. Next, we have to tell the state space generator which of the nodes in the rule should be used and in which order they should appear as parameters in transitions. For this, edit the properties of the state space and edit (or create) the properties paramsRule where Rule is the name of the parameterized rule. Specify a comma separated list of node names in the rule. An example for the dining philosophers is shown on the right.
Last but not least: enable the option node IDs and reset the state space. When you now regenerate the state space, you will see the parameters on the transition labels. These parameterized actions can be also very useful for model checking later (see the paragraph on model checking with parametrized actions).
State space validation
To validate a state space open it in the graphical explorer and make sure it is fully explored (it has no open states). Then you can use the Validation menu in the control panel to validate it.
You can specify OCL constraints in the validation tool in the explorer and check them for your state space. For example in the dining philosophers state space we can check the following constraint:
self.forks->size() > 0
meaning that there is always at least one fork on the table. After having selected OCL (invariant) in the drop down menu, we can simply click on Run to check the constraint. In out case this should give us a negative result. Moreover, a trace into a state which does not fullfil the constraint is automatically selected in the explorer. This gives you essentially a counterexample for your invariant.
Single root container
Similarly to the OCL invariant checker, the validation tool Single root can be used to check a structural invariant of state models. This tool checks whether all state models have a single root container object. Henshin collects objects created during the transformation which are not directly or transitively contained in a root object. Using the Single root validation tool, it can be checked whether for all states, all objects are properly contained a single root container object. This essentially ensures that there are no dangling references in your model.
Qualitative model checking with CADP and mCRL2
Full model checking of temporal properties is supported using external model checkers. For qualitative model checking you can currently use either CADP or mCRL2. To use the tools in Henshin you have to install it somewhere on your computer. Note that CADP requires an (academic) license, whereas mCRL2 is open source.
When you have installed either of the tools, make sure they are in the system-wide PATH, so that Henshin can find them. For CADP you also have to define the environment variable CADP, which should point to the directory where it is installed.
Now you can model check your state space. Both mCRL2 and CADP support the model mu-calculus which has a great raw expressive power, but is also hard to read/write. As an example, freedom of deadlock can be verified using the formula:
In our example, this should evaluate to false. CADP moreover generates a counterexample, which is shown in the explorer (here it is a trace into one of the deadlock states). Another property that we can check is the following:
which basically says: Is there an infinite sequence of the actions left and right? This should evaluate to false. However, if we try:
we get true. Note that in CADP you have to put quotes around the action names.
Model checking with parametrized actions
State space with parameterized actions can be also analyzed. Currently, mCRL2 can be used for this. The type of the actions is induced by the parameter definitions for rules. In the following, we use the example with parameterized actions from above. We can use the parameterized actions in the model checking. For instance, consider the following formula:
[true*](forall f1,f2:Fork . exists p:Philosopher . ( [left(p,f1).right(p,f2)] (nu X. mu Y. ([release(p,f1,f2)]X && [!release(p,f1,f2)]Y))) )
It states: for all forks f1,f2 there exists a philosopher, such that first left(p,f1) followed by right(p,f2) and then eventually release(p,f1,f2). This property is satisfied in our example.
Probabilistic model checking with PRISM
For a stochastic analysis of your transformation you can use the PRISM model checker. Based on some user-defined rates for the transformation rules, Henshin generates a so-called continuous-time Markov chain in the input format of PRISM.
A standard task in PRISM is to compute so-called steady-state probabilities for a state space. In essence, this analysis yields probabilities for your system being in a certain state.
To compute steady-state probabilities in the Henshin explorer choose the tool PRISM (steady-states). Before running this tool, you should specify application rates for all rules first. This can be done by editing the properties of the state space. For a rule called myRule, its rate is specified using the property with the key rateMyRule. Rates must be specified as integers or doubles. The screenshot on the left shows some example rates. Note that you can also specify the location of PRISM and optional parameters using the properties prismPath and prismParams (if something goes wrong). Now you can generate the steady-state probabilities, as shown in the screenshot on the right.
Probabilistic model checking
Using PRISM, we can check CSL properties for state spaces generated by Henshin. You need to identify a set of target states for which you want to compute the probability for. We recommend to check out the very nice documentation in the PRISM manual on property specification for this. However, a standard state property supported by PRISM is "deadlock". You can compute the probability for eventually reaching a deadlock with the following formula (this will actually produce either 0 or 1):
P=? [ F "deadlock" ]
To compute the probability for ending up in some specific states, e.g. in state 13 or 17, you can use this:
label "target" = s=13 | s=17; P=? [ F "target" ]
You can also use OCL to specify the target states, e.g.:
label "target" = <<<OCL self.philosophers->size() > 4 and self.philosophers->size() = self.forks->size() >>> P=? [ F "target" ]
Plots generated from experiments
PRISM supports a so-called experiments which are essentially a sequence of model checking runs in which one parameter is changed. Based on this approach it is possible to generate plots that show how a numerical property changes if another one is changed. This feature is also supported by the PRISM adapter in Henshin's state space tools.
The only thing that you have to do is to replace some of the concrete rates for the rules by intervals. For instance, specifying the property rateLeft as 10:10:250 means that PRISM will compute the result for values 10, 20, 30, ..., 250 for rateLeft. You can do this with multiple parameters. In that case, you should specify which parameter is used for the X-axis. For instance, to vary the parameter rateLeft you need to set the following state space property: prismExperiment=rateLeft.
The Henshin tool will invoke PRISM with the correct parameters, parse the output and generate a plot such as the one in the screenshot on the right.