D32 Model Animation

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 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 , 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

Rodin 10 Paper

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

Lukas Ladenberger's Master's thesis

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

Planning

• Finish Validation Report
• Write up Constraint-Based Deadlock Checking and integrate fully into Rodin Platform
• Support mathematical extensions in ProB