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
1996In Lecture Notes in Computer Science, 1051, p. 465-478
Peer reviewed
 

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



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 :
F.R.S.-FNRS - Fonds de la Recherche Scientifique
Bell Laboratories
Available on ORBi :
since 03 November 2010

Statistics


Number of views
51 (6 by ULiège)
Number of downloads
110 (3 by ULiège)

Scopus citations®
 
15
Scopus citations®
without self-citations
8
OpenCitations
 
9
OpenAlex citations
 
22

Bibliography


Similar publications



Contact ORBi