Difference between pages "D23 Decomposition" and "D32 Model Animation"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Pascal
 
imported>Leuschel
 
Line 1: Line 1:
= Overview =
+
= Model Animation =  
The Event-B model decomposition is a new feature in the Rodin platform.
 
  
Two methods have been identified in the DEPLOY project for model decomposition: the ''shared variable'' decomposition (or A-style decomposition, after Abrial), and the ''shared event'' decomposition (or B-style decomposition, after Butler). They both answer to the same requirement, namely the possibility to decompose a model <math>M</math> into several independent sub-models <math>M_1, ...,M_n</math>.
+
== 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.
  
Academic (ETH Zurich, University of Southampton) and industrial (Systerel) partners were involved in the specifications and developments. Systerel, which could have useful discussions with Jean-Raymond Abrial on the topic, was more especially responsible of the A-style decomposition. The University of Southampton, where Michael Butler is professor, was in charge of the B-style decomposition.
+
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).
  
= Motivations =
+
More details:
One of the most important feature of the Event-B approach is the possibility to introduce new events and data-refinement of variables during refinement steps.
+
* <ref>Leuschel et al. FAC, special issue of FM'2009</ref>
 +
* <ref>Leuschel et al. Draft of Validation Report</ref>
  
It however results in an increasing complexity of the refinement process when having to deal with many events, many state variables, and consequently many proof obligations.
+
=== Multi-level Animation ===
This is well illustrated in the ''Event build-up'' slide of the Wright presentation during the Rodin Workshop 2009.
+
(ABZ'2010 & SCP journal paper)
: See [http://wiki.event-b.org/index.php/Image:Steve_Wright_Quite_Big_Model_Presentation.pdf http://wiki.event-b.org/index.php/Image:Steve_Wright_Quite_Big_Model_Presentation.pdf].
 
  
The purpose of the Event-B model decomposition is precisely to give a way to address such a difficulty, by cutting a large model <math>M</math> into smaller sub-models <math>M_1, ..., M_n</math>. The sub-models can then be refined separately and more comfortably than the whole. The constraint that shall be satisfied by the decomposition is that these refined models might be recomposed into a whole model <math>MR</math> in a way that guarantees that <math>MR</math> refines <math>M</math>.
+
=== 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.
  
The model decomposition leads to some interesting benefits:
+
=== Constraint-Based Deadlock Checking ===
* Design/architectural decision. It applies in particular when it is noticed that it is not necessary to consider the whole model for a given refinement step, because only a few events and variables are involved instead.
+
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
* Complexity management. In other words, it alleviates the complexity by splitting the proof obligations over the sub-models.
+
chosen.
* Team development. More precisely, it gives a way for several developers to share the parts of a decomposed model, and to work independently and possibly in parallel on them.
 
  
Note that the possibility of team development is among the current priorities for all industrial partners. The model decomposition is a first answer to this issue.
+
Idea: solve constraints of axioms, invariant together with a constraint specifying a deadlock.
  
= Choices / Decisions =
+
Required Developments:
The main decision concerning the implementation of the Event-B model decomposition in the Rodin platform is to make available both decomposition styles (''shared variables'' vs. ''shared events'') through one single plug-in. These approaches are indeed complementary and the end-user may take advantage of the former or of the latter, depending on the model (eg. the ''shared variables'' approach seems more suitable when modelling parallel system and the ''shared events'' approach seems more suitable when modelling message-passing distributed systems).
+
* 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)
  
Choices, either related to the plug-in core or to the plug-in graphical user interface, have been made with the following constraints in mind:
+
Success: Model 1 and Model 2: CrCtrl_Comb2Final;
* Planning. Some options, such as using the Graphical Modelling Framework for the decomposition visualization, or outsourcing the context decomposition, have not been explored (at least in the first instance), mainly because of time constraints (according to the DEPLOY description of work, the decomposition support was expected by the end of 2009).
+
relevance of Counter=10 due to flow
* Easy-to-use (however not simplistic) tool. It applies on the one hand to the tool implementation (decomposition wizard, configuration file to replay the decomposition) and on the other hand to the tool documentation (the purpose of the user's guide is to provide useful information for beginners and for more advanced users, in particular through a ''Tips and Tricks'' section).
 
* Modularity and consistency. In particular, the developments have not been performed in the Event-B core. Instead the Eclipse extension mechanisms have been used to keep the plug-in independent (eg. the static checker, the proof obligation generator and the editor have been extended).
 
* Performance.
 
* Recursivity. Thus, it is possible to decompose a previously decomposed model.
 
  
Other technical decisions are justified in the specification wiki pages.
+
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.
  
= Available Documentation =
+
=== BMotionStudio for Industrial Models ===
The following wiki pages have been respectively written for developers and end-users to document the Event-B model decomposition:
 
* Shared variables (A-style) decomposition specification.
 
:See [[Event_Model_Decomposition | http://wiki.event-b.org/index.php/Event_Model_Decomposition]].
 
* Decomposition plug-in user's guide.
 
:See [[Decomposition_Plug-in_User's_Guide | http://wiki.event-b.org/index.php/Decomposition_Plug-in_User's_Guide]].
 
  
= Planning =
+
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.
The decomposition plug-in is available since release 1.2 of the platform.
+
 
:See [[Rodin_Platform_1.2_Release_Notes | http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes]].
+
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 ===
 +
<references/>
 +
 
 +
== Planning ==
 +
 
 +
* 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