@incollection(ref4SECdeli,
 author       = {F. Mazzanti et al.},
 year         = {2020},
 title        = {Work Stream 1 Deliverables},
 publisher    = {4SECURail},
 doi          = {10.5281/zenodo.5807738},
)
@inproceedings(refFMICSbasile,
 author       = {D. Basile and A. Fantechi and I. Rosadi},
 year         = {2021},
 title        = {Formal Analysis of the {UNISIG} Safety Application Intermediate Sub-layer - Applying Formal Methods to Railway Standard Interfaces},
 editor       = {Lluch{-}Lafuente, Alberto and Anastasia Mavridou},
 booktitle    = {Formal Methods for Industrial Critical Systems - 26th International Conference, {FMICS} 2021},
 series       = {LNCS},
 volume       = {12863},
 publisher    = {Springer},
 pages        = {174--190},
 doi          = {10.1007/978-3-030-85248-1\_11},
)
@inproceedings(refKANDI,
 author       = {M. ter Beek and S. Gnesi and F. Mazzanti},
 year         = {2015},
 title        = {From {EU} Projects to a Family of Model Checkers - From Kandinsky to KandISTI},
 editor       = {Rocco De Nicola and Rolf Hennicker},
 booktitle    = {Software, Services, and Systems},
 series       = {LNCS},
 volume       = {8950},
 publisher    = {Springer},
 pages        = {312--328},
 doi          = {10.1007/978-3-319-15545-6_20},
)
@article(refUMC2,
 author       = {M.H. ter Beek and A. Fantechi and S. Gnesi and F. 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},
)
@inproceedings(refBasPoint,
 author       = {M. Bouwman and D van der Wal and Luttik and M. Stoelinga and A. Rensink},
 year         = {2020},
 title        = {What is the Point: Formal Analysis and Test Generation for a Railway Standard},
 editor       = {Piero Baraldi and {Di Maio}, Francesco and Enrico Zio},
 booktitle    = {Proceedings of the 30th European Safety and Reliability Conference and the 15th Probabilistic Safety Assessment and Management Conference},
 pages        = {921--928},
 doi          = {10.3850/978-981-14-8593-0_4410-cd},
)
@inproceedings(refICSE,
 author       = {A. Ferrari and F. Mazzanti and D. Basile and M. H. ter Beek and A. Fantechi},
 year         = {2020},
 title        = {Comparing Formal Tools for System Design: a Judgment Study},
 booktitle    = {Proceedings of the 42nd {ACM/IEEE} International Conference on Software Engineering (ICSE'20)},
 publisher    = {ACM},
 pages        = {62--74},
 doi          = {10.1145/3377811.3380373},
)
@article(refTSE,
 author       = {A. Ferrari and F. Mazzanti and D. Basile and M. Ter Beek},
 year         = {2021},
 title        = {Systematic Evaluation and Usability Analysis of Formal Methods Tools for Railway Signaling System Design},
 journal      = {IEEE Transactions on Software Engineering},
 pages        = {1--1},
 doi          = {10.1109/TSE.2021.3124677},
)
@misc(refD43,
 author       = {A. Ferrari and F. Mazzanti and D. Basile and A. Fantechi and S. Gnesi and D. Trentini and A. Piattino and B. Sturani},
 year         = {2012},
 title        = {ASTRAIL Deliverable D4.3 - Validation Report},
 url          = {http://www.astrail.eu/download.aspx?id=d7ae1ebf-52b4-4bde-b25e-ae251fd906df},
)
@inproceedings(refSVL,
 author       = {H. Garavel and F. Lang},
 year         = {2001},
 title        = {{SVL:} {A} Scripting Language for Compositional Verification},
 booktitle    = {Formal Techniques for Networked and Distributed Systems, {FORTE} 2001, {IFIP} {TC6/WG6.1} - 21${}^{\unhbox\voidb@x \hbox{st}}$ International Conference on Formal Techniques for Networked and Distributed Systems, August 28-31, 2001, Cheju Island, Korea},
 series       = {{IFIP} Conference Proceedings},
 volume       = {197},
 publisher    = {Kluwer},
 pages        = {377--394},
 doi          = {10.1007/0-306-47003-9_24},
)
@article(refCADP,
 author       = {H. Garavel and F. Lang and R. Mateescu and W. Serwe},
 year         = {2013},
 title        = {{CADP} 2011: a toolbox for the construction and analysis of distributed processes},
 journal      = {Int. J. Softw. Tools Technol. Transf.},
 volume       = {15},
 number       = {2},
 pages        = {89--107},
 doi          = {10.1007/s10009-012-0244-z},
)
@inproceedings(refLNT,
 author       = {H. Garavel and F. Lang and W. Serwe},
 year         = {2017},
 title        = {From {LOTOS} to {LNT}},
 booktitle    = {ModelEd, TestEd, TrustEd - Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday},
 series       = {Lecture Notes in Computer Science},
 volume       = {10500},
 publisher    = {Springer},
 pages        = {3--26},
 doi          = {10.1007/978-3-319-68270-9_1},
)
@inbook(refUMC1,
 author       = {S. Gnesi and F. Mazzanti},
 year         = {2011},
 title        = {An Abstract, on the Fly Framework for the Verification of Service-Oriented Systems},
 pages        = {390--407},
 series       = {Lecture Notes in Computer Science},
 volume       = {6582},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-20401-2_18},
)
@inproceedings(refTACAS,
 author       = {F. Lang and R. Mateescu and F. Mazzanti},
 year         = {2020},
 title        = {Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities},
 editor       = {Armin Biere and David Parker},
 booktitle    = {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}},
 series       = {Lecture Notes in Computer Science},
 volume       = {12079},
 publisher    = {Springer},
 pages        = {57--76},
 doi          = {10.1007/978-3-030-45237-7\_4},
)
@article(refFMSD,
 author       = {F. Lang and R. Mateescu and F. Mazzanti},
 year         = {2021},
 title        = {Compositional verification of concurrent systems by combining bisimulations},
 journal      = {Formal Methods in System Design},
 doi          = {10.1007/s10703-021-00360-w},
)
@article(refProB2008,
 author       = {M Leuschel and M.J. Butler},
 year         = {2008},
 title        = {ProB: an automated analysis toolset for the {B} method},
 journal      = {Int. J. Softw. Tools Technol. Transf.},
 volume       = {10},
 number       = {2},
 pages        = {185--203},
 doi          = {10.1007/s10009-007-0063-9},
)
@incollection(refD2.1,
 author       = {F. Mazzanti and D. Basile and A. Fantechi and S. Gnesi and A. Ferrari},
 year         = {2020},
 title        = {{D2.1}: {S}pecification of formal development demonstrator},
 booktitle    = {Work Stream 1 Deliverables},
 publisher    = {4SECURail},
 doi          = {10.5281/zenodo.5807738},
)
@incollection(refD2.5,
 author       = {F. Mazzanti and D. Belli},
 year         = {2020},
 title        = {{D2.1}: {F}ormal development demonstrator prototype, final release},
 booktitle    = {Work Stream 1 Deliverables},
 publisher    = {4SECURail},
 doi          = {10.5281/zenodo.5807738},
)
@misc(refZENmodels,
 author       = {F. Mazzanti and D. Belli},
 year         = {2020},
 title        = {Formal models of the SAI /CSL systems of the 4SECURail case study},
 doi          = {10.5281/zenodo.5541307},
)
@misc(refZENcode,
 author       = {F. Mazzanti and D. Belli},
 year         = {2020},
 title        = {The UMC2LNT and UMC2PROB model transformation tools},
 doi          = {10.5281/zenodo.5541350},
)
@inproceedings(refrssrail,
 author       = {F. Mazzanti and D.Belli},
 year         = {2022},
 title        = {The 4SECURail Formal Methods Demonstrator},
 booktitle    = {The 4th International Conference on Reliability, Safety and Security of Railway Systems (RSSRAIL)},
 series       = {Lecture Notes in Computer Science},
 volume       = {13294},
 publisher    = {Springer},
 doi          = {10.5281/zenodo.6245955},
)
@inproceedings(refMARSten,
 author       = {F. Mazzanti and A. Ferrari},
 year         = {2018},
 title        = {{Ten Diverse Formal Models for a {CBTC} Automatic Train Supervision System}},
 editor       = {John P. Gallagher and Rob van Glabbeek and Wendelin Serwe},
 booktitle    = {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)},
 series       = {EPTCS},
 volume       = {268},
 pages        = {104--149},
 doi          = {10.4204/EPTCS.268.4},
)
@article(refST7T7,
 author       = {F. Mazzanti and A. Ferrari and G. O. Spagnolo},
 year         = {2018},
 title        = {{Towards formal methods diversity in railways: an experience report with seven frameworks}},
 journal      = {Int. J. Softw. Tools Technol. Transf.},
 volume       = {20},
 number       = {3},
 pages        = {263--288},
 doi          = {10.1007/s10009- 018-0488-3},
)
@incollection(refD2.3,
 author       = {A. Piattino},
 year         = {2020},
 title        = {{D2.1}: {C}ase study requirements and specification},
 booktitle    = {Work Stream 1 Deliverables},
 publisher    = {4SECURail},
 doi          = {10.5281/zenodo.5807738},
)
@inproceedings(refSYSMLB,
 author       = {S. Salunkhe and R. Berglehner and A. Rasheeq},
 year         = {2021},
 title        = {Automatic Transformation of SysML Model to Event-B Model for Railway {CCS} Application},
 editor       = {Alexander Raschke and Dominique M{\'{e}}ry},
 booktitle    = {Rigorous State-Based Methods - 8th International Conference, {ABZ} 2021, Ulm, Germany, June 9-11, 2021, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {12709},
 publisher    = {Springer},
 pages        = {143--149},
 doi          = {10.1007/978-3-030-77543-8\_14},
)
@article(refUMLB,
 author       = {C. F. Snook and M. J. Butler},
 year         = {2006},
 title        = {{UML-B:} Formal modeling and design aided by {UML}},
 journal      = {{ACM} Trans. Softw. Eng. Methodol.},
 volume       = {15},
 number       = {1},
 pages        = {92--122},
 doi          = {10.1145/1125808.1125811},
)
@misc(lotos,
 author       = {ISO/IEC International Organization for Standardization Information Technology, Geneva.},
 year         = {1989},
 title        = {International Standard 8807 - LOTOS \IeC{\textendash} A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour},
)
@misc(elotos,
 author       = {ISO/IEC International Organization for Standardization Information Technology, Geneva.},
 year         = {2001},
 title        = {International Standard 15437:2001 - Enhancements to LOTOS (E-LOTOS)},
)
@misc(sub98,
 author       = {UNISIG},
 year         = {2012},
 title        = {SUBSET-098, RBC/RBC Safe Communication Interface, v3.0.3},
 url          = {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},
)
@misc(sub37,
 author       = {UNISIG},
 year         = {2015},
 title        = {SUBSET-037, EuroRadio FIS v3.2.0},
 url          = {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},
)
@misc(sub39,
 author       = {UNISIG},
 year         = {2015},
 title        = {SUBSET-039, FIS for the RBC/RBC Handover v3.2.0},
 url          = {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},
)
@incollection(refD2.6,
 author       = {C. Vaghi},
 year         = {2021},
 title        = {Specification of Cost-Benefit Analysis and learning curves, final release},
 booktitle    = {Work Stream 1 Deliverables},
 publisher    = {4SECURail},
 doi          = {10.5281/zenodo.5807738},
)