D32 Model Animation: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Leuschel No edit summary |
imported>Leuschel No edit summary |
||
| Line 1: | Line 1: | ||
= Model Animation = | = Model Animation = | ||
== Siemens Application== | == Overview == | ||
=== Siemens Application=== | |||
The most important additions of the last 12 months are: | 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. | * 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. | ||
| Line 16: | Line 17: | ||
* <ref>Leuschel et al. Draft of Validation Report</ref> | * <ref>Leuschel et al. Draft of Validation Report</ref> | ||
== Multi-level Animation == | === Multi-level Animation === | ||
(ABZ'2010 & SCP journal paper) | (ABZ'2010 & SCP journal paper) | ||
== Improvements to the ProB Constraint solver and empirical evaluation == | === Improvements to the ProB Constraint solver and empirical evaluation === | ||
Rodin 10 Paper | Rodin 10 Paper | ||
== Constraint-Based Deadlock Checking == | === Constraint-Based Deadlock Checking === | ||
== BMotionStudio for Industrial Models == | === BMotionStudio for Industrial Models === | ||
Lukas Ladenberger's Master's thesis | Lukas Ladenberger's Master's thesis | ||
== Various other improvements == | === Various other improvements === | ||
mainly inspired by Siemens and Bosch Applications | mainly inspired by Siemens and Bosch Applications | ||
| Line 37: | Line 38: | ||
record support, treatment of infinite sets, | 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 === | ||
<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:00, 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
Rodin 10 Paper
Constraint-Based Deadlock Checking
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
Available Documentation
References
Planning
- Finish Validation Report
- Write up Constraint-Based Deadlock Checking and integrate fully into Rodin Platform
- Support mathematical extensions in ProB
