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 4: Line 4:
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 \cite{LeuschelEtAl:STS09} 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 \cite{LeuschelEtAl:STS09} 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
* 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.
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.
* 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.
* 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.
Line 11: Line 10:
  The validation also lead to the discovery of errors in the English version of the Atelier B reference manual.
  The validation also lead to the discovery of errors in the English version of the Atelier B reference manual.
   
   
Also, since  \cite{LeuschelEtAl:STS09}, ProB itself has been further improved
Also, since  \cite{LeuschelEtAl:STS09}, ProB itself has been further improved inspired by the application, resulting in new optimisations in the kernel (see below).
inspired by the application, resulting in new optimisations in the kernel
  (see below).




== multi-level animation ==
== Multi-level Animation ==
  (ABZ'2010 & SCP journal paper)
  (ABZ'2010 & SCP journal paper)


Line 29: Line 26:
Lukas Ladenberger's Master's thesis
Lukas Ladenberger's Master's thesis


== various other improvements, e.g., inspired by Siemens and Bosch Applications ==
== Various other improvements ==
 
mainly inspired by Siemens and Bosch Applications


Improved AVL algorithms, more operators
Improved AVL algorithms, more operators


  record support, treatment of infinite sets,
  record support, treatment of infinite sets,

Revision as of 08:52, 29 November 2010

Model Animation:

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 \cite{LeuschelEtAl:STS09} 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 \cite{LeuschelEtAl:STS09}, ProB itself has been further improved inspired by the application, resulting in new optimisations in the kernel (see below).


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,