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

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Ladenberger
 
imported>Leuschel
 
Line 1: Line 1:
−
= Overview =
+
= Model Animation =  
−
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.
 
  
−
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.
+
== 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 <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.
  
−
= Motivations / Decisions =
+
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).
  
 +
More details:
 +
* <ref>Leuschel et al. FAC, special issue of FM'2009</ref>
 +
* <ref>Leuschel et al. Draft of Validation Report</ref>
  
−
'''Secondary toolchain'''
+
=== Multi-level Animation ===
 +
(ABZ'2010 & SCP journal paper)
  
−
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]
+
=== 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.
  
−
'''B to TLA<sup>+</sup>'''
+
=== 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.
  
−
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.
+
Idea: solve constraints of axioms, invariant together with a constraint specifying a deadlock.
−
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'''
+
Required Developments:
−
''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).
+
* 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).
−
We will evaluate how we can employ more SMT based techniques in ProB.''
+
* 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)
  
−
{{TODO}}'''  Constraint Solver Improvements '''
+
Success: Model 1 and Model 2: CrCtrl_Comb2Final;
−
''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.
+
relevance of Counter=10 due to flow
−
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'''
+
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.
  
−
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.
+
=== BMotionStudio for Industrial Models ===
−
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'''
+
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.
  
−
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.
+
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:
  
−
''' Physical Units'''
+
* 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.
  
−
The work on physical unit support has been completed and is available as an optional plug-in available from the ProB update site.
+
=== Various other improvements ===
  
−
'''  BMotion Studio '''
+
mainly inspired by Siemens and Bosch Applications
  
−
[[File:d33_bms2_prototype.png|150px|thumb|right|BMotion Studio 2 Prototype]]
+
Improved AVL algorithms, more operators
  
−
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.
+
record support, treatment of infinite sets,
−
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 =
+
== Motivations ==
  
−
'''ProB'''<br>
+
The above works were motivated mainly to support the following three industrial deployments:
−
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.
+
* 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
  
−
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.
+
== Available Documentation ==
  
−
'''BMotion Studio'''<br>
+
=== References ===
−
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.
+
<references/>
  
−
= Planning =
+
== Planning ==
−
{{TODO}}
 
−
 
 
−
= References =
 
−
<references/>
 
  
−
[[Category:ADVANCE D3.3 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
Retrieved from ‘https://wiki.event-b.org/index.php?title=ADVANCE_D3.3_Model_Checking&oldid=2511’