DocumentCode
1556000
Title
The model checker SPIN
Author
Holzmann, Gerard J.
Author_Institution
Comput. Sci. Res. Center, AT&T Bell Labs., Murray Hill, NJ, USA
Volume
23
Issue
5
fYear
1997
fDate
5/1/1997 12:00:00 AM
Firstpage
279
Lastpage
295
Abstract
SPIN is an efficient verification system for models of distributed software systems. It has been used to detect design errors in applications ranging from high-level descriptions of distributed algorithms to detailed code for controlling telephone exchanges. The paper gives an overview of the design and structure of the verifier, reviews its theoretical foundation, and gives an overview of significant practical applications
Keywords
distributed processing; formal specification; formal verification; SPIN model checker; design error detection; detailed code; distributed software system models; efficient verification system; high-level distributed algorithm descriptions; telephone exchange control; verifier design; verifier structure; Algorithm design and analysis; Application software; Concurrent computing; Control system synthesis; Design methodology; Distributed algorithms; Error correction codes; Message passing; Software systems; Telephony;
fLanguage
English
Journal_Title
Software Engineering, IEEE Transactions on
Publisher
ieee
ISSN
0098-5589
Type
jour
DOI
10.1109/32.588521
Filename
588521
Link To Document