Difference between pages "D32 Code generation" and "D32 Model Animation"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
m
 
imported>Daniel
 
Line 1: Line 1:
= General Overview =
+
= Model Animation =  
  
The code generation activity has been undertaken at the University of Southampton. This has been a new line of work for DEPLOY that was not identified in the original Description of Work for the project. The development of the approach, and the tools to support, it involved a number of team members at Southampton; and also at other institutions. This work draws on our recent experience with technologies such as ''Shared Event Decomposition'' <ref name = "SharedEventDecomp">[[Event_Model_Decomposition]]</ref>, and the ''EMF Framework for Event-B'' <ref name = "EMF4EventB">[[EMF_framework_for_Event-B]]</ref>. There was collaboration at an early stage with Newcastle University, where we explored the commonalities between their flow plug-in <ref name = "flow">[[Flows]]</ref> and the flow control structures used in our approach. Collaboration with the University of York was also established since we chose to use their ''Epsilon'' <ref name = "Epsilon"> http://www.eclipse.org/gmt/epsilon/</ref> model-to-model transformation technology.
+
== 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 name="fm2009">Michael Leuschel, Jérôme Falampin, Fabian Fritz and Daniel Plagge, Automated Property Verification for Large Scale B Models, FM'2009, LNCS 5850, Springer-Verlag, 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 =
+
The validation also lead to the discovery of errors in the English version of the Atelier B reference manual.
 +
 +
Also, since  <ref name="fm2009"/>, ProB itself has been further improved inspired by the application, resulting in new optimisations in the kernel (see below).
  
The decision was taken in 2009 to include code generation as a project goal <ref name = "d23"> [[D23_Code_Generation]]</ref>. It had been recognised that support for generation of code from refined Event-B models would be an important factor in ensuring eventual deployment of the DEPLOY approach within their organisations. This was especially true for Bosch and Space Systems Finland (SSF). After receiving more detailed requirements from Bosch and SSF, it became clear we should focus our efforts on supporting the generation of code for typical real-time embedded control software.
+
More details:
 +
* <ref>Leuschel et al. FAC, special issue of FM'2009</ref>
 +
* <ref>Leuschel et al. Draft of Validation Report</ref>
  
= Choices / Decisions =
+
=== Multi-level Animation ===
== Strategic Overview ==
 
During the last year we have focussed on supporting the generation of code for typical real-time embedded control software. To this end we have evolved a multi-tasking approach which is conceptually similar to that of the Ada tasking model. Tasks are modelled by an extension to Event-B, called ''Tasking Machines''. Tasking Machines are an extension of the existing Event-B Machine component. In implementations such as Ada, tasks share the resources and have mutually exclusive access to shared state through the use of a protection mechanism. An Event-B machine can also be viewed as an abstraction of a shared resource, and the  mechanism protecting it. We use existing Event-B machines with minimal extensions (called Shared Machines) to represent shared resources.
 
  
For real-time control, periodic and one-shot activation is currently supported; and it is planned to support triggered tasks in the near future. Tasks have priorities to ensure appropriate responsiveness of the control software. For the DEPLOY project, it was regarded as sufficient to support construction of programs with a fixed number of tasks and a fixed number of shared variables – no dynamic creation of processes or objects has been accommodated.  
+
Prior versions of ProB only supported the animation of a single refinement level. Abstract variables and predicates referring to them were ignored.
 +
In
 +
<ref name="abz2010">Stefan Hallerstede, Michael Leuschel and Daniel Plagge, Refinement-Animation for Event-B - Towards a Method of Validation, ASM'2010, LNCS 5977, Springer-Verlag, 2010</ref>
 +
and
 +
<ref name="ml-journal">Stefan Hallerstede, Michael Leuschel and Daniel Plagge, Validation of Formal Models by Refinement Animation, to appear in Science of Computer Programming, Elsevier</ref>
 +
we extended ProB in a way that all refinement levels of a model can be animated simultaneously.
  
Our main goal this year has been to devise an approach for, and provide tool support for, code generation (initially to Ada). In accord with the resources available during the year it was decided to limit the provision of tool support to that of a demonstrator tool. The tool is a proof-of-concept only, and lacks the productivity enhancements expected in a more mature tool. Nevertheless much insight has been gained in undertaking this work; it lays a foundation for future research, and will be useful since it will allow interested parties to explore the approach.
+
First, this can give the user a deeper insight into how the model behaves and how the refinement levels are related to each other.
  
== The Tasking Extension for Event-B ==
+
Second, we can now find errors in context of refinement. This include violation of the gluing invariant or not satisfiable witnesses for abstract variables. If such errors are present in a model, the corresponding proof obligation cannot be discharged. But without an animator it is not always easy to see for an user if this is caused by the complexity of the proof or by an error.
  
The following text can be read in conjunction with the slides<ref name = "Zurich2010Slides">http://deploy-eprints.ecs.soton.ac.uk/260/2/CGSlidesAndy%2520Edmunds%2520-%2520Code%2520Generation%2520Slides.pdf</ref> from the Deploy Plenary Meeting - Zurich 2010.
+
In the articles we summarized Event-B's current refinement methodology and showed for each proof obligation how the algorithm would find a counter-example. We presented empirical results and discussed how the algorithm can be combined with symmetry reduction.
  
Tasking Event-B can be viewed as an extension of the existing Event-B language. We use the existing approaches of refinement and decomposition to structure a development that is suitable for construction of a Tasking Development. At some point during the modelling phase parameters may have to be introduced to facilitate decomposition. This constitutes a natural part of the refinement process as it moves towards decomposition and on to the implementation level. During decomposition parameters form part of the interface that enables event synchronization. We make use of this interface and add information (see [[#Implementing Events]]) to facilitate code generation.
+
=== Evaluation of the ProB Constraint Solver ===
 +
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 (TLC was only able to solve the n-queens problem up until n=9, or n=14 when reformulating the problem as a model checking problem rather than a constraint-solving problem). In another small experiment, we checked whether two graphs with 9 nodes of out-degree exactly one are isomorphic by checking for the existence of a permutation which preserved the graph structure. TLC finds a permutation after 2 hours 6 minutes and 28 seconds; ProB 1.3.3 takes 0.01 seconds to find the same solution, while Alloy takes 0.11 seconds with SAT4J and 0.05 seconds with minisat.
 +
For some other examples (in particular time-tabling) involving operators such as the relational image, 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.
  
A Tasking Development is generated programmatically, at the direction of the user; the Tasking Development consists of a number of machines (and perhaps associated contexts). In our approach we make use of the Event-B EMF extension mechanism which allows addition of new constructs to a model. The tasking extension consists of the constructs in the following table.
+
=== 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.
  
<center>
+
The basic idea is to generate deadlocks by solving a constraint consisting of the axioms Ax, the invariants Inv together with a constraint D specifying a deadlock. More formally, D is the negation of the disjunction of all the guards.
{| border="1"
 
|Construct
 
|Options
 
|-
 
|Machine Type
 
|DeclaredTask, AutoTask, SharedMachine
 
|-
 
|Control
 
|Sequence, Loop, Branch, EventSynch
 
|-
 
|Task Type
 
|Periodic(n), Triggered, Repeating, OneShot
 
|-
 
|Priority
 
| -
 
|-
 
|Event Type
 
|Branch, Loop, ProcedureDef, ProcedureSynch
 
|-
 
|Parameter Type
 
|ActualIn, ActualOut, FormalIn, FormalOut
 
|}
 
</center>
 
  
The machines in the Tasking Development are extended with the constructs shown in the table, and may be viewed as keywords in a textual representation of the language. With extensions added, a Tasking Development can be translated to a common language model for mapping to implementation source code. There is also a translator that constructs new machines/contexts modelling the implementation, and these should refine/extend the existing elements of the Event-B project.
+
The following tool developments were required to meet the challenges raised by the industrial application:
 +
* generation of the deadlock freedom proof obligation by ProB (to avoid dependence on other plug-ins and being able to control whether theorems are to be used or not; currently they are not used)
 +
* implementation of a constraint-based deadlock checking algorithm:
 +
** with the possibility to specify an additional goal predicate  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
 +
** with semantic relevance filtering (to be able to filter out guards which are always false given the goal predicate).
 +
** with partitioning of the constraint predicate into components and optionally reordering according to usage (basic predicates which occur in most guards are listed first)
 +
* Improvements to ProB's constraint solving engine: (reification of constraints, detection of common sub-predicates, more precise information propagation for membership constraints, performance improvments in the typchecker and other parts of the kernel).
  
== Tasking Machines ==
+
ProB has been applied successfully to two models of the adaptive cruise control by Bosch. The more complicated model is CrCtrl_Comb2Final. To give an idea, here are some statistics of the deadlock freedom proof obligation for CrCtrl_Comb2Final:
The following constructs relate only to Tasking Machines, and provide implementation details. Timing of periodic tasks is not modelled formally. Tasking Machines are related to the concept of an Ada task. These can be implemented in Ada using tasks, in C using the pthread library C, or in Java using threads.
+
* when printed in 9-point Courier ASCII the formula takes 32 A4 pages (the disjunction of the guards starts at page 6)
 +
* the model contains 59 events with 837 guards (19 of them disjunctions, some of which themselves nested)
 +
* Bosch are interested in deadlocks that are possible according to a flow specified using the flow plugin; these can be found with ProB by specifying a goal predicate (such as "Counter=10")
 +
* the proof obligation (as generated by the flow plugin) initially could not be loaded in Rodin due to "Java Heap Space Error".
 +
* Counter examples are found by ProB for various versions of the model in 9-24 seconds (including loading, typechecking and deadlock PO generation; the constraint solving time is 1.03 to 12.86 seconds).
  
* Tasking Machines may be characterised by the following types:
+
=== BMotionStudio for Industrial Models ===
** AutoTasks - Singleton Tasks.
 
** Declared tasks - (Not currently used) A task template relating to an Ada ''tasktype'' declaration.
 
** TaskType - Defines the scheduling, cycle and lifetime of a task. i.e. one-shot periodic or triggered.
 
** Priority - An integer value is supplied, the task with the highest value priority takes precedence when being scheduled.
 
  
== Shared Machines ==
+
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.
A Shared Machine corresponds to the concept of a protected resource, such as a monitor. They may be implemented in Ada as a Protected Object, in C using mutex locking, or in Java as a monitor.
 
  
* Applied to the Shared Machine we have:
+
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:
** A SharedMachine ''keyword'' that identifies a machine as a Shared Machine.
 
  
== Tasks and Events ==
+
* 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.
=== Control Constructs ===
+
* 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.
Each Tasking Machine has a ''task body'' which contains the flow control, or algorithmic, constructs.  
+
* 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.
  
* We have the following constructs available in the Tasking Machine body:
+
=== Various other improvements ===
** Sequence - for imposing an order on events.
 
** Branch - choice between a number of mutually exclusive events.
 
** Loop - event repetition while it's guard remains true.
 
** Event Synchronisation - synchronization between an event in a Tasking Machine and an event in a Shared Machine. Synchronization corresponds to an subroutine call with atomic (with respect to an external viewer) updates. The updates in the protected resource are implemented by a procedure call to a protected object, and tasks do not share state.  The synchronization construct also provides the means to specify parameter passing, both in and out of the task.
 
** Event wrappers - The event synchronization construct is contained in an event wrapper. The wrapper may also contain a single event (we re-use the synchronization construct, but do not use it for synchronizing). The event may belong to the Tasking Machine, or to a Shared Machine that is visible to the task. Single events in a wrapper correspond to a subroutine call in an implementation.
 
  
=== Implementing Events ===
+
mainly inspired by Siemens and Bosch Applications
An event's role in the implementation is identified using the following extensions which are added to the event. Events used in task bodies are 'references' that make use of existing event definitions from the abstract development. The events are extended. to assist with translation, with a keyword indicating their role in the implementation.
 
  
* Event implementation.
+
* Improved AVL algorithms, more operators
** Branch - In essence a task's event is split in the implementation; guards are mapped to branch conditions and actions are mapped to the branch body. If the branch refers to a Shared Machine event (procedureDef) then this is mapped to a simple procedure call.
 
** Loop - The task's event guard maps to the loop condition and actions to to loop body. If the loop refers to a Shared Machine event then it is mapped to a simple procedure call.
 
** ProcedureSych - This usually indicates to the translator that the event maps to a subroutine, but an event in a task may not require a subroutine implementation if its role is simply to provide parameters for a procedure call.
 
** ProcedureDef - Identifies an event that maps to a (potentially blocking) subroutine definition. Event guards are implemented as a conditional wait; in Ada this is an entry barrier, and in C may use a pthread condition variable .
 
  
In an implementation, when an subroutine is defined, its formal parameters are replaced by actual parameter values at run-time. To assist the code generator we extend the Event-B parameters. We identify formal and actual parameters in the implementation, and add the following keywords to the event parameters, as follows:
+
* record support: automatic detection of records described by a bijection between a cartesian product and a carrier set (these axioms can either be entered manually, such as in the Bosch models, or generated by the Records plug-in).  
  
* Event parameter types
+
* treatment of infinite sets, in particular complement sets such as INTEGER \ {x}. Such sets are being used in some of the Siemens models.
** FormalIn or FormalOut - event parameters are extended with the ParameterType construct. Extension with formal parameters indicates a mapping to formal parameters in the implementation.
 
** ActualIn or ActualOut - Extension with an actual parameter indicates a mapping to an actual parameter in the implementation.
 
  
== Other Technical Issues ==
+
* Partitioning of predicates into connected sub-components (was useful for Siemens application, to be able to pinpoint location of an inconsistency in the axioms; it turned out useful for constraint-based deadlock checking as well)
=== Translation Technology ===
 
In order to provide a structured extensible code generation tool it was decided to use a multi-stage translation approach. The Event-B EMF model provided by the Event-B EMF Framework is extended to accommodate the tasking constructs as described above. The Tasking model is then translated to an intermediate model, the Common Language Model. The Common Language Meta-model is an abstraction of some useful generic programming constructs such as sequence, loop, branch and subroutine call/definition and so on. The translation of the Common Language Model to programme source code is then a relatively small step. The main translation activity takes place in the step between Tasking and Common Language models.
 
  
The decision was made to use Epsilon <ref name = "Epsilon"> </ref> to facilitate model to model translation for this stage. It was felt that an extensible, easily maintainable solution was required for this. Various model-to-model technologies (Java code, ATL, Epsilon) were appraised and it was judged that the Epsilon tool best matched our requirements. It proved to be a good choice initially for the specification of translations, especially in simpler areas of the project where the correspondence between models were simple. However the lack of debugging facilities, and productivity enhancements that are found in more mature tools, somewhat hindered rapid development as the project increased in complexity.
+
* Improved constraint solving, better use of Prolog's CLP(FD) constraint solver
  
=== Implementation - Source Code ===
+
* reification of constraints, detection of common sub-predicates, more precise information propagation for membership constraints, performance improvments in the typchecker and other parts of the kernel
Early in the current phase of work we identified the possibility of translating the Common Language Model to EMF models of programming languages such as Ada and C, in addition to producing textual source. While the EMF route still remains an option, it was decided that we would produce a PrettyPrinter for the Ada code. This allows a user to cut and paste the Ada source code from the PrettyPrinter window to an Ada editor, and was the optimal route to code for this phase of the code generation activity in DEPLOY.
 
  
=== Editing the Tasking Model ===
+
== Motivations ==
The editor for the Tasking Development is based on a EMF tree-editor. The tree editor provides a facility for adding the extensions to Event-B constructs. The readability of the editor is enhanced by a PrettyPrinter, which provides a textual version of the Tasking Development, which is easier to read. It is envisaged that the textual notation will be fully integrated as a Camille extension when the facility/resources become available.
 
  
== The Tool Deliverable ==
+
The above works were motivated mainly to support the following three industrial deployments:
The demonstrator tool was released on 30 November 2010, and is available as an update site, or bundled Rodin package from:
+
* Siemens: enable Siemens to use ProB in their SIL4 development chain, replacing Atelier B for data validation.
https://sourceforge.net/projects/codegenerationd/files
+
* 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
  
Sources are available from:
+
== Available Documentation ==
https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd
 
  
The tool is based on a build of Rodin 1.3.1 (not Rodin 2.0.0 due to dependency conflicts).
+
=== References ===
 
+
<references/>
* The Code Generation tool consists of,
 
** a Tasking Development Generator.
 
** a Tasking Development Editor (Based on an EMF Tree Editor).
 
** a translator, from Tasking Development to Common Language Model (IL1).
 
** a translator, from the Tasking Development to Event-B model of the implementation.
 
** a pretty-printer for the Tasking Development.
 
** a pretty-printer for Common Language Model, which generates Ada Source Code.
 
 
 
= Available Documentation =
 
== Technical Background ==
 
 
 
Much insight was gained during the work on code generation reported in the thesis ''Providing Concurrent Implementations for Event-B Developments'' <ref name="aeThesis">http://eprints.ecs.soton.ac.uk/20826/</ref>
 
 
 
Tooling issues were reported in a paper ''Tool Support for Event-B Code Generation''
 
<ref name = "toolSupport">http://eprints.ecs.soton.ac.uk/20824/</ref>
 
which was presented at ''Workshop on Tool Building in Formal Methods'',
 
http://abzconference.org/
 
 
 
There are technical notes available <ref name = "techNotes">http://wiki.event-b.org/images/Translation.pdf</ref>, that give more precise details of the approach and the mapping between Event-B and the common language meta-model, and its corresponding Event-B model.
 
 
 
== For Users ==
 
 
 
There is an overview at [[Tasking Event-B Overview for D32 ]]
 
 
 
There is a wiki page at [[Code_Generation_Activity]]
 
 
 
There is a tutorial at [[Code_Generation_Tutorial]]
 
  
= Planning =
+
== Planning ==
 
 
During 2011 we plan to develop the code generation tools further, taking on board any feedback from interested parties. The tool support should advance to the prototype stage, with improvements in the tool's usability in terms of features and user experience.
 
 
 
== References ==
 
 
 
<references/>
 
  
[[Category:D32 Deliverable]]
+
* Finish Validation Report
 +
* Write up Constraint-Based Deadlock Checking and integrate fully into Rodin Platform
 +
* Support mathematical extensions in ProB
 +
* Further improvements in the constraint-solving kernel of ProB; in particular for relations and operators. A Kodkod translator is being developed.

Revision as of 08:01, 30 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 [1], ProB itself has been further improved inspired by the application, resulting in new optimisations in the kernel (see below).

More details:

Multi-level Animation

Prior versions of ProB only supported the animation of a single refinement level. Abstract variables and predicates referring to them were ignored. In [4] and [5] we extended ProB in a way that all refinement levels of a model can be animated simultaneously.

First, this can give the user a deeper insight into how the model behaves and how the refinement levels are related to each other.

Second, we can now find errors in context of refinement. This include violation of the gluing invariant or not satisfiable witnesses for abstract variables. If such errors are present in a model, the corresponding proof obligation cannot be discharged. But without an animator it is not always easy to see for an user if this is caused by the complexity of the proof or by an error.

In the articles we summarized Event-B's current refinement methodology and showed for each proof obligation how the algorithm would find a counter-example. We presented empirical results and discussed how the algorithm can be combined with symmetry reduction.

Evaluation of the ProB Constraint Solver

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 (TLC was only able to solve the n-queens problem up until n=9, or n=14 when reformulating the problem as a model checking problem rather than a constraint-solving problem). In another small experiment, we checked whether two graphs with 9 nodes of out-degree exactly one are isomorphic by checking for the existence of a permutation which preserved the graph structure. TLC finds a permutation after 2 hours 6 minutes and 28 seconds; ProB 1.3.3 takes 0.01 seconds to find the same solution, while Alloy takes 0.11 seconds with SAT4J and 0.05 seconds with minisat. For some other examples (in particular time-tabling) involving operators such as the relational image, 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.

The basic idea is to generate deadlocks by solving a constraint consisting of the axioms Ax, the invariants Inv together with a constraint D specifying a deadlock. More formally, D is the negation of the disjunction of all the guards.

The following tool developments were required to meet the challenges raised by the industrial application:

  • generation of the deadlock freedom proof obligation by ProB (to avoid dependence on other plug-ins and being able to control whether theorems are to be used or not; currently they are not used)
  • implementation of a constraint-based deadlock checking algorithm:
    • with the possibility to specify an additional goal predicate 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
    • with semantic relevance filtering (to be able to filter out guards which are always false given the goal predicate).
    • with partitioning of the constraint predicate into components and optionally reordering according to usage (basic predicates which occur in most guards are listed first)
  • Improvements to ProB's constraint solving engine: (reification of constraints, detection of common sub-predicates, more precise information propagation for membership constraints, performance improvments in the typchecker and other parts of the kernel).

ProB has been applied successfully to two models of the adaptive cruise control by Bosch. The more complicated model is CrCtrl_Comb2Final. To give an idea, here are some statistics of the deadlock freedom proof obligation for CrCtrl_Comb2Final:

  • when printed in 9-point Courier ASCII the formula takes 32 A4 pages (the disjunction of the guards starts at page 6)
  • the model contains 59 events with 837 guards (19 of them disjunctions, some of which themselves nested)
  • Bosch are interested in deadlocks that are possible according to a flow specified using the flow plugin; these can be found with ProB by specifying a goal predicate (such as "Counter=10")
  • the proof obligation (as generated by the flow plugin) initially could not be loaded in Rodin due to "Java Heap Space Error".
  • Counter examples are found by ProB for various versions of the model in 9-24 seconds (including loading, typechecking and deadlock PO generation; the constraint solving time is 1.03 to 12.86 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: automatic detection of records described by a bijection between a cartesian product and a carrier set (these axioms can either be entered manually, such as in the Bosch models, or generated by the Records plug-in).
  • treatment of infinite sets, in particular complement sets such as INTEGER \ {x}. Such sets are being used in some of the Siemens models.
  • Partitioning of predicates into connected sub-components (was useful for Siemens application, to be able to pinpoint location of an inconsistency in the axioms; it turned out useful for constraint-based deadlock checking as well)
  • Improved constraint solving, better use of Prolog's CLP(FD) constraint solver
  • reification of constraints, detection of common sub-predicates, more precise information propagation for membership constraints, performance improvments in the typchecker and other parts of the kernel

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. 1.0 1.1 Michael Leuschel, Jérôme Falampin, Fabian Fritz and Daniel Plagge, Automated Property Verification for Large Scale B Models, FM'2009, LNCS 5850, Springer-Verlag, 2009
  2. Leuschel et al. FAC, special issue of FM'2009
  3. Leuschel et al. Draft of Validation Report
  4. Stefan Hallerstede, Michael Leuschel and Daniel Plagge, Refinement-Animation for Event-B - Towards a Method of Validation, ASM'2010, LNCS 5977, Springer-Verlag, 2010
  5. Stefan Hallerstede, Michael Leuschel and Daniel Plagge, Validation of Formal Models by Refinement Animation, to appear in Science of Computer Programming, Elsevier

Planning

  • Finish Validation Report
  • Write up Constraint-Based Deadlock Checking and integrate fully into Rodin Platform
  • Support mathematical extensions in ProB
  • Further improvements in the constraint-solving kernel of ProB; in particular for relations and operators. A Kodkod translator is being developed.