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

2014

Contribution to book Restricted

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

Fantechi A.

D.2.4 SOFTWARE ENGINEERING. Formal methods Formal verification

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.

Source: Software Engineering and Formal Methods, edited by Steve Counsell, Manuel Núñez, pp. 167–183, 2014

Metrics

Back to previous page

Cite as

BibTeX entry

@inbook{oai:it.cnr:prodotti:302181,
	title = {Twenty-Five Years of Formal Methods and Railways: What Next?},
	author = {Fantechi A.},
	doi = {10.1007/978-3-319-05032-4_13},
	booktitle = {Software Engineering and Formal Methods, edited by Steve Counsell, Manuel Núñez, pp. 167–183, 2014},
	year = {2014}
}