Formal methods have a great potential of application as powerful specification and early debugging methods in the development of industrial systems. In certain application fields, formal methods are even becoming part of standards. However, the application of formal methods in the development of industrial products is by no means trivial. Indeed, formal methods can be costly, slow down the process of development, and require changes on the development cycle, and training. This paper describes a project developed by Ansaldo Segnalamento Ferroviario with the collaboration of Irst. Formal methods have been successfully applied to the development of an industrial communication protocol for distributed, safety critical systems. The project used a formal language to specify the protocol, and codes checking techniques to validate the model
Formal Specification and validation of a Vital Communication Protocol
Cimatti, Alessandro;Sebastiani, Roberto;Traverso, Paolo;Villafiorita Monteleone, Adolfo
1999-01-01
Abstract
Formal methods have a great potential of application as powerful specification and early debugging methods in the development of industrial systems. In certain application fields, formal methods are even becoming part of standards. However, the application of formal methods in the development of industrial products is by no means trivial. Indeed, formal methods can be costly, slow down the process of development, and require changes on the development cycle, and training. This paper describes a project developed by Ansaldo Segnalamento Ferroviario with the collaboration of Irst. Formal methods have been successfully applied to the development of an industrial communication protocol for distributed, safety critical systems. The project used a formal language to specify the protocol, and codes checking techniques to validate the modelI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
