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

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Jens
 
imported>Leuschel
 
Line 1: Line 1:
= Overview =
+
= Model Animation =  
This part of the deliverable describes improvement of the ProB animation and model checking plugin.
 
  
The improvements and development of ProB were mainly carried out by University of Düsseldorf, with some support by the University of Southampton.
+
== Overview ==
Furthermore, the work was driven by requirements of Siemens and SAP; some tool development was also undertaken by SAP.
+
=== 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.
  
New features:
+
  The validation also lead to the discovery of errors in the English version of the Atelier B reference manual.
  * Multi-level animation and validation
+
   
* B-Motion Studio
+
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).
  * Disprover Support
 
  * first steps towards test-case generation
 
  
Improvements:
+
More details:
* Scalability improvements driven by Siemens and SAP applications
+
* <ref>Leuschel et al. FAC, special issue of FM'2009</ref>
* Using proof information to improve model checking
+
* <ref>Leuschel et al. Draft of Validation Report</ref>
  
Other works:
+
=== Multi-level Animation ===
* First steps towards validation of ProB for usage by Siemens in SIL-4 chain
+
  (ABZ'2010 & SCP journal paper)
  * Evaluation against SAT/SMT/BDD-based approaches
 
  
= Motivations =
+
=== Improvements to the ProB Constraint solver and empirical evaluation ===
This paragraph shall express the motivation for each tool extension and improvement. More precisely, it shall first indicate the state before the work, the encountered difficulties, and shall highlight the requirements (eg. those of industrial partners). Then, it shall summarize how these requirements are addressed and what are the main benefits.
+
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.
  
=== Multi-level Animation and Validation ===
+
Idea: solve constraints of axioms, invariant together with a constraint specifying a deadlock.
  
Thus far ProB only alllowed single-level animation, i.e., the animator would animate a single refinement level in isolation.
+
Required Developments:
This meant that ProB was not able to detect a large class of potential errors in the model:
+
* 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).
* a broken gluing invariant
+
* 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)
* an invalid witness
 
* violation of guard strengthening
 
* violation of variant decrease (resp. decrease or stability) for convergent (resp. anticipated) events
 
  
The new validation algorithm now can animate a range of refinements together. The user can decide which levels are to be animated together.
+
Success: Model 1 and Model 2: CrCtrl_Comb2Final;
As such, all of the above errors can now be detected by ProB.
+
relevance of Counter=10 due to flow
User experience is also improved, as he or she can inspect also the abstract variables.
 
The new algorithm has been sucessfully applied to various case studies, and thus far up to 14 levels have been animated concurrently without problem.
 
  
 +
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.
  
=== B-Motion Studio ===
+
=== BMotionStudio for Industrial Models ===
  
It is often very important to be able to show a formal model to a domain expert or manager, not versed in formal methods.
+
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.
For example, only a domain expert will be able to detect certain mistakes in the formal model.
 
To enable to easily and quickly build graphical visualisations of Rodin models, we have developed B-Motion Studio.
 
B-Motion Studio comes with a graphical editor to arrange graphical components and link them with the formal model.
 
No new programming language has to be learned: the linking is described in B itself.
 
To run a graphical visualisation, the ProB animator is used.
 
  
=== Test-Case Generation ===
+
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:
  
During deployment in the SAP workpackage it became clear that test-case generation from the Event-B models
+
* 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.
is required for success.
+
* 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.
In this task, we have developed a first algorithm for test-case generation, which ensures complete transition coverage of a high-level model, and translates the test-cases into traces of a refined model, so that the tests can be run on the "real" system.
+
* 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.
Optimisations, to reduce the length and number of test cases, as well as to minimise race conditions, have been implemented.
 
  
=== Scalability, Application by Siemens and Validation ===
+
=== Various other improvements ===
We tackled  a  case study in WP2, which centres on the San Juan metro system installed by Siemens. The control software was developed and formally proven with B. However, the development contains certain assumptions about the actual rail network topology which have to be validated separately in order to ensure safe operation. For this task, Siemens has developed custom proof rules for AtelierB. AtelierB, however, was unable to deal with about 80 properties of the deployment (running out of memory). These properties thus had to be validated by hand at great expense (and they need to be revalidated whenever the rail network infrastructure changes). I
 
  
The motivation then was to try and use ProB for this task.
+
mainly inspired by Siemens and Bosch Applications
This required a considerable amount of work on improving the scalability of the ProB kernel, to be able to deal with large sets and relations.
 
