References

  1. F. Mazzanti et al. (2020): Work Stream 1 Deliverables. 4SECURail, doi:10.5281/zenodo.5807738.
  2. D. Basile, A. Fantechi & I. Rosadi (2021): Formal Analysis of the UNISIG Safety Application Intermediate Sub-layer - Applying Formal Methods to Railway Standard Interfaces. In: Alberto Lluch-Lafuente & Anastasia Mavridou: Formal Methods for Industrial Critical Systems - 26th International Conference, FMICS 2021, LNCS 12863. Springer, pp. 174–190, doi:10.1007/978-3-030-85248-1_11.
  3. M. ter Beek, S. Gnesi & F. Mazzanti (2015): From EU Projects to a Family of Model Checkers - From Kandinsky to KandISTI. In: Rocco De Nicola & Rolf Hennicker: Software, Services, and Systems, LNCS 8950. Springer, pp. 312–328, doi:10.1007/978-3-319-15545-6_20.
  4. M.H. ter Beek, A. Fantechi, S. Gnesi & F. 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.
  5. M. Bouwman, D van der Wal, Luttik, M. Stoelinga & A. Rensink (2020): What is the Point: Formal Analysis and Test Generation for a Railway Standard. In: Piero Baraldi, Francesco Di Maio & Enrico Zio: Proceedings of the 30th European Safety and Reliability Conference and the 15th Probabilistic Safety Assessment and Management Conference, pp. 921–928, doi:10.3850/978-981-14-8593-0_4410-cd.
  6. A. Ferrari, F. Mazzanti, D. Basile, M. H. ter Beek & A. Fantechi (2020): Comparing Formal Tools for System Design: a Judgment Study. In: Proceedings of the 42nd ACM/IEEE International Conference on Software Engineering (ICSE'20). ACM, pp. 62–74, doi:10.1145/3377811.3380373.
  7. A. Ferrari, F. Mazzanti, D. Basile & M. Ter Beek (2021): Systematic Evaluation and Usability Analysis of Formal Methods Tools for Railway Signaling System Design. IEEE Transactions on Software Engineering, pp. 1–1, doi:10.1109/TSE.2021.3124677.
  8. A. Ferrari, F. Mazzanti, D. Basile, A. Fantechi, S. Gnesi, D. Trentini, A. Piattino & B. Sturani (2012): ASTRAIL Deliverable D4.3 - Validation Report. Available at http://www.astrail.eu/download.aspx?id=d7ae1ebf-52b4-4bde-b25e-ae251fd906df.
  9. H. Garavel & F. Lang (2001): SVL: A Scripting Language for Compositional Verification. In: Formal Techniques for Networked and Distributed Systems, FORTE 2001, IFIP TC6/WG6.1 - 21^\voidb@x st International Conference on Formal Techniques for Networked and Distributed Systems, August 28-31, 2001, Cheju Island, Korea, IFIP Conference Proceedings 197. Kluwer, pp. 377–394, doi:10.1007/0-306-47003-9_24.
  10. H. Garavel, F. Lang, R. Mateescu & W. Serwe (2013): CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. 15(2), pp. 89–107, doi:10.1007/s10009-012-0244-z.
  11. H. Garavel, F. Lang & W. Serwe (2017): From LOTOS to LNT. In: ModelEd, TestEd, TrustEd - Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday, Lecture Notes in Computer Science 10500. Springer, pp. 3–26, doi:10.1007/978-3-319-68270-9_1.
  12. S. Gnesi & F. Mazzanti (2011): An Abstract, on the Fly Framework for the Verification of Service-Oriented Systems, pp. 390–407, Lecture Notes in Computer Science 6582. Springer, doi:10.1007/978-3-642-20401-2_18.
  13. F. Lang, R. Mateescu & F. Mazzanti (2020): Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities. In: Armin Biere & David Parker: Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part II, Lecture Notes in Computer Science 12079. Springer, pp. 57–76, doi:10.1007/978-3-030-45237-7_4.
  14. F. Lang, R. Mateescu & F. Mazzanti (2021): Compositional verification of concurrent systems by combining bisimulations. Formal Methods in System Design, doi:10.1007/s10703-021-00360-w.
  15. M Leuschel & M.J. Butler (2008): ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), pp. 185–203, doi:10.1007/s10009-007-0063-9.
  16. F. Mazzanti, D. Basile, A. Fantechi, S. Gnesi & A. Ferrari (2020): D2.1: Specification of formal development demonstrator. In: Work Stream 1 Deliverables. 4SECURail, doi:10.5281/zenodo.5807738.
  17. F. Mazzanti & D. Belli (2020): D2.1: Formal development demonstrator prototype, final release. In: Work Stream 1 Deliverables. 4SECURail, doi:10.5281/zenodo.5807738.
  18. F. Mazzanti & D. Belli (2020): Formal models of the SAI /CSL systems of the 4SECURail case study, doi:10.5281/zenodo.5541307.
  19. F. Mazzanti & D. Belli (2020): The UMC2LNT and UMC2PROB model transformation tools, doi:10.5281/zenodo.5541350.
  20. F. Mazzanti & D.Belli (2022): The 4SECURail Formal Methods Demonstrator. In: The 4th International Conference on Reliability, Safety and Security of Railway Systems (RSSRAIL), Lecture Notes in Computer Science 13294. Springer, doi:10.5281/zenodo.6245955.
  21. F. Mazzanti & A. Ferrari (2018): Ten Diverse Formal Models for a CBTC Automatic Train Supervision System. In: John P. Gallagher, Rob van Glabbeek & Wendelin Serwe: Proceedings of the 3rd Workshop on Models for Formal Analysis of Real Systems and the 6th International Workshop on Verification and Program Transformation (MARS/VPT'18), EPTCS 268, pp. 104–149, doi:10.4204/EPTCS.268.4.
  22. F. Mazzanti, A. Ferrari & G. O. Spagnolo (2018): Towards formal methods diversity in railways: an experience report with seven frameworks. Int. J. Softw. Tools Technol. Transf. 20(3), pp. 263–288, doi:10.1007/s10009- 018-0488-3.
  23. A. Piattino (2020): D2.1: Case study requirements and specification. In: Work Stream 1 Deliverables. 4SECURail, doi:10.5281/zenodo.5807738.
  24. S. Salunkhe, R. Berglehner & A. Rasheeq (2021): Automatic Transformation of SysML Model to Event-B Model for Railway CCS Application. In: Alexander Raschke & Dominique Méry: Rigorous State-Based Methods - 8th International Conference, ABZ 2021, Ulm, Germany, June 9-11, 2021, Proceedings, Lecture Notes in Computer Science 12709. Springer, pp. 143–149, doi:10.1007/978-3-030-77543-8_14.
  25. C. F. Snook & M. J. Butler (2006): UML-B: Formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), pp. 92–122, doi:10.1145/1125808.1125811.
  26. Geneva. ISO/IEC International Organization for Standardization Information Technology (1989): International Standard 8807 - LOTOS A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour.
  27. Geneva. ISO/IEC International Organization for Standardization Information Technology (2001): International Standard 15437:2001 - Enhancements to LOTOS (E-LOTOS).
  28. UNISIG (2012): SUBSET-098, RBC/RBC Safe Communication Interface, v3.0.3. Available at https://www.era.europa.eu/sites/default/files/filesystem/ertms/ccs_tsi_annex_a_-_mandatory_specifications/set_of_specifications_1_etcs_b2_gsm-r_b1/index063_-_subset-098_v100.pdf.
  29. UNISIG (2015): SUBSET-037, EuroRadio FIS v3.2.0. Available at https://www.era.europa.eu/sites/default/files/filesystem/ertms/ccs_tsi_annex_a_-_mandatory_specifications/set_of_specifications_3_etcs_b3_r2_gsm-r_b1/index010_-_subset-037_v320.pdf.
  30. UNISIG (2015): SUBSET-039, FIS for the RBC/RBC Handover v3.2.0. Available at https://www.era.europa.eu/sites/default/files/filesystem/ertms/ccs_tsi_annex_a_-_mandatory_specifications/set_of_specifications_3_etcs_b3_r2_gsm-r_b1/index012_-_subset-039_v320.pdf.
  31. C. Vaghi (2021): Specification of Cost-Benefit Analysis and learning curves, final release. In: Work Stream 1 Deliverables. 4SECURail, doi:10.5281/zenodo.5807738.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org