PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Fantechi A. Twenty-five years of formal methods and railways: what next?. Steve Counsell, Manuel Nez (eds.). (Lecture Notes in Computer Science, vol. 8368). Heidelberg: Springer-Verlag, 2014.
 
 
Abstract
(English)
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.
URL: http://link.springer.com/chapter/10.1007%2F978-3-319-05032-4_13
DOI: 10.1007/978-3-319-05032-4_13
Subject Railway Signalling Systems
Formal methods
Formal verification
D.2.4 SOFTWARE ENGINEERING. Formal methods


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional