Since more than 25 years, railway signalling is the subject of successful industrial application of formal methods in the development and verification of its computerized equipment. However the evolution of the technology of railways signalling systems in this long term has had a strong influence on the way formal methods can be applied in their design and implementation. At the same time important advances had been also achieved in the formal methods area. The scope of the formal methods discipline has enlarged from the methodological provably correct software construction of the beginnings to the analysis and modelling of increasingly complex systems, always on the edge of the ever improving capacity of the analysis tools, thanks to the technological advances in formal verification of both qualitative and quantitative properties of such complex systems. The thesis we will put forward in this paper is that the complexity of future railway systems of systems can be addressed with advantage only by a higher degree of distribution of functions on local interoperable computers - communicating by means of standard protocols - and by adopting a multi-level formal modelling suitable to support the verification at different abstraction levels, and at different life-cycle times, of the safe interaction among the distributed functions.

Twenty-Five Years of Formal Methods and Railways: What Next? - Software Engineering and Formal Methods / Fantechi, Alessandro. - STAMPA. - 8368:(2014), pp. 167-183. (Intervento presentato al convegno Formal Methods for Industrial Critical Systems (FMICS) 2013) [10.1007/978-3-319-05032-4_13].

Twenty-Five Years of Formal Methods and Railways: What Next? - Software Engineering and Formal Methods

FANTECHI, ALESSANDRO
2014

Abstract

Since more than 25 years, railway signalling is the subject of successful industrial application of formal methods in the development and verification of its computerized equipment. However the evolution of the technology of railways signalling systems in this long term has had a strong influence on the way formal methods can be applied in their design and implementation. At the same time important advances had been also achieved in the formal methods area. The scope of the formal methods discipline has enlarged from the methodological provably correct software construction of the beginnings to the analysis and modelling of increasingly complex systems, always on the edge of the ever improving capacity of the analysis tools, thanks to the technological advances in formal verification of both qualitative and quantitative properties of such complex systems. The thesis we will put forward in this paper is that the complexity of future railway systems of systems can be addressed with advantage only by a higher degree of distribution of functions on local interoperable computers - communicating by means of standard protocols - and by adopting a multi-level formal modelling suitable to support the verification at different abstraction levels, and at different life-cycle times, of the safe interaction among the distributed functions.
2014
Lecture Notes in Computer Science - Software Engineering and Formal Methods
Formal Methods for Industrial Critical Systems (FMICS) 2013
Fantechi, Alessandro
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/845322
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 43
  • ???jsp.display-item.citation.isi??? 34
social impact