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 model checking techniques to validate the model.
Chapter PDF
Similar content being viewed by others
References
J. Bowen. Formal Methods in Safety-Critical Standards. Oxford University Computing Laboratory Technical Report, 1995.
J. Bowen. The Industrial Take-Up of Formal Methods. Oxford University Computing Laboratory Technical Report, 1995.
A. Cimatti, R. Sebastiani, and P. Traverso. Specifica formale dei protocolli Safety Layer e Connection Manager (Formal specification of the Safety Layer and Connection Manager protocols). In italian. ITC-IRST deliverable 9808-02, project Safety Critical Applications III-SCAPIII, January 1999.
European Commitee for Electrotechnical Standardization. European Standard-Railway Applications: Software for Railways Control and Protection Systems. EN 50128, 1995.
G.J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.
ITU-T. CCITT specification and description language (SDL), March 1993. ITU-T Recommendation Z.100.
ITU-T. Message Sequence Chart (MSC), October 1996. ITU-T Recommendation Z.120.
Profibus Nutzerorganization. Profibus Standard, July 1996. DIN 19 245.
A. Tanenbaum. Computer Networks. Prentice Hall, 1989.
VERILOG. ObjectGEODE Documentation. Available at http://www.verilogusa.com.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cimatti, A., Pieraccini, P.L., Sebastiani, R., Traverso, P., Villafiorita, A. (1999). Formal specification and validation of a vital communication protocol. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_34
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_34
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive