Difference between pages "ADVANCE D3.2 Model Checking" and "D32 Model Animation"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Leuschel
 
imported>Leuschel
 
Line 1: Line 1:
 +
= Model Animation =
 +
 
== Overview ==
 
== Overview ==
{{TODO|Fill this paragraph.}}
+
=== Siemens Application===
 +
The most important additions of the last 12 months are:
 +
* Application of ProB in three active deployments, namely the upgrading of the Paris Metro Line 1 for driverless trains, line 4 of the S\~{a}o Paulo metro and line 9 of the Barcelona metro. We also briefly report on experiments on the models of the CDGVAL shuttle. The paper <ref>Leuschel et al. FM'2009</ref> only contained the initial San Juan case study, which was used to evaluate the potential of our approach.
 +
* In this article we describe the previous method adopted by Siemens in much more detail,  as well as explaining the performance issues with Atelier B.
 +
* Comparisons and empirical evaluations with other potential approaches and alternate tools (Brama, AnimB, BZ-TT and TLC) have been conducted.
 +
* We provide more details about the ongoing validation process of ProB, which is required by Siemens for it to use ProB to replace the existing method.
  
* TLA to B conversion, support for TLA+ in ProB (motivation: TLA can deal with real numbers,...; extend reach of the project)
+
The validation also lead to the discovery of errors in the English version of the Atelier B reference manual.
 +
 +
Also, since  <ref>Leuschel et al. FM'2009</ref>, ProB itself has been further improved inspired by the application, resulting in new optimisations in the kernel (see below).
  
* Continuous improvements of constraint solving capabilities of ProB
+
More details:
 +
* <ref>Leuschel et al. FAC, special issue of FM'2009</ref>
 +
* <ref>Leuschel et al. Draft of Validation Report</ref>
  
* Work towards full support of Theory Plug-in: Support for external and recursive functions, translator, (work in progress)
+
=== Multi-level Animation ===
 +
(ABZ'2010 & SCP journal paper)
  
* Finish conversion to Kodkod, experiments with Kodkod and SMT translators
+
=== Improvements to the ProB Constraint solver and empirical evaluation ===
 +
Various industrial applications have shown the need for improved constraint-solving capabilities (see CBC Deadlock, Test-Case Generation). In order to evaluate ProB, and detect areas for improvement, we have studied to what extent classical constraint satisfaction problems can be  conveniently expressed as B predicates, and then solved by ProB. In particular, we have studied problems such as the n-Queens problem, graph colouring, graph isomorphism detection, time tabling, Sudoku, Hanoi, magic squares, Alphametic puzzles, and several more. We have then compared the performance with respect to other tools, such as the model checker TLC  for TLA+, AnimB for Event-B,  and Alloy.
 +
 
 +
The experiments show that some constraint satisfaction problems can be expressed very conveniently in B and solved very effectively with ProB. For example, TLC takes 8747 seconds (2 hours 25 minuts) to solve the 9-queens problem expressed as a logical predicate; Alloy 4.1.10 with minisat takes 0.406 seconds, ProB 1.3.3 takes 0.01 seconds. For 32 queens, ProB 1.3.3 takes 0.28 seconds, while Alloy 4.1.10 with minisat takes over 4 minutes. For some others, the performance of ProB is still sub-optimal with respect to, e.g., Alloy; we plan to overcome this shortcoming in the future. Our long term goal is that B can not only be used to as a formal method for developing safety critical software, but also as a high-level constraint  programming language.
  
* Maybe: initial work on physical units supprt
+
=== Constraint-Based Deadlock Checking ===
 +
Ensuring the absence of deadlocks is important for certain applications, in particular for Bosch's Adaptive Cruise Control. We are tackling the problem of finding deadlocks via constraint solving rather than by model checking. Indeed, model checking is problematic when the out-degree is very large. In particular, quite often there can be a practically infinite number of ways to instantiate the constants of a B model. In this case, model checking will only find deadlocks for the given constants
 +
chosen.
  
== Motivations / Decisions ==
+
Idea: solve constraints of axioms, invariant together with a constraint specifying a deadlock.
{{TODO|Fill this paragraph.}}
 
  
=== Improvements to Constraint-Solving ===
+
Required Developments:
 +
* implementation of the algorithm, with semantic relevance filtering (to be able to restrict the deadlock search to certain scenarios: in Bosch's case due to the flow plugin, one wants to restrict deadlock checking e.g. to states with the variable Counter set to 10).
 +
* Improvements to ProB's constraint solving engine: (reification of constraints, more precise information propagation for membership constraints, performance improvments in the typchecker and other parts of the kernel)
  
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.
+
Success: Model 1 and Model 2: CrCtrl_Comb2Final;
It is thus important to improve this aspect of ProB.
+
relevance of Counter=10 due to flow
In particular, we have continuously improved the performance of the kernel, as can be seen in the figure below showing the performance of ProB on the N-Queens problem for 100 queens.
 
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]]
+
Deadlock Freedom PO: 34 pages of ASCII, could not be loaded in Rodin "Java Heap Space Error". Counter examples found for 8 versions in 1-18 seconds.
  
=== TLA2B ===
+
=== BMotionStudio for Industrial Models ===
  
TLA+ and B share the common base of predicate logic, arithmetic and set theory.
+
Previously, we presented BMotion Studio, a visual editor which enables the developer of a formal model to set-up easily a domain specific visualization for discussing it with the domain expert. However, BMotion Studio had not yet reached the status of an Industrial strength tool due to the lack of important features known from modern editors.
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 ===
+
In this work we present the improvements to BMotion Studio mainly aimed at upgrading it to an industrial strength tool and to show that we can apply the benefits of BMotion Studio for visualizing more complex models which are on the level of industrial applications. In order to reach this level the contribution of this work consists of three parts:
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 ===
+
* We added a lot of new features to the graphical editor known from modern editors like: Copy-paste support, undo-redo support, rulers, guides and error reporting. One step towards was the redesign of the graphical editor with GEF.
 +
* Since extensibility is a very important design principle for reaching the level of an industrial strength tool we pointed up the extensibility options of BMotion Studio.
 +
* We introduced the visualization for two models which are on the level of industrial applications in order to demonstrate that we can apply the benefits of BMotion Studio for visualizing more complex models. The first model is a mechanical press controller and the second model is a train system which manages the crossing of trains in a certain track network.
  
 +
=== Various other improvements ===
  
In the ProB core, we have improved ProB to better deal with infinite and recursive functions.
+
mainly inspired by Siemens and Bosch Applications
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. As soon as the theory plug-in allows ProB to access the definitions (this is not yet implemented in the theory plug-in) we will finalize the implementation.
+
Improved AVL algorithms, more operators
  
=== Kodkod ===
+
record support, treatment of infinite sets,
The motivation behind incorporating the relational logic solver "Kodkod" into ProB was to evaluate how other technologies can complement ProB's constraint solving capabilities. A tight integration into ProB makes it available as well for model checking, animation as well as for the disproving capabilities mentioned above. Our integration allows predicates from Event-B (and B, Z and TLA+ as well) to be solved using a mixture of SAT-solving and ProB's own constraint-solving capabilities developed using constraint logic programming: the first-order parts which can be dealt with by Kodkod and the remaining parts solved by the existing ProB kernel. We have conducted a first empirical evaluation and analyzed the respective merits of SAT-solving and classical constraint solving. We also compare to using SMT solvers via recently available translators for Event-B.
 
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). An interesting side-effect of our work 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.
 
  
Before starting our translation to Kodkod, we had experimented with several other alternate approaches to solve constraints in ProB.
+
== Motivations ==
[http://bddbddb.sourceforge.net/ bddbddb] offers the user a Datalog-like language that aims to support program analysis.
 
It uses BDDs to represent relations and compute queries on these relations.
 
In particular, one has to represent a state of the model as a bit-vector and events have to be implemented as relations between two of those bit-vectors.
 
These relations have to be constructed by creating BDDs directly with the underlying BDD library (JavaBDD) and storing them into a file.
 
Soon after starting experimenting with [http://bddbddb.sourceforge.net/ bddbddb] it became  apparent that due to the lack of more abstract data types than bit vectors, the complexity of a direct translation from B to [http://bddbddb.sourceforge.net/ bddbddb] was too high, even for small models, and this avenue was abandoned.
 
 
SAL is a model-checking framework combining a range of tools for reasoning about systems.
 
The SAL tool suite includes a state of the art symbolic (BDD-based) and bounded (SAT-based) model checkers.
 
Some first results were encouraging for a small subset of the Event-B language, but the gap between B and SAL turned out to be too big in general and no realistic way was found to handle important B operators.
 
  
Kodkod has the advantage that is provides good support for relations and sets which play an essential role in Event-B's mathematical notation.
+
The above works were motivated mainly to support the following three industrial deployments:
 +
* Siemens: enable Siemens to use ProB in their SIL4 development chain, replacing Atelier B for data validation.
 +
* Bosch: provide animation and constraint-based deadlock detection for the Adaptive Cruise Control
 +
* SAP: provide a way to generate test cases using constraint-based animation
  
 
== Available Documentation ==
 
== Available Documentation ==
{{TODO|Fill this paragraph.}}
 
  
=== Constraint Solving ===
+
=== References ===
 
+
<references/>
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. 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.
 
  
 
== Planning ==
 
== Planning ==
{{TODO|Fill this paragraph.}}
 
 
== References ==
 
<references/>
 
  
[[Category:ADVANCE D3.2 Deliverable]]
+
* Finish Validation Report
 +
* Write up Constraint-Based Deadlock Checking and integrate fully into Rodin Platform
 +
* Support mathematical extensions in ProB

Revision as of 09:44, 29 November 2010

Model Animation

Overview

Siemens Application

The most important additions of the last 12 months are:

  • Application of ProB in three active deployments, namely the upgrading of the Paris Metro Line 1 for driverless trains, line 4 of the S\~{a}o Paulo metro and line 9 of the Barcelona metro. We also briefly report on experiments on the models of the CDGVAL shuttle. The paper [1] only contained the initial San Juan case study, which was used to evaluate the potential of our approach.
  • In this article we describe the previous method adopted by Siemens in much more detail, as well as explaining the performance issues with Atelier B.
  • Comparisons and empirical evaluations with other potential approaches and alternate tools (Brama, AnimB, BZ-TT and TLC) have been conducted.
  • We provide more details about the ongoing validation process of ProB, which is required by Siemens for it to use ProB to replace the existing method.
The validation also lead to the discovery of errors in the English version of the Atelier B reference manual.

Also, since [2], ProB itself has been further improved inspired by the application, resulting in new optimisations in the kernel (see below).

More details:

Multi-level Animation

(ABZ'2010 & SCP journal paper)

Improvements to the ProB Constraint solver and empirical evaluation

Various industrial applications have shown the need for improved constraint-solving capabilities (see CBC Deadlock, Test-Case Generation). In order to evaluate ProB, and detect areas for improvement, we have studied to what extent classical constraint satisfaction problems can be conveniently expressed as B predicates, and then solved by ProB. In particular, we have studied problems such as the n-Queens problem, graph colouring, graph isomorphism detection, time tabling, Sudoku, Hanoi, magic squares, Alphametic puzzles, and several more. We have then compared the performance with respect to other tools, such as the model checker TLC for TLA+, AnimB for Event-B, and Alloy.

The experiments show that some constraint satisfaction problems can be expressed very conveniently in B and solved very effectively with ProB. For example, TLC takes 8747 seconds (2 hours 25 minuts) to solve the 9-queens problem expressed as a logical predicate; Alloy 4.1.10 with minisat takes 0.406 seconds, ProB 1.3.3 takes 0.01 seconds. For 32 queens, ProB 1.3.3 takes 0.28 seconds, while Alloy 4.1.10 with minisat takes over 4 minutes. For some others, the performance of ProB is still sub-optimal with respect to, e.g., Alloy; we plan to overcome this shortcoming in the future. Our long term goal is that B can not only be used to as a formal method for developing safety critical software, but also as a high-level constraint programming language.

Constraint-Based Deadlock Checking

Ensuring the absence of deadlocks is important for certain applications, in particular for Bosch's Adaptive Cruise Control. We are tackling the problem of finding deadlocks via constraint solving rather than by model checking. Indeed, model checking is problematic when the out-degree is very large. In particular, quite often there can be a practically infinite number of ways to instantiate the constants of a B model. In this case, model checking will only find deadlocks for the given constants chosen.

Idea: solve constraints of axioms, invariant together with a constraint specifying a deadlock.

Required Developments:

  • implementation of the algorithm, with semantic relevance filtering (to be able to restrict the deadlock search to certain scenarios: in Bosch's case due to the flow plugin, one wants to restrict deadlock checking e.g. to states with the variable Counter set to 10).
  • Improvements to ProB's constraint solving engine: (reification of constraints, more precise information propagation for membership constraints, performance improvments in the typchecker and other parts of the kernel)

Success: Model 1 and Model 2: CrCtrl_Comb2Final; relevance of Counter=10 due to flow

Deadlock Freedom PO: 34 pages of ASCII, could not be loaded in Rodin "Java Heap Space Error". Counter examples found for 8 versions in 1-18 seconds.

BMotionStudio for Industrial Models

Previously, we presented BMotion Studio, a visual editor which enables the developer of a formal model to set-up easily a domain specific visualization for discussing it with the domain expert. However, BMotion Studio had not yet reached the status of an Industrial strength tool due to the lack of important features known from modern editors.

In this work we present the improvements to BMotion Studio mainly aimed at upgrading it to an industrial strength tool and to show that we can apply the benefits of BMotion Studio for visualizing more complex models which are on the level of industrial applications. In order to reach this level the contribution of this work consists of three parts:

  • We added a lot of new features to the graphical editor known from modern editors like: Copy-paste support, undo-redo support, rulers, guides and error reporting. One step towards was the redesign of the graphical editor with GEF.
  • Since extensibility is a very important design principle for reaching the level of an industrial strength tool we pointed up the extensibility options of BMotion Studio.
  • We introduced the visualization for two models which are on the level of industrial applications in order to demonstrate that we can apply the benefits of BMotion Studio for visualizing more complex models. The first model is a mechanical press controller and the second model is a train system which manages the crossing of trains in a certain track network.

Various other improvements

mainly inspired by Siemens and Bosch Applications

Improved AVL algorithms, more operators

record support, treatment of infinite sets,

Motivations

The above works were motivated mainly to support the following three industrial deployments:

  • Siemens: enable Siemens to use ProB in their SIL4 development chain, replacing Atelier B for data validation.
  • Bosch: provide animation and constraint-based deadlock detection for the Adaptive Cruise Control
  • SAP: provide a way to generate test cases using constraint-based animation

Available Documentation

References

  1. Leuschel et al. FM'2009
  2. Leuschel et al. FM'2009
  3. Leuschel et al. FAC, special issue of FM'2009
  4. Leuschel et al. Draft of Validation Report

Planning

  • Finish Validation Report
  • Write up Constraint-Based Deadlock Checking and integrate fully into Rodin Platform
  • Support mathematical extensions in ProB