D32 Model Animation

Overview

Most of the improvements made to model animation and model checking are related to the industrial deployment workpackages, in particular deployment within Siemens, SAP and Bosch.

Siemens Data Validation

STS are successfully using the B-method and have over the years acquired considerable expertise in its application. One aspect of the current development process, which is unfortunately still problematic, is the validation of properties on configuration parameters. These parameters, such as the rail network topology parameters, are only known at deployment time. Up to now, Siemens was using a custom version of Atelier B to check properties on these parameters. However, the data parameters are nowadays becoming so large (relations with thousands of tuples) that Atelier B quite often runs out of memory, even with the dedicated proof rules and with maximum memory allocated. In some of the bigger and more recent models, just substituting values for variables fails with out-of-memory conditions. The alternative consisting in the manual checking of these properties (e.g., by creating huge spreadsheets on paper for the compatibility constraints of all possible itineraries), is very costly and arguably less reliable than automated checking.

Previously, we had established the feasibility of using the ProB tool on a case study (metro of San Juan) to validate runtime data for the industrial B models, replacing a month worth of effort by a few minutes of calculation. The next step was to apply ProB to ongoing developments of Siemens and to allow Siemens to use ProB in their SIL4 development chain.

The most important contributions 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ã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 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.
• Reports about the ongoing validation process of ProB, which is required by Siemens to allow them to use ProB instead of the existing method. The validation also lead to the discovery of errors in the English version of the Atelier B reference manual.

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

More details about this work can be found in the following works: and .

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. To support validation of Event-B models such as the ones generated by Bosch, this short coming had to be addressed. In and 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.

Constraint-Based Deadlock Checking

Ensuring the absence of deadlocks is important for certain applications, in particular for Bosch's 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.

More details can be found in and

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.

Various other improvements

Mainly inspired by the Siemens and Bosch applications mentioned above, various improvements to the ProB kernel were undertaken.

• Improved algorithms for large sets and relations (such computing the domain of a relation), optimised support for more B operators on relations, functions, and sequences.

• 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 of the Cruise Control, or generated automatically by the Records plug-in. In both cases, ProB detects that a record is being used, and sets the carrier set to the cartesian product and sets the bijection to the identity function.

• Detection and treatment of certain infinite sets, in particular complement sets such as INTEGER \ {x}. Such sets are being used in some of the Siemens models. Similarly, infinite identity functions are also never expanded and always treated symbolically.

• 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 in particular:
  • better use of Prolog's CLP(FD) constraint solver for arithmetic constraints as well as for elements of carrier sets. For example, x:{a,b,d} will attach a finite-domain constraint to x, even without enumeration.
  • improved boolean constraint solver; deals with well-definedness and propagates known boolean values through complicated predicates. Can also solve SAT problems expressed in B (up to around 600 variables and 2000 clauses).
  • Reification of constraints inside the boolean constraint solver. In particular, given x:1..10, the ProB boolean constraint solver will know that, e.g., x:{12,13,14} must be false.
  • detection of common sub-predicates inside larger formulas. This is to improve performance and overcome possible precision problems of the constraint solver. The main motivation here is deadlock checking (where the same predicate often appear multiple times, sometimes in negated form).

• General performance improvments, such as in the typchecker and other parts of the kernel when loading larger B models.

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 (see above).
• Bosch: provide animation and constraint-based deadlock detection for the Cruise Control. Indeed, proving absence of deadlocks is important to Bosch, as it means that the modelers have thought of every possible scenario. Currently, the proof obligation is so big (see above) that it is difficult to apply the provers and the feedback obtained during a failed proof attempt is not very useful. Using ProB to find concrete deadlock counterexample helps Bosch to find scenarios they have not yet thought about, and enables them to adapt the model. Once all cases have been covered, the proof of deadlock freedom can be done with Rodin's provers (at least that was the case for the smaller of the two models; the bigger one is still contains deadlocks and is being improved).
• SAP: provide a way to generate test cases using constraint-based animation; for more details see the description of the Model-based testing work.

Choices / Decisions

For constraint-based deadlock checking we had the choice of either generating the deadlock freedom proof obligation with ProB or using ProB as a disprover on a generated proof obligation. Currently, the core of Rodin does not generate the deadlock freedom proof obligation. The flow plugin can be used to generate deadlock freedom proof obligations. The advantage, however, of generating them within ProB are the following:

• ProB knows which parts of the axioms are theorems (and can thus be ignored; they are often added for simplifying proof but can make constraint solving more difficult)
• the techniques can also be applied to classical B

For record detection we decided not to use any potential "hints" provided by the records plugin, but infer the information from the axioms. In this way, the improvement can also be applied to records generated manually (as was the case in the Bosch case study) or in a classical B setting.

Available Documentation

See the references below.

The validation document is being prepared and will probably be made available in spring 2011.

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.