References

  1. (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.
  2. Jean-Raymond Abrial (2010): Modeling in Event-B: System and Software Engineering. Cambridge University Press, doi:10.1017/S0956796812000081.
  3. 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.
  4. 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.
  5. 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.
  6. INRIA CONVECS (2018): CADP Home Page. https://cadp.inria.fr.
  7. Microsoft Corp. (2018): The TLA Toolbox Home Page. https://lamport.azurewebsites.net/tla/toolbox.html.
  8. 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.
  9. Technische Universiteit Eindhoven (2018): mCRL2 Home Page. http://www.mcrl2.org/.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. Jan Friso Groote & Mohammad Reza Mousavi (2014): Modeling and analysis of communicating systems. MIT Press.
  15. Heinrich-Heine-University (2018): The ProB Animator and Model Checker. https://www3.hhu.de/stups/prob/index.php/Main_Page.
  16. Gerard Holzmann (2003): The Spin Model Checker: Primer and Reference Manual. Addison-Wesley Professional.
  17. Kurt Jensen & Lars M Kristensen (2009): Coloured Petri nets: modelling and validation of concurrent systems. Springer Science & Business Media, doi:10.1007/b95112.
  18. Fondazione Bruno Kessler (2018): The nuXmv model checker Home Page. https://nuxmv.fbk.eu/.
  19. 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.
  20. ISTI-FMT Laboratory (2018): KandISTI-UMC Home Page. https://fmt.isti.cnr.it/umc.
  21. Leslie Lamport (2002): Specifying Systems. https://lamport.azurewebsites.net/tla/book-02-08-08.pdf.
  22. 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.
  23. 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.
  24. 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.
  25. 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.
  26. 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.
  27. University of Oxford (2018): FDR4 — The CSP Refinement Checker Home Page. https://www.cs.ox.ac.uk/projects/fdr/.
  28. 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.
  29. spinroot (2018): Verifying Multi-threaded Software with Spin. http://spinroot.com/spin/whatispin.html.
  30. 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.
  31. CPN Tools (2018): CPN Tools Home Page. http://cpntools.org/.
  32. Uppsala University and Aalborg University (2015): UPPAAL Home Page. http://www.uppaal.org/.
  33. 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.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org