The ProB parser and type checker also had to be re-developed to be able to deal with large industrial specifications.
 
  
The case study was a succcess:ProB was able to validate all of the about 300 properties of the San Juan deployment, detecting exactly the same faults automatically in around 17 minutes that were manually uncovered in about one man-month.
+
Improved AVL algorithms, more operators
  
This leads to the next task: the issue of validating ProB, so that it can be integrated into the SIL4 development chain at Siemens
+
record support, treatment of infinite sets,
  
=== Proof Directed Model Checking ===
+
== Motivations ==
  
In order to improve the performance and scalability of animation and model checking with ProB, we want to make use of the proof information available in an integrated platform such as Rodin.
+
The above works were motivated mainly to support the following three industrial deployments:
In particular, we can use the information about which POs have already been discharged to simplify the task of the model checker and to guide the order in which it evaluates states.
+
* 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
  
Our first implementation has shown significant reduction of the model checking effort for industrial applications. It uses proof information obtained from Rodin to remove invariants that are proven to hold. Actually, if unproven(e) is the unproven part of the invariant for event e, and a state is reachable via events e and f, we only need to check the intersection of unproven(e) and unproven(f) (see [http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=253 Jens Bendisposto, Michael Leuschel. Proof Assisted Model Checking for B. ICFEM 2009.]).
+
== Available Documentation ==
  
=== SAT/SMT/Kodkod ===
+
=== References ===
 +
<references/>
  
In this subtask we investigate alternate approaches for validating high-level B models using techniques and tools based on BDDs, SAT-solving and SMT-solving.
+
== Planning ==
The overall motivation is to improve the scalability of the animator and model checker.
 
  
=== Disprover ===
+
* Finish Validation Report
 
+
* Write up Constraint-Based Deadlock Checking and integrate fully into Rodin Platform
In order to help the user, we wanted to make it possible to apply ProB to individual proof obligations.
+
* Support mathematical extensions in ProB
In some cases, this enables proving a sequent by exhaustive case analysis.
 
Also, if ProB finds a counter example, the user gets important feedback: the proof obligation cannot be discharged, along with a reason why.
 
 
 
= Choices / Decisions =
 
 
 
One important choice for ProB is to use the same constraint solving kernel and interpreter for B, Event-B and Z. This decision, allows us to maintain a tool capable of animating and model checking these three formalisms. It also gives us a much wider range of test cases. For example, most of the regression tests of ProB come in the form of B machines (Rodin archives are much "cumbersome" as a basis of regression tests: they need to be upgraded and imported into workspaces).
 
This choice also enabled us to achieve the successful deployment of ProB in WP2, where the use of classical B was mandatory.
 
 
 
Concerning the inclusion of SMT, SAT, BDD techniques into ProB, no decision has been taken yet. We are still investigating the possibilities.
 
 
 
Concerning B-Motion Studio, we decided not to use Flash (we had an earlier prototype using Flash). We wanted a tool that can be easily used and installed into Rodin. We also wanted a tool that can be used without having to learn a new programming language (Action Script).
 
 
 
= Available Documentation =
 
 
 
== User Manual ==
 
 
 
[http://asap0.cs.uni-duesseldorf.de/trac/prob/wiki/ ProB User Manual]
 
 
 
== Published Papers ==
 
 
 
Below is a list of published papers, along with an abstract.
 
 
 
=== Improved Kernel to deal with large sets and relations ===
 
In this part we describe the successful application of the ProB validation tool on an industrial case study. The case study centres on the San Juan metro system installed by Siemens. The control software was developed and formally proven with B. However, the development contains certain assumptions about the actual rail network topology which have to be validated separately in order to ensure safe operation. For this task, Siemens has developed custom proof rules for AtelierB. AtelierB, however, was unable to deal with about 80 properties of the deployment (running out of memory). These properties thus had to be validated by hand at great expense (and they need to be revalidated whenever the rail network infrastructure changes). In this paper we show how we were able to use ProB to validate all of the about 300 properties of the San Juan deployment, detecting exactly the same faults automatically in around 17 minutes that were manually uncovered in about one man-month. This achievement required the extension of the ProB kernel for large sets as well as an improved constraint propagation phase. We also outline some of the effort and features that were required in moving from a tool capable of dealing with medium-sized examples towards a tool able to deal with actual industrial specifications. Notably, a new parser and type checker had to be developed. We also touch upon the issue of validating ProB, so that it can be integrated into the SIL4 development chain at Siemens
 
 
 
 
 
[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=248 Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge. Automated Property Verification for Large Scale B Models, FM'2009.]
 
 
 
=== Multi-Level Animation and Validation ===
 
We provide a detailed description of refinement in Event-B, both as a contribution in itself and as a foundation for the approach to simultaneous animation of multiple levels of refinement that we propose.
 
We present an algorithm for simultaneous multi-level animation of refinement, and show how it can be used to detect a variety of errors that occur frequently when using refinement.
 
The algorithm has been implemented in ProB and we applied it to several case studies, showing that multi-level animation is tractable also on larger models.
 
 
 
[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=256 Stefan Hallerstede, Michael Leuschel, Daniel Plagge. Refinement-Animation for Event-B --- Towards a Method of Validation. ABZ'2010 ]
 
 
 
See also [http://www.springerlink.com/content/282p2316x7165588/ Stefan Hallerstede, Michael Leuschel. How to Explain Mistakes. TFM'09.]
 
 
 
=== Test-Case Generation ===
 
Choreography models describe the communication protocols between services. Testing of service choreographies is an important task for the quality assurance of service-based systems as used e.g. in the context of service-oriented architectures (SOA). The formal modeling of service choreographies enables a model-based integration testing (MBIT) approach. We present MBIT methods for our service choreography modeling approach called Message Choreography Models (MCM). For the model-based testing of service choreographies, MCMs are translated into Event-B models and used as input for our test generator which uses the model checker ProB.
 
 
 
[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=252 Sebastian Wieczorek, Vitaly Kozyura, Andreas Roth, Michael Leuschel, Jens Bendisposto, Daniel Plagge, Ina Schieferdecker. Applying Model Checking to Generate Model-based Integration Tests from Choreography Models. TESTCOM/FATES 2009.]
 
 
 
 
 
=== Proof-Directed Model Checking ===
 
With the aid of the ProB Plugin, the Rodin Platform provides an integrated environment for editing, proving, animating and model checking Event-B models. This is of considerable benefit to the modeler, as it allows him to switch between the various tools to validate, debug and improve his or her models. The crucial idea of this paper is that the integrated platform also provides benefits to the tool developer, i.e., it allows easy access to information from other tools. Indeed, there has been considerable interest in combining model checking, proving and testing. In previous work we have already shown how a model checker can be used to complement the Event-B proving environment, by acting as a disprover. In this paper we show how the prover can help improve the efficiency of the animator and model checker.
 
 
 
[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=253 Jens Bendisposto, Michael Leuschel. Proof Assisted Model Checking for B. ICFEM 2009.]
 
 
 
=== Debugging Tricky Proof Obligations with the ProB Disprover ===
 
While a large number of proof obligations can be discharged automatically by tools such as the RODIN platform, a considerable number still have to be proven interactively.  In this paper, we we describe a disprover plugin for RODIN that utilizes ProB to automatically find counterexamples for a given problematic proof obligation.  In case the disprover finds a counterexample, the user can directly investigate the source of teh problem, as pinpointed by the counterexample.  We also discuss under which circumstances our plug-in can be used as a prover, i.e., when the absence of a counterexample
 
actually is a proof of the proof obligation.
 
 
 
[http://www.stups.uni-duesseldorf.de/publications_detail.php?id=219 Olivier Ligot, Jens Bendisposto, Michael Leuschel. Debugging Event-B Models using the ProB Disprover Plug-in.  AFADL 2007.]
 
 
 
=== Inspection of Alternate Approaches ===
 
 
 
ProB is a model checker for high-level B and Event-B models based on constraint-solving. In this paper we investigate alternate approaches for validating high-level B models using techniques and tools based on using BDDs, SAT-solving and SMT-solving. In particular, we examine whether ProB can be complemented or even supplanted by using one of the tools BDDBDDB, Kodkod or SAL.
 
 
 
[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=249 Daniel Plagge, Michael Leuschel, Ilya Lopatkin, Alexander Romanovsk. SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook. AFM'09.]
 
 
 
=== Validation of ProB ===
 
 
 
Symmetry reduction is a model checking technique that can help alleviate the problem of state space explosion, by preventing redundant state space exploration. In previous work, we have developed three effective approaches to symmetry reduction for B that have been implemented into the ProB model checker, and we have proved the soundness of our state symmetries. However, it is also important to show our techniques are sound with respect to standard model checking, at the algorithmic level. In this paper, we present a retrospective B development that addresses this issue through a series of B refinements. This work also demonstrates the valuable insights into a system that can be gained through formal modelling.
 
 
 
[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=257 Edd Turner, Michael Butler, Michael Leuschel. A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking. ABZ'2010.]
 
 
 
 
 
=== B-Motion Studio ===
 
 
 
B-Motion Studio provides a way to quickly generate domain specific visualisations for a formal model, enabling domain experts and managers to understand and validate the model. We also believe that our tool will be of use when teaching formal methods, both during lectures as a way to motivate students to write their own formal models.
 
 
 
[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=258 Lukas Ladenberger, Jens Bendisposto, Michael Leuschel. Visualising Event-B models with B-Motion Studio. FMICS'2009.]
 
 
 
= Planning =
 
This paragraph shall give a timeline and current status (as of 29 Jan 2010).
 
 
 
=== Model-based Testing ===
 
 
 
* Directed Model Checking to achieve coverage (Deploy extension; Flow Graphs)
 
* Integrate Algorithm into Rodin
 
* Make Algorithm more generic
 
* Top-down multi-level animation
 
* Move from prototype to real product
 
 
 
=== B-Motion Studio ===
 
 
 
* Experiment with existing Flash animation and B model of ClearSy
 
* Improve usability, more widgets
 
 
 
=== Validation of ProB ===
 
 
 
* Test coverage analysis for Prolog code
 
* Validation Document to be delivered to Siemens
 
 
 
=== Scalability ===
 
 
 
* More experiments with SAT, SMT, BDD techniques
 
 
 
* Integration of Kodkod into ProB for solving complicated predicates over first order relations and simple sets
 
 
 
* Adaption of ProB for the upcoming mathematical extensions. Indeed, for the moment the Rodin user is often required to model basic datatypes (records, sequences,...) or operators (transitive closure) herself. This is a big challenge to the animator, which does not know that the constants and variables of the machine (e.g., injective functions) are "simply" meant to model quite basic datatypes. With the introduction of mathematical extensions for records, transitive closure, ... this hurdle will be overcome.
 
 
 
=== Usability ===
 
* Feedback errors found by ProB into the PO view (as red icons)
 
* Improve Disprover, detect when it is a decision procedure
 
* Further improvments to GUI: 2-D Viewer, better multi-level animation view
 

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