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

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.