In this directory are contained the models cited in the MARS 2018 paper:

"Ten Diverse Formal Models for a CBTC Automatic Train Supervision System"
by Franco Mazzzanti and Alessio Ferrari,

All the models are formalizations of the Train Deadlock Avoidance system
initially described in:

  Franco Mazzanti,Giorgio Oronzo Spagnolo, AlessioFerrari (2014):
  Designing a deadlock-free train scheduler: A model checking approach. 
  In: NASA Formal Methods Symposium, 
  LNCS 8430, Springer, pp. 264–269, 
  doi:10.1007/978-3-319-06200-6 22.

and later extended in:

Franco Mazzanti,Giorgio Oronzo Spagnolo,Simone Della Longa, AlessioFerrari(2014):
  Deadlockavoidance in train scheduling: a model checking approach. 
  In: International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2014, 
  LNCS 8718, Springer, pp. 109–123, 
 doi:10.1007/978-3-319- 10702-8 8.
 
 
An initial comparison of the various translations for six different formal varification
framworks has been initially presened in:
  
  Franco Mazzanti,Alessio Ferrari, Giorgio Oronzo Spagnolo(2014):
  "Experiments in Formal Modelling of a Deadlock Avoidance Algorithm for a CBTC System"
  In: International Symposium on Leveraging Applications of Formal Methods ISoLA 2016, 
  Volune Part II, LNCS 9953, Springer, pp. 297–314, 
  doi:10.1007/978-3- 319-47169-3 22.

The initial comparison has been later extended in the following paper, where the focus 
was centered of the verification capabilities of the seven considered frameworks.

Franco Mazzanti, Alessio Ferrari & Giorgio Oronzo Spagnolo (2018): 
  Towards Formal Methods Diversity in Railways: an Experience Report with Seven Frameworks.
  International Journal on Software Tools for Technology Transfer, STTT 20(3),
  doi:10.1007/s10009-018-0488-3.

-----------------

In the MARS 2018 paper, we are now considering the modelling in ten different 
formal languages, keeping the focus more on the linguistic issues rather then the
verfication issues.

A public read-only version of the STTT paper can be accessed through the 
Springer Nature’s link: http://rdcu.be/ID78

Public version of the other mentioned papers can be accessed through the author home site:
http://fmt.isti.cnr.it/~mazzanti/publications

-----------------