This book constitutes the refereed proceedings of the 8th International SPIN Workshop held in Toronto, Canada, in May 2001.
The SPIN model checker is one of the most powerful and popular systems for the analysis and verification of distributed and concurrent systems.
The 13 revised full papers presented together with one invited survey paper and three invited industrial experience reports were carefully reviewed and selected from 26 submissions. Besides foundational issues of program analysis and formal verification, the papers focus on tools for model checking and practical applications in a variety of fields.
Author(s): Doron Peled, Lenore Zuck (auth.), Matthew Dwyer (eds.)
Series: Lecture Notes in Computer Science 2057
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2001
Language: English
Pages: 318
Tags: Logics and Meanings of Programs; Software Engineering; Programming Languages, Compilers, Interpreters
From model checking to a temporal proof....Pages 1-14
Model checking if your life depends on it: a view from intel’s trenches....Pages 15-15
Model-checking in finite state-space systems with fine-grained abstractions using SPIN....Pages 16-36
Implementing LTL model checking with net unfoldings....Pages 37-56
Directed explicit model checking with HSF-SPIN....Pages 57-79
Addressing dynamic issues of program model checking....Pages 80-102
Automatically validating temporal safety properties of interfaces....Pages 102-122
Verification experiments on the MASCARA protocol....Pages 123-142
Using SPIN for feature interaction analysis - a case study....Pages 143-162
Behavioural analysis of the enterprise javaBeans ™ component architecture....Pages 163-182
p2b: A translation utility for linking promela and symbolic model checking (tool paper)....Pages 183-191
Transformations for model checking distributed java programs....Pages 192-199
Distributed LTL model-checking in SPIN....Pages 200-216
Parallel state space construction for model-checking....Pages 217-234
Model checking systems of replicated processes with spin....Pages 235-251
A SPIN-based model checker for telecommunication protocols....Pages 252-271
Modeling and verifying a price model for congestion control in computer networks using promela/spin....Pages 272-287
A model checking project at philips research....Pages 288-295
Applications of model checking at honeywell laboratories....Pages 296-303
Coarse-granular model checking in practice....Pages 304-311
