作者:
B Boigelot，P Godefroid
关键词:
model checking ； spin ； access.bus
摘要:
This paper presents a case study of the use of model checking for analyzing an industrial protocol, the ACCESS.bus 64 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 64 were unaware of these flaws at a very late stage of their development process. We also present suggestions for solving the detected problems.
在线下载