ADVANCE D3.3 Model Checking: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older edit
imported>Jens
imported>Jens
 
(51 intermediate revisions by 5 users not shown)
Line 1: Line 1:
= Overview =
== Overview ==
{{TODO}}
Experience with industrial case studies, such as those of WP1 and WP2, have demonstrated 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<sup>+</sup> specifications. We now also support the direction from B to TLA<sup>+</sup>. 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 =
Outside ADVANCE we improved the model checker by adding support for distributed model checking, partial order reduction and partial guard evaluation. We think that these improvements are also valuable within the ADVANCE project.
'''Distributed Model Checking '''


We have developed a version of ProB that is able to verify invariants and assertions and check for deadlocks in parallel on a multicore processor. The restrictions of the execution environment( i.e., Sicstus Prolog does not support multithreading) led to a distributed version of ProB where multiple instances of ProB are spawned and coordinated via sockets. Initial experiments indicate that the approach scales very well if the model is suited for parallel model checking, i.e., it is non-deterministic. The additional overhead of our implementation is at least an order of magnitude lower than the runtime of the model checker. Even if the model is not suited at all, the effect of running the parallel version can be neglected.
== Motivations / Decisions ==


'''Second toolchain'''


'''Partial Order Reduction '''  
'''Secondary toolchain'''


'''B to TLA'''
Independently of ProB we completed the development of a tool, which is able read solutions (constant and variable-values) generated by ProB and evaluate predicates like the properties or the invariant of a B model. Also it is possible to evaluate expression in an interactive mode or animate B machines. The tool is (with the exception of the parser) a complete new implementation of a predicate/expression B-evaluator and animator in python. The goal of the reimplementation is to establish a second independent toolchain to crosscheck results of ProB. The python tool has been successfully tested with industrial B Models from the railway domain. The tool is available from [https://github.com/hhu-stups/pyB http://github.com/hhu-stups/pyB]


''' Kodkod'''
'''B to TLA<sup>+</sup>'''
''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.''


'''  Constraint Solver Improvements '''
We developed a transcompiler from B to TLA<sup>+</sup> (Temporal Logic of Actions) to verify B specifications with TLC. TLC is an explicit state model checker for TLA<sup>+</sup> 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.
''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.
Moreover it uses static analyses to verify the validity of the B specification (e.g. type checking and scope checking) and creates an optimized translation for the validation with TLC.
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.''
Error traces (e.g. leading to deadlocks or invariant violations) detected by TLC are translated back to B and can be verified by ProB.


'''Theory Plugin support'''
''' Kodkod'''


Kodkod is a Java library that provides an interface to SAT solvers for solving relational problems. In <ref name="Kodkod-FM2012">http://www.stups.uni-duesseldorf.de/w/Special:Publication/PlaggeLeuschel_Kodkod2012</ref> we described a translation from B/Event-B to Kodkod where we applied the translation to improve
finding values for the constants of a model and ProB's constraint based deadlock check.
We have now applied the technique to check theories of a context in Event-B, check assertions in classical B and to the constraint-based invariant check.
It became apparent that reducing the model to a relevant set of variables and predicates can improve the applicability of the method because
often only a part of a model can be translated to Kodkod.
We have implemented such a ''slicing'' of the model and plan to validate if this leads to a performance improvement when we use only ProB's constraint solver without Kodkod.
'''Theory Plug-in support'''
We adapted ProB to the changes that had been made to the Theory Plug-in in preparation of the upcoming release.
ProB had support for recursive data types and operators that were defined by direct definitions. Also the SUM and PRODUCT operators were explicitly supported.
Additionally we implemented now 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".
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.


'''  LTL Fairness'''  
'''  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.''
 
We currently explore ways to implement Fairness into ProB's LTL model checker. However, it is already possible to use fairness by using the B to TLA translator and running TLC.


''' Physical Units'''  
''' Physical Units'''  
''Physical units work will be completed. First experiments with industrial models from Alstom are encouraging.''


''' BMotion Studio '''  
The work on physical unit support has been completed and is available as an optional plug-in available from the ProB update site.
''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 ==
 
'''ProB'''<br>
The ProB Website<ref>http://www.stups.uni-duesseldorf.de/ProB</ref> is the place where we collect information on the ProB toolset. There are several tutorials on ProB available in the User manual section. We also supply documentation on extending ProB for developers.
 
In addition we run a bug tracking system<ref>http://jira.cobra.cs.uni-duesseldorf.de/</ref> to document known bugs, workarounds and feature requests.
 
'''BMotion Studio'''<br>
A developer-, user documentation, tutorial and examples are available from a dedicated webpage<ref>http://www.stups.uni-duesseldorf.de/bmotionstudio</ref> hosted by the University of Duesseldorf.


= Available Documentation =
== Planning ==
'''Distributed Model Checking'''


An extended abstract has been published at the Rodin User and Developer Workshop 2013<ref>http://tucs.fi/publications/view/?pub_id=pBuHaWa13a</ref>.


= Planning =
* We will continue to work on the translation of B to TLA+ in order to use the TLC model checker. The translation needs to be validated and more of the full classical B language needs to be covered. We will also strive to make TLC available within Rodin for Event-B specifications.
{{TODO}}
* We will also continue to try to add fairness constraints efficiently both to ProB's own model checker and via the translation to TLC.
* We will continue our work on porting BMotionStudio to HTML. We want to define an open architecture that allows re-using BMotionStudio outside of ProB.
* We will further improve support for theories with recursive functions and try to make recursive functions more efficient.
* We will continue evaluating and improving our SAT backend via Kodkod and also evaluate the possibility of using SMT backends.


= References =
== References ==
<references/>
<references/>


[[Category:ADVANCE D3.3 Deliverable]]
[[Category:ADVANCE D3.3 Deliverable]]

Latest revision as of 10:41, 23 September 2013

Overview

Experience with industrial case studies, such as those of WP1 and WP2, have demonstrated 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.

Outside ADVANCE we improved the model checker by adding support for distributed model checking, partial order reduction and partial guard evaluation. We think that these improvements are also valuable within the ADVANCE project.

Motivations / Decisions

Secondary toolchain

Independently of ProB we completed the development of a tool, which is able read solutions (constant and variable-values) generated by ProB and evaluate predicates like the properties or the invariant of a B model. Also it is possible to evaluate expression in an interactive mode or animate B machines. The tool is (with the exception of the parser) a complete new implementation of a predicate/expression B-evaluator and animator in python. The goal of the reimplementation is to establish a second independent toolchain to crosscheck results of ProB. The python tool has been successfully tested with industrial B Models from the railway domain. The tool is available from http://github.com/hhu-stups/pyB

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 validity 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.

Kodkod

Kodkod is a Java library that provides an interface to SAT solvers for solving relational problems. In [1] we described a translation from B/Event-B to Kodkod where we applied the translation to improve finding values for the constants of a model and ProB's constraint based deadlock check. We have now applied the technique to check theories of a context in Event-B, check assertions in classical B and to the constraint-based invariant check. It became apparent that reducing the model to a relevant set of variables and predicates can improve the applicability of the method because often only a part of a model can be translated to Kodkod. We have implemented such a slicing of the model and plan to validate if this leads to a performance improvement when we use only ProB's constraint solver without Kodkod.

Theory Plug-in support

We adapted ProB to the changes that had been made to the Theory Plug-in in preparation of the upcoming release. ProB had support for recursive data types and operators that were defined by direct definitions. Also the SUM and PRODUCT operators were explicitly supported. Additionally we implemented now 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". 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.

LTL Fairness

We currently explore ways to implement Fairness into ProB's LTL model checker. However, it is already possible to use fairness by using the B to TLA translator and running 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.

Available Documentation

ProB
The ProB Website[2] is the place where we collect information on the ProB toolset. There are several tutorials on ProB available in the User manual section. We also supply documentation on extending ProB for developers.

In addition we run a bug tracking system[3] to document known bugs, workarounds and feature requests.

BMotion Studio
A developer-, user documentation, tutorial and examples are available from a dedicated webpage[4] hosted by the University of Duesseldorf.

Planning

  • We will continue to work on the translation of B to TLA+ in order to use the TLC model checker. The translation needs to be validated and more of the full classical B language needs to be covered. We will also strive to make TLC available within Rodin for Event-B specifications.
  • We will also continue to try to add fairness constraints efficiently both to ProB's own model checker and via the translation to TLC.
  • We will continue our work on porting BMotionStudio to HTML. We want to define an open architecture that allows re-using BMotionStudio outside of ProB.
  • We will further improve support for theories with recursive functions and try to make recursive functions more efficient.
  • We will continue evaluating and improving our SAT backend via Kodkod and also evaluate the possibility of using SMT backends.

References

  1. ↑ http://www.stups.uni-duesseldorf.de/w/Special:Publication/PlaggeLeuschel_Kodkod2012
  2. ↑ http://www.stups.uni-duesseldorf.de/ProB
  3. ↑ http://jira.cobra.cs.uni-duesseldorf.de/
  4. ↑ http://www.stups.uni-duesseldorf.de/bmotionstudio
Retrieved from ‘https://wiki.event-b.org/index.php?title=ADVANCE_D3.3_Model_Checking&oldid=534’