Paper Info
Title
The Design of a Multicore Extension of the SPIN Model Checker
Abstract
We describe an extension of the SPIN model checker for use on multi-core shared-memory systems and report on its performance. We show how, with proper load balancing, the time requirements of a verification run can in some cases be reduced close to N-fold when N processing cores are used. We also analyze the types of verification problems for which multi-core algorithms cannot provide relief. The extensions discussed here require only relatively small changes in the SPIN source code, and are compatible with most existing verification modes, such as partial order reduction, the verification of temporal logic formulae, bitstate hashing, and hash-compact compression.
Year
DOI
Venue
2007
10.1109/TSE.2007.70724
IEEE Transactions on Software Engineering
Keywords
Field
DocType
existing verification mode,verification problem,verification run,SPIN model checker,SPIN source code,multi-core algorithm,multi-core shared-memory system,N processing core,hash-compact compression,partial order reduction,Multicore Extension,SPIN Model Checker
Model checking,Computer science,Load balancing (computing),Source code,Parallel computing,Theoretical computer science,Model of computation,Partial order reduction,Temporal logic,Multi-core processor,SPIN model checker
Journal
Volume
Issue
ISSN
33
10
0098-5589
Citations 
PageRank 
References 
8
0.61
20
Authors
2
Name
Order
Citations
PageRank
Gerard J. Holzmann13539381.90
Dragan Bosnacki227626.95