(2010):
IEEE Standard for Property Specification Language (PSL).
IEEE Std 1850-2010 (Revision of IEEE Std 1850-2005),
pp. 1–182,
doi:10.1109/IEEESTD.2010.5446004.
Jean-Raymond Abrial (2010):
Modeling in Event-B: System and Software Engineering.
Cambridge University Press,
doi:10.1017/S0956796812000081.
Rajeev Alur, Tomás Feder & Thomas A. Henzinger (1991):
The Benefits of Relaxing Punctuality.
In: Proceedings of the Tenth Annual ACM Symposium on Principles of Distributed Computing, Montreal, Quebec, Canada, August 19-21, 1991,
pp. 139–152,
doi:10.1145/112600.112613.
Maurice H ter Beek, Stefania Gnesi & Franco Mazzanti (2015):
From EU projects to a family of model checkers.
In: Software, Services, and Systems,
LNCS 8950.
Springer,
pp. 312–328,
doi:10.1007/978-3-319-15545-6_20.
Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri & Stefano Tonetta (2014):
The nuXmv Symbolic Model Checker.
In: CAV,
pp. 334–342,
doi:10.1007/978-3-319-08867-9_22.
INRIA CONVECS (2018):
CADP Home Page.
https://cadp.inria.fr.
Microsoft Corp. (2018):
The TLA Toolbox Home Page.
https://lamport.azurewebsites.net/tla/toolbox.html.
Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikučionis & Danny Bøgsted Poulsen (2015):
Uppaal SMC tutorial.
International Journal on Software Tools for Technology Transfer 17(4),
pp. 397–415,
doi:10.1007/s10009-014-0361-y.
Technische Universiteit Eindhoven (2018):
mCRL2 Home Page.
http://www.mcrl2.org/.
Alessio Ferrari, Giorgio O Spagnolo, Giacomo Martelli & Simone Menabeni (2014):
From commercial documents to system requirements: an approach for the engineering of novel CBTC solutions.
International Journal on Software Tools for Technology Transfer, STTT 16(6),
pp. 647–667,
doi:10.1007/s10009-013-0298-6.
Hubert Garavel, Frédéric Lang, Radu Mateescu & Wendelin Serwe (2013):
CADP 2011: a toolbox for the construction and analysis of distributed processes.
STTT 15(2),
pp. 89–107,
doi:10.1007/s10009-012-0244-z.
Hubert Garavel, Frédéric Lang & Wendelin Serwe (2017):
From LOTOS to LNT.
In: ModelEd, TestEd, TrustEd - Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday,
pp. 3–26,
doi:10.1007/978-3-319-68270-9_1.
Thomas Gibson-Robinson, Philip Armstrong, Alexandre Boulgakov & Andrew W Roscoe (2014):
FDR3— A modern refinement checker for CSP.
In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems.
Springer,
pp. 187–201,
doi:10.1007/978-3-642-54862-8_13.
Jan Friso Groote & Mohammad Reza Mousavi (2014):
Modeling and analysis of communicating systems.
MIT Press.
Heinrich-Heine-University (2018):
The ProB Animator and Model Checker.
https://www3.hhu.de/stups/prob/index.php/Main_Page.
Gerard Holzmann (2003):
The Spin Model Checker: Primer and Reference Manual.
Addison-Wesley Professional.
Kurt Jensen & Lars M Kristensen (2009):
Coloured Petri nets: modelling and validation of concurrent systems.
Springer Science & Business Media,
doi:10.1007/b95112.
Fondazione Bruno Kessler (2018):
The nuXmv model checker Home Page.
https://nuxmv.fbk.eu/.
Tuomas Kuismin & Keijo Heljanko (2013):
Increasing confidence in liveness model checking results with proofs.
In: Haifa Verification Conference.
Springer,
pp. 32–43,
doi:10.1007/978-3-319-03077-7_3.
ISTI-FMT Laboratory (2018):
KandISTI-UMC Home Page.
https://fmt.isti.cnr.it/umc.
Radu Mateescu & Damien Thivolle (2008):
A model checking language for concurrent value-passing systems.
In: International Symposium on Formal Methods.
Springer,
pp. 148–164,
doi:10.1007/978-3-540-68237-0_12.
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.
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.
Franco Mazzanti, Giorgio Oronzo Spagnolo, Simone Della Longa & Alessio Ferrari (2014):
Deadlock avoidance 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.
Franco Mazzanti, Giorgio Oronzo Spagnolo & Alessio Ferrari (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.
University of Oxford (2018):
FDR4 — The CSP Refinement Checker Home Page.
https://www.cs.ox.ac.uk/projects/fdr/.
Marjan Sirjani (2017):
Power is Overrated, Go for Friendliness! Expressiveness, Faithfulness and Usability in Modeling - The Actor Experience.
In: Principles of Modeling -Essays dedicated to Edward A. Lee on the Occasion of his 60th Birtday.
Available at http://rebeca-lang.org/assets/papers/2017/Friendliness.pdf.
spinroot (2018):
Verifying Multi-threaded Software with Spin.
http://spinroot.com/spin/whatispin.html.
Maurice H Ter Beek, Alessandro Fantechi, Stefania Gnesi & Franco Mazzanti (2011):
A state/event-based model-checking approach for the analysis of abstract system properties.
Science of Computer Programming 76(2),
pp. 119–135,
doi:10.1016/j.scico.2010.07.002.
CPN Tools (2018):
CPN Tools Home Page.
http://cpntools.org/.
Uppsala University and Aalborg University (2015):
UPPAAL Home Page.
http://www.uppaal.org/.
Kirsten Winter & Neil J Robinson (2003):
Modelling large railway interlockings and model checking small ones.
In: Proceedings of the 26th Australasian computer science conference-Volume 16.
Australian Computer Society, Inc.,
pp. 309–316.