D32 Model Animation

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.

\item 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

= Constraint-Based Deadlock Checking

= record support, treatment of infinite sets, application to Bosch models

= BMotionStudio for Industrial Models

= various other improvements, e.g., inspired by Siemens application

Improved AVL algorithms, more operators, improved CLP(FD) support