Abstract
This paper presents a case study of the use of model checking for analyzing an industrial protocol, the ACCESS.bus™ protocol. Our analysis of this protocol was carried out using SPIN, an automated verification system which includes an implementation of model-checking algorithms. A model of the protocol was developed, and properties expressed by linear-time temporal-logic formulas were checked on this model. This analysis revealed subtle flaws in the design of the protocol. Developers who worked on implementations of ACCESS.bus™were unaware of these flaws at a very late stage of their development process. We also present suggestions for solving the detected problems.
Cite
CITATION STYLE
Boigelot, B., & Godefroid, P. (1996). Model checking in practice: An analysis of the ACCESS.busTM protocol using SPIN. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1051, pp. 465–478). Springer Verlag. https://doi.org/10.1007/3-540-60973-3_102
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
