Revision as of 16:05, 23 August 2013

Overview

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.

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

BMotion Studio

BMotion Studio 2 Prototype

BMotion Studio provides an easy and fast way to create a visualization for a formal model. It comes with a set of predefined widgets and observer which are sufficient for most visualizations. However, it is still cumbersome to add custom widgets and observer to BMotion Studio, since the user needs programming skills in Java and Eclipse Plugin Development. As a consequence we decided to replace the rendering-engine of BMotion Studio with HTML. This has the benefit that we can use the entire HTML functionality. For instance, HTML elements like tables, buttons and images as well as features like CSS (Cascading Style Sheets) and SVG (Scalable Vector Graphics). In addition, the user can reuse all HTML snippets which can be found in the WWW for his own visualization. While the user can create visualizations by writing HTML or SVG, we will also provide a way to create visualizations as in the old BMotion Studio, i.e. via a visual editor with easy to use dialogues and wizards. The screenshot shows a first prototype of the new BMotion Studio visualising a model of a simple lift.

Available Documentation

ProB
The ProB Website^[1] 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^[2] to document known bugs, workarounds and feature requests.

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

Planning

TODO

References

[1] ttp://www.stups.uni-duesseldorf.de/ProB

[2] ttp://jira.cobra.cs.uni-duesseldorf.de/

[3] ttp://www.stups.uni-duesseldorf.de/bmotionstudio

[1]

[2]

[3]

@@ Line 1: / Line 1: @@
 = Overview =
+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.
-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<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.
-* A conversion from TLA to B has been added. ProB now supports TLA+. The motivation is to extend the reach of the project and to learn from TLA concerning certain features relevant for cyber-physical systems (e.g. real number support).
+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.
-* There is work in progress towards full support of Theory plug-in: support for external and recursive functions has been added.
+= Motivations / Decisions =
-* The conversion to the relational logic solver Kodkod has been completed and experiments with Kodkod and SMT translators have been conducted.
-* We are working on an analysis of the use of physical units in a formal model.
+'''Secondary toolchain'''
-* We improved the usability of the LTL model checker.
+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]
-* Regarding BMotion Studio, we focused on fixing identified bugs and rectifying usability issues.
+'''B to TLA<sup>+</sup>'''
-= Motivations / Decisions =
+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.
+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.
-== Improvements to Constraint-Solving ==
+{{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.''
-ProB's constraint solving capabilities are at the core of many of ProB's features: animation of high-level models with complicated predicates, model-based testing, constraint-based invariant and deadlock checking, etc.
+{{TODO}}'''  Constraint Solver Improvements '''
-It is thus important to improve this aspect of ProB.
+''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.
-In particular, we have continuously improved the performance of the kernel, as can be seen in the figure below showing the performance of ProB (in seconds) on the N-Queens problem for 100 queens.
+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.''
-Other improvements lie in better expansion of universal and existential quantifiers, reification for the the <tt>bool</tt> operator and support for infinite and recursive functions.
-The latter is particularly important in light of the Theory Plug-In work below.
-[[Image:performance of ProB on the N-Queens problem for 100 queens.jpg|240px]]
+'''Theory Plug-in support'''
-== TLA2B ==
+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".
+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.
-TLA+ and B share the common base of predicate logic, arithmetic and set theory.
+'''  LTL Fairness'''
-However, there are still considerable differences, such as very different approaches to typing and modularization. Some features of TLA+ are interesting in the context of cyber-physical systems, such as real numbers.
-There is also considerable difference in the available tool support. In particular, we wanted to compare ProB with TLC and gain insights about performance.
-== Physical Units ==
+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.
-Formal models of cyber physical systems will contain variables which represent values with physical units.
-We are thus exploring to use the ProB model checker as a tool to infer and validate physical units usage in formal models.
-In particular, we want to make sure that the physical units in a model are used in a consistent way.
-== Theory Plug-in and Mathematical Extensions ==
+''' 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.
-In the ProB core, we have improved ProB to better deal with infinite and recursive functions.
+'''  BMotion Studio '''
-This can be used to provide formal specifications for mathematical extensions which can be animated and model checked by ProB.
-Using the newly developed external function mechanism, it should also be possible to support floats or reals, which will be important for certain cyber-physical systems.
-On the technical side, we have extended the ProB internal representation of predicates and expressions to support the Theory plug-in. The implementation will be finalize as the Theory plug-in will allow access to definitions will be granted to ProB.
+[[File:d33_bms2_prototype.png|150px|thumb|right|BMotion Studio 2 Prototype]]
-== Kodkod ==
+BMotion Studio provides an easy and fast way to create a visualization for a formal model. It comes with a set of predefined widgets and observer which are sufficient for most visualizations. However, it is still cumbersome to add custom widgets and observer to BMotion Studio, since the user needs programming skills in Java and Eclipse Plugin Development. As a consequence we decided to replace the rendering-engine of BMotion Studio with HTML. This has the benefit that we can use the entire HTML functionality. For instance, HTML elements like tables, buttons and images as well as features like CSS (Cascading Style Sheets) and SVG (Scalable Vector Graphics). In addition, the user can reuse all HTML snippets which can be found in the WWW for his own visualization.
-We have integrated a translation of B predicates to the relational logic solver "Kodkod" and evaluated how ProB's constraint solving compares to Kodkod's SAT solving.
+While the user can create visualizations by writing HTML or SVG, we will also provide a way to create visualizations as in the ''old'' BMotion Studio, i.e. via a visual editor with easy to use dialogues and wizards. The screenshot shows a first prototype of the new BMotion Studio visualising a model of a simple lift.
-The integration allows to apply SAT solving to predicates where a translation is possible and a fallback to constraint solving for the remaining predicates.
-Our experiments have shown that the translation can be highly beneficial for certain kinds of constraints, and as such opens up new ways to analyze and validate formal specifications in Event-B. However, the experiments have also shown that the constraint logic programming approach of ProB can be superior in a considerable number of scenarios; the translation to Kodkod and down to SAT is not (yet) the panacea. The same can be said of the existing translations from B to SMT.
-As such, we believe that much more research required to reap the best of both worlds (SAT/SMT and constraint programming).
-A side-effect of the translation to Kodkod is that the ProB toolset now provides a double-chain (relying on technology developed independently and using different programming languages and paradigms) of validation for first-order predicates, which should prove relevant in high safety integrity level contexts.
-In comparision with other formalisms Kodkod has the advantage that is provides good support for relations and sets which play an essential role in Event-B's mathematical notation.
-== LTL ==
-ProB supports LTL model checking. One problem when using LTL to validate a model is that counter-examples returned by the model checker are often hard to understand.
-A counter-example typically consists of a lasso-chaped sequence of states and events. Instead of just loading the sequence into the history of the animator, we have
-implemented a dedicated visualisation for LTL counter-examples. The visualisation which is now part of ProB's Rodin plug-in shows why an LTL operator is true or false in each state of the sequence.
-== CSP and B ==
-ProB supports also other formalisms like CSP. CSP can also be used to guide B and Event-B models and can also be used for specifying scenarios or for model testing.
-Within the project this feature of ProB was continuously maintained and improved. We have extended the implementation of the CSP interpreter and animator to be able to support more complex and larger data types (e.g. mixing of dot and non-associative tuples) as well as supporting more complicated pattern matching inside set comprehensions and function definitions. Some effort for supporting more of CSP built-in functions (like seq(-), set(-) and card(-))was made as well.
-Finally, ProB now supports checking LTL-assertions directly from the CSP model by using pragmas ({-# assert_ltl = … #-}). The syntax is the same as for LTL-assertions in DEFINTION clauses in B models.
 = Available Documentation =
-== Constraint Solving ==
+'''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.
-The improvements are available in the nightly builds of ProB.
-Two specific pages have been added to the ProB user manual:  <ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/Recursively_Defined_Functions Recursive functions entry in ProB user manual</ref>,  <ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/External_Functions External functions entry in ProB user manual</ref>.
-== TLA2B ==
-The TLA+ to B translation has been published at the iFM'2012 conference. A technical report is available<ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschelTLA2012 Translating TLA+ to B for Validation with ProB. Technical Report, 2012.</ref>
-A presentation at the FM'2012 TLA+ workshop will also be made.
-A page has been added to the ProB user manual: <ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/TLA TLA2B entry in ProB user manual</ref>.
-== Physical Units ==
-This work is still in progress. A first tutorial page is available in the ProB online documentation <ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/Tutorial_Unit_Plugin Unit Plug-in Tutorial entry in ProB user manual</ref>. Full documentation will be made available later in the project.
-The latest nightly build of ProB contains an experimental version of the analysis.
-== Kodkod ==
-A technical report has been published on the validation using ProB and Kodkod <ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/PlaggeLeuschel_Kodkod2012 Validating B,Z and TLA+ using ProB and Kodkod. Technical Report, 2012.</ref>. The paper has been accepted for FM'2012.
-== LTL ==
-The concept and implemenation of the visualisation is described in <ref>http://www.stups.uni-duesseldorf.de/w/Visualisierung_von_LTL-Gegenbeispielen Andriy Tolstoy: Visualisierung von LTL-Gegenbeispielen, Master thesis, University of Düsseldorf, 2012</ref>.
+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 ==
+'''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.
-A developer-, user documentation, tutorial and examples are available at <ref>http://www.stups.uni-duesseldorf.de/bmotionstudio</ref>.
 = Planning =
+{{TODO}}
-=== Physical Units ===
-Physical units work will be completed.
-First experiments with industrial models from Alstom are encouraging.
-== 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.
-== Constraint Solving ==
-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.
-== LTL ==
-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.
-== 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.
 = References =
 <references/>
-[[Category:ADVANCE D3.2 Deliverable]]
+[[Category:ADVANCE D3.3 Deliverable]]

Difference between pages "ADVANCE D3.2 Model Checking" and "ADVANCE D3.3 Model Checking"

Revision as of 16:05, 23 August 2013

Contents

Overview

Motivations / Decisions

Available Documentation

Planning

References

Navigation menu

Page actions

Page actions

Personal tools

Navigation

contribute

Search

Tools