This book constitutes the refereed proceedings of the 10th International SPIN workshop on Model Checking of Software, SPIN 2003, held in Portland, OR, USA in May 2003 as an ICSE 2003 satellite workshop.
The 14 revised full papers and 3 revised tool papers presented were carefully reviewed and selected from 30 submissions. The book presents state-of-the-art results on the analysis and verification of distributed software systems using the SPIN model checker as one of the most powerful and widely applied systems.
Author(s): Theo C. Ruys (auth.), Thomas Ball, Sriram K. Rajamani (eds.)
Series: Lecture Notes in Computer Science 2648
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2003
Language: English
Pages: 241
Tags: Logics and Meanings of Programs; Software Engineering; Programming Languages, Compilers, Interpreters
Optimal Scheduling Using Branch and Bound with SPIN 4.0....Pages 1-17
A Requirements Patterns-Driven Approach to Specify Systems and Check Properties....Pages 18-33
Formal Modeling and Analysis of an Avionics Triplex Sensor Voter....Pages 34-48
Distributed Explicit Fair Cycle Detection (Set Based Approach)....Pages 49-73
Efficient Model Checking of Safety Properties....Pages 74-88
A Light-Weight Algorithm for Model Checking with Symmetry Reduction and Weak Fairness....Pages 89-103
A SAT Characterization of Boolean-Program Correctness....Pages 104-120
What Went Wrong: Explaining Counterexamples....Pages 121-136
A Nearly Memory-Optimal Data Structure for Sets and Mappings....Pages 136-150
Checking Consistency of SDL+MSC Specifications....Pages 151-166
Model Checking Publish-Subscribe Systems....Pages 166-180
A Methodology for Model-Checking Ad-hoc Networks....Pages 181-196
Promela Planning....Pages 197-213
Thread-Modular Model Checking....Pages 213-224
Unification & Sharing in Timed Automata Verification....Pages 225-229
The Maude LTL Model Checker and Its Implementation....Pages 230-234
Software Verification with BLAST....Pages 235-239
