@article(psl,
 year         = {2010},
 title        = {IEEE Standard for Property Specification Language (PSL)},
 journal      = {IEEE Std 1850-2010 (Revision of IEEE Std 1850-2005)},
 pages        = {1--182},
 doi          = {10.1109/IEEESTD.2010.5446004},
)
@book(eventb,
 author       = {Jean-Raymond Abrial},
 year         = {2010},
 title        = {{Modeling in Event-B: System and Software Engineering}},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/S0956796812000081},
)
@inproceedings(mitl,
 author       = {Rajeev Alur and Tom{\'{a}}s Feder and Thomas A. Henzinger},
 year         = {1991},
 title        = {The Benefits of Relaxing Punctuality},
 booktitle    = {Proceedings of the Tenth Annual {ACM} Symposium on Principles of Distributed Computing, Montreal, Quebec, Canada, August 19-21, 1991},
 pages        = {139--152},
 doi          = {10.1145/112600.112613},
)
@incollection(kandi,
 author       = {Maurice H ter Beek and Stefania Gnesi and Franco Mazzanti},
 year         = {2015},
 title        = {{From EU projects to a family of model checkers}},
 booktitle    = {Software, Services, and Systems},
 series       = {LNCS},
 volume       = {8950},
 publisher    = {Springer},
 pages        = {312--328},
 doi          = {10.1007/978-3-319-15545-6_20},
)
@inproceedings(nuxmv,
 author       = {Roberto Cavada and Alessandro Cimatti and Michele Dorigatti and Alberto Griggio and Alessandro Mariotti and Andrea Micheli and Sergio Mover and Marco Roveri and Stefano Tonetta},
 year         = {2014},
 title        = {The nuXmv Symbolic Model Checker},
 booktitle    = {CAV},
 pages        = {334--342},
 doi          = {10.1007/978-3-319-08867-9_22},
)
@misc(cadpsite,
 author       = {INRIA CONVECS},
 year         = {2018},
 title        = {{CADP Home Page}},
 howpublished = {https://cadp.inria.fr},
)
@misc(tlasite,
 author       = {Microsoft Corp.},
 year         = {2018},
 title        = {{The TLA Toolbox Home Page}},
 howpublished = {https://lamport.azurewebsites.net/tla/toolbox.html},
)
@article(uppaalsmc,
 author       = {Alexandre David and Kim G. Larsen and Axel Legay and Miku{\v{c}}ionis, Marius and Danny B{\o}gsted Poulsen},
 year         = {2015},
 title        = {Uppaal SMC tutorial},
 journal      = {International Journal on Software Tools for Technology Transfer},
 volume       = {17},
 number       = {4},
 pages        = {397--415},
 doi          = {10.1007/s10009-014-0361-y},
)
@misc(mcrl2site,
 author       = {Technische Universiteit Eindhoven},
 year         = {2018},
 title        = {{mCRL2 Home Page}},
 howpublished = {http://www.mcrl2.org/},
)
@article(ferrari2014commercial,
 author       = {Alessio Ferrari and Giorgio O Spagnolo and Giacomo Martelli and Simone Menabeni},
 year         = {2014},
 title        = {From commercial documents to system requirements: an approach for the engineering of novel CBTC solutions},
 journal      = {International Journal on Software Tools for Technology Transfer, STTT},
 volume       = {16},
 number       = {6},
 pages        = {647--667},
 doi          = {10.1007/s10009-013-0298-6},
)
@article(cadp,
 author       = {Hubert Garavel and Fr{\'{e}}d{\'{e}}ric Lang and Radu Mateescu and Wendelin Serwe},
 year         = {2013},
 title        = {{CADP} 2011: a toolbox for the construction and analysis of distributed processes},
 journal      = {{STTT}},
 volume       = {15},
 number       = {2},
 pages        = {89--107},
 doi          = {10.1007/s10009-012-0244-z},
)
@inproceedings(lnt,
 author       = {Hubert Garavel and Fr{\'{e}}d{\'{e}}ric Lang and Wendelin Serwe},
 year         = {2017},
 title        = {From {LOTOS} to {LNT}},
 booktitle    = {ModelEd, TestEd, TrustEd - Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday},
 pages        = {3--26},
 doi          = {10.1007/978-3-319-68270-9_1},
)
@inproceedings(fdr3,
 author       = {Gibson-Robinson, Thomas and Philip Armstrong and Alexandre Boulgakov and Andrew W Roscoe},
 year         = {2014},
 title        = {FDR3— A modern refinement checker for CSP},
 booktitle    = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
 organization = {Springer},
 pages        = {187--201},
 doi          = {10.1007/978-3-642-54862-8_13},
)
@book(mcrl2,
 author       = {Jan Friso Groote and Mohammad Reza Mousavi},
 year         = {2014},
 title        = {Modeling and analysis of communicating systems},
 publisher    = {MIT Press},
)
@misc(probsite,
 author       = {Heinrich-Heine-University},
 year         = {2018},
 title        = {{The ProB Animator and Model Checker}},
 howpublished = {https://www3.hhu.de/stups/prob/index.php/Main_Page},
)
@book(spin,
 author       = {Gerard Holzmann},
 year         = {2003},
 title        = {{The Spin Model Checker: Primer and Reference Manual}},
 publisher    = {Addison-Wesley Professional},
)
@book(cpn,
 author       = {Kurt Jensen and Lars M Kristensen},
 year         = {2009},
 title        = {Coloured Petri nets: modelling and validation of concurrent systems},
 publisher    = {Springer Science \& Business Media},
 doi          = {10.1007/b95112},
)
@misc(smvsite,
 author       = {Fondazione Bruno Kessler},
 year         = {2018},
 title        = {{The nuXmv model checker Home Page}},
 howpublished = {https://nuxmv.fbk.eu/},
)
@inproceedings(kuismin,
 author       = {Tuomas Kuismin and Keijo Heljanko},
 year         = {2013},
 title        = {Increasing confidence in liveness model checking results with proofs},
 booktitle    = {Haifa Verification Conference},
 organization = {Springer},
 pages        = {32--43},
 doi          = {10.1007/978-3-319-03077-7_3},
)
@misc(umcsite,
 author       = {ISTI-FMT Laboratory},
 year         = {2018},
 title        = {{KandISTI-UMC Home Page}},
 howpublished = {https://fmt.isti.cnr.it/umc},
)
@misc(tla,
 author       = {Leslie Lamport},
 year         = {2002},
 title        = {Specifying Systems},
 howpublished = {https://lamport.azurewebsites.net/tla/book-02-08-08.pdf},
)
@inproceedings(mcl,
 author       = {Radu Mateescu and Damien Thivolle},
 year         = {2008},
 title        = {A model checking language for concurrent value-passing systems},
 booktitle    = {International Symposium on Formal Methods},
 organization = {Springer},
 pages        = {148--164},
 doi          = {10.1007/978-3-540-68237-0_12},
)
@inproceedings(isola,
 author       = {Franco Mazzanti and Alessio Ferrari and Giorgio Oronzo Spagnolo},
 year         = {2014},
 title        = {{Experiments in Formal Modelling of a Deadlock Avoidance Algorithm for a CBTC System}},
 booktitle    = {International Symposium on Leveraging Applications of Formal Methods - ISoLA 2016, Volune Part II},
 series       = {LNCS},
 volume       = {9953},
 publisher    = {Springer},
 pages        = {297--314},
 doi          = {10.1007/978-3-319-47169-3_22},
)
@article(mazzanti2018towards,
 author       = {Franco Mazzanti and Alessio Ferrari and Giorgio Oronzo Spagnolo},
 year         = {2018},
 title        = {Towards Formal Methods Diversity in Railways: an Experience Report with Seven Frameworks},
 journal      = {International Journal on Software Tools for Technology Transfer, STTT},
 volume       = {20},
 number       = {3},
 doi          = {10.1007/s10009-018-0488-3},
)
@inproceedings(mazzanti2014deadlock,
 author       = {Franco Mazzanti and Giorgio Oronzo Spagnolo and Della Longa, Simone and Alessio Ferrari},
 year         = {2014},
 title        = {Deadlock avoidance in train scheduling: a model checking approach},
 booktitle    = {International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2014},
 series       = {LNCS},
 volume       = {8718},
 organization = {Springer},
 pages        = {109--123},
 doi          = {10.1007/978-3-319-10702-8_8},
)
@inproceedings(nfm14,
 author       = {Franco Mazzanti and Giorgio Oronzo Spagnolo and Alessio Ferrari},
 year         = {2014},
 title        = {Designing a deadlock-free train scheduler: A model checking approach},
 booktitle    = {NASA Formal Methods Symposium},
 series       = {LNCS},
 volume       = {8430},
 organization = {Springer},
 pages        = {264--269},
 doi          = {10.1007/978-3-319-06200-6_22},
)
@misc(fdrsite,
 author       = {University of Oxford},
 year         = {2018},
 title        = {{FDR4 — The CSP Refinement Checker Home Page}},
 howpublished = {https://www.cs.ox.ac.uk/projects/fdr/},
)
@inproceedings(rebeca,
 author       = {Marjan Sirjani},
 year         = {2017},
 title        = {{Power is Overrated, Go for Friendliness! Expressiveness, Faithfulness and Usability in Modeling - The Actor Experience}},
 booktitle    = {Principles of Modeling -Essays dedicated to Edward A. Lee on the Occasion of his 60th Birtday},
 url          = {http://rebeca-lang.org/assets/papers/2017/Friendliness.pdf},
)
@misc(spinsite,
 author       = {spinroot},
 year         = {2018},
 title        = {{Verifying Multi-threaded Software with Spin}},
 howpublished = {http://spinroot.com/spin/whatispin.html},
)
@article(ter2011state,
 author       = {Ter Beek, Maurice H and Alessandro Fantechi and Stefania Gnesi and Franco Mazzanti},
 year         = {2011},
 title        = {A state/event-based model-checking approach for the analysis of abstract system properties},
 journal      = {Science of Computer Programming},
 volume       = {76},
 number       = {2},
 pages        = {119--135},
 doi          = {10.1016/j.scico.2010.07.002},
)
@misc(cpnsite,
 author       = {CPN Tools},
 year         = {2018},
 title        = {{CPN Tools Home Page}},
 howpublished = {http://cpntools.org/},
)
@misc(uppaalsite,
 author       = {{Uppsala University and Aalborg University}},
 year         = {2015},
 title        = {{UPPAAL Home Page}},
 howpublished = {http://www.uppaal.org/},
)
@inproceedings(winter2003modelling,
 author       = {Kirsten Winter and Neil J Robinson},
 year         = {2003},
 title        = {Modelling large railway interlockings and model checking small ones},
 booktitle    = {Proceedings of the 26th Australasian computer science conference-Volume 16},
 organization = {Australian Computer Society, Inc.},
 pages        = {309--316},
)