Model Checking in Practice: An Analysis of the ACCESS.bus Protocol using SPIN

Boigelot, Bernard; Godefroid, Patrice

doi:10.1007/3-540-60973-3_102

Download

Paper published in a journal (Scientific congresses and symposiums)

Model Checking in Practice: An Analysis of the ACCESS.bus Protocol using SPIN

Boigelot, Bernard; Godefroid, Patrice

1996 • In Lecture Notes in Computer Science, 1051, p. 465-478

Peer reviewed

Permalink
https://hdl.handle.net/2268/74871

DOI
10.1007/3-540-60973-3_102

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

BG97a.pdf

Author preprint (202.49 kB)

Download

The original publication is available at www.springerlink.com

All documents in ORBi are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Keywords :

model checking; spin; access.bus

Abstract :

[en] 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.

Disciplines :

Computer science

Author, co-author :

Boigelot, Bernard ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique

Godefroid, Patrice

Language :

English

Title :

Model Checking in Practice: An Analysis of the ACCESS.bus Protocol using SPIN

Publication date :

1996

Event name :

Third International Symposium of Formal Methods Europe

Event place :

Oxford, United Kingdom

Audience :

International

Journal title :

Lecture Notes in Computer Science

ISSN :

0302-9743

eISSN :

1611-3349

Publisher :

Springer, Berlin, Germany

Volume :

1051

Pages :

465-478

Peer reviewed :

Peer reviewed

Funders :

Fonds de la Recherche Scientifique (Communauté française de Belgique) - F.R.S.-FNRS, Bell Laboratories

Available on ORBi :

since 03 November 2010

Statistics

Number of views

41 (6 by ULiège)

Number of downloads

95 (3 by ULiège)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

Bibliography

ACCESS.bus Industry Group. Access.bus specifications, version 2.2. 370 Altair Way, Suite 215, Sunnyvale, California 94086, USA, 1994.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. A CM Transactions on Programming Languages and Systems, 8(2):244-263, January 1986.
C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. In Proc. And Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science, pages 233-242, Rutgers, June 1990.
D. L. Dill, A. J. Drexler, A. J. Hu, and C. H. Yang. Protocol verification as a hardware design aid. In 1992 IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 522-525, Cambridge, MA, October 1992. IEEE Computer Society.
E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science. Elsevier/MIT Press, Amsterdam/ Cambridge, 1990.
J.C. Fernandez, H. Garavel, L. Mounier, A. Rasse, C. Rodriguez, and J. Sifakis. A toolbox for the verification of LOTOS programs. In Proc. of the l$th International Conference on Software Engineering ICSE'14, Melbourne, Australia, May 1992. ACM.
P. Godefroid and G. J. Holzmann. On the verification of temporal properties. In Proc. 13th IFIP WG 6.1 International Symposium on Protocol Specification, Testing, and Verification, pages 109-124, Liege, May 1993. North-HoUand.
R. Gerth, D. Peled, M. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Protocol Specification Testing and Verification, pages 3-18, Warsaw, Poland, 1995. Chapman & Hall.
Z. Har'El and R. P. Kurshan. Software for analytical development of communication protocols. ATFJT Technical Journal, 1990.
G. J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.
J. Hooman. Verifying part of the ACCESS.bus protocol using PVS. To appear in the Proceedings of Foundations of Software Technology and Theoretical Computer Science, December 1995.
M.T. Liu. Protocol engineering. Advances in Computing, 29:79-195, 1989.
O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Twelfth A CM Symposium on Principles of Programming Languages, pages 97-107, New Orleans, January 1985.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
S. Owre, J. Rushby, and N. Shankar. PVS: A prototype verification system. In Proc. 11th Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 748-752. Springer-Verlag, 1992.
J.P. Quielle and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proc. 5th Int'l Symp. on Programming, volume 137 of Lecture Notes in Computer Science, pages 337-351. Springer-Verlag, 1981.
H. Rudin. Network protocols and tools to help produce them. Annual Review of Computer Science, 2:291-316, 1987.
M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science, pages 322-331, Cambridge, June 1986.