Difference between revisions of "ADVANCE D3.3 Model Checking"

From Event-B
Jump to navigationJump to search
imported>Daniel
imported>Daniel
Line 27: Line 27:
 
To allow a translation from ProB to Kodkod, we implemented an integer interval analysis. We plan to adapt the analysis to set up sizes of deferred sets. This is necessary because ProB chooses a fixed size for a deferred set and sometimes a model has only solutions for a certain size. Currently a user must supply a size manually.''
 
To allow a translation from ProB to Kodkod, we implemented an integer interval analysis. We plan to adapt the analysis to set up sizes of deferred sets. This is necessary because ProB chooses a fixed size for a deferred set and sometimes a model has only solutions for a certain size. Currently a user must supply a size manually.''
  
'''Theory Plugin support'''
+
'''Theory Plug-in support'''
We adapted ProB to the changes that had been made to the Theory Plugin in preperation of the upcoming release. We implemented support for the theory of transitive closures.
+
We adapted ProB to the changes that had been made to the Theory Plug-in in preperation of the upcoming release. We implemented support for the theory of transitive closures.
 
From the current set of standard theories, ProB supports animation of models that use operators of the theories "BoolOps", "FixPoint", "Seq", "SUMandPRODUCT" and "closure".
 
From the current set of standard theories, ProB supports animation of models that use operators of the theories "BoolOps", "FixPoint", "Seq", "SUMandPRODUCT" and "closure".
 
The support is included in the current development version of ProB.
 
The support is included in the current development version of ProB.
Still unsupported are the operators of the standard theories "BinaryTree" and "List" which use recursively defined operators. We plan to implement support for them for the next release.
+
Still unsupported are the operators of the remaining standard theories "BinaryTree" and "List" which use recursively defined operators. We plan to implement support for them for the next release.
  
 
{{TODO}}'''  LTL Fairness'''  
 
{{TODO}}'''  LTL Fairness'''  

Revision as of 04:13, 23 August 2013

Overview

TODO We think that animation and model checking are important tools when building a model. Animation allows the user to validate if the model corresponds to the user's intentions. Model checking allows to check if the model contains errors and provides counter-examples that help to understand the problem beforehand. Moreover, it allows to reason with domains (like physical units) and verify some properties (like temporal logic ones), that have currently no matching proof support. The following activities were pursued within the project:

  • The constraint solving capabilities of ProB have been continuously improved along with scalability improvements.
  • Previously we implemented a TLA to B compiler to use ProB on TLA+ specifications. We now also support the direction from B to TLA+. This allows to use the TCL model checker on B specifications.
  • There is work in progress towards support of the upcoming 2.0 version of the Theory plug-in.
  • We are working on a secondary independent toolchain for animation.
  • We finalized and released the of physical units plug-in.

Motivations / Decisions

TODO Secondary toolchain

B to TLA+

We developed a transcompiler from B to TLA+ (Temporal Logic of Actions) to verify B specifications with TLC. TLC is an explicit state model checker for TLA+ with an efficient disk-based algorithm and support for temporal formulas and fairness.Our translator is full automatic and supports a large subset of B. Moreover it uses static analyses to verify the correctness of the B specification (e.g. type checking and scope checking) and creates an optimized translation for the validation with TLC. Error traces (e.g. leading to deadlocks or invariant violations) detected by TLC are translated back to B and can be verified by ProB.

TODO Kodkod Currently the translation to Kodkod is only applied to axioms when trying to find values for the constants and during the constraint based deadlock check. We plan to restructure ProB's internal programming interfaces in a way that allows to apply Kodkod more easily and make it available for other checks (e.g. constraint-based invariant check, assertion checks). We will evaluate how we can employ more SMT based techniques in ProB.

TODO Constraint Solver Improvements During the further development of ProB's constraint solving it became apparent that it would be helpful to represent the cardinality of a set by a CLP(FD) variable. We plan to change ProB's internal representation of sets in a way that its cardinality can be accessed in this way. To allow a translation from ProB to Kodkod, we implemented an integer interval analysis. We plan to adapt the analysis to set up sizes of deferred sets. This is necessary because ProB chooses a fixed size for a deferred set and sometimes a model has only solutions for a certain size. Currently a user must supply a size manually.

Theory Plug-in support We adapted ProB to the changes that had been made to the Theory Plug-in in preperation of the upcoming release. We implemented support for the theory of transitive closures. From the current set of standard theories, ProB supports animation of models that use operators of the theories "BoolOps", "FixPoint", "Seq", "SUMandPRODUCT" and "closure". The support is included in the current development version of ProB. Still unsupported are the operators of the remaining standard theories "BinaryTree" and "List" which use recursively defined operators. We plan to implement support for them for the next release.

TODO LTL Fairness Fairness properties are very common when specifying LTL formula. Fairness can be encoded by using standard LTL, but it makes the formula significantly larger. The complexity of the model checking algorithm grows exponentially with the number of used LTL operators in a formula. We plan to incorporate support for fairness directly into the model checker which should lead to a drastic improvement in performance when fairness is used. Additionally, the usability of the model checker is improved by having the ability to specify fairness conditions seperatly from the rest of the LTL formula.

It is already possible to use fairness by using the B to TLA translator and run TLC.

Physical Units

The work on physical unit support has been completed and is available as an optional plug-in available from the ProB update site.

TODO BMotion Studio We will provide a way to link up other Java-based simulation tools with BMotion Studio. Furthermore, beside working on identified bugs and and rectifying usability issues, we want to create more visual elements to aid humans understand large-scale simulations.

Available Documentation

Planning

TODO

References