Model Checking Software: 14th International SPIN Workshop, Berlin, Germany, July 1-3, 2007, Proceedings (Lecture Notes in Computer Science, 4595)

✍ Scribed by Dragan Bosnacki (editor), Stefan Edelkamp (editor)

• Publisher: Springer
• Year: 2007
• Tongue: English
• Leaves: 294
• Category: Library

✦ Synopsis

This book presents the proceedings of the 14th International SPIN workshop on Model Checking Software, held in Berlin, Germany. Fourteen full papers are presented, together with four tool presentation papers and the abstracts of two invited talks. The papers are organized into topical sections covering directed model checking, partial order reduction, program analysis, exploration advances, modeling and case studies, and tool demonstrations.

✦ Table of Contents

Title Page
Preface
Organization
Table of Contents
StackSnuffer: Curing Orion’s Unsoundness
Tutorial: Parallel Model Checking
Local Abstraction-Refinement for the mu-Calculus
Introduction
Example
Preliminaries
System
Strong-Weak-Parity-Game
Property Language
CEGAR Locally Applied on Configurations
Heuristics
Bottom Up Strategy
Breadth First Strategy
Youngest First Strategy
Optimizations of the Algorithm
Conclusion
Pseudo Code of Additional Procedures
Minimal Counterexample Generation for SPIN
Introduction
Context and Notations
Space Constraints
An Algorithm to Find the Smallest Counterexample
Reconstructing the Counterexample
Distances from the Initial State
Another Breadth First Search
BFS Guided by a Priority Queue
Synthesis
Improvements
Conclusion
Generating Counter-Examples Through Randomized Guided Search
Introduction
Background
Randomized GDS
Evaluation
Conclusions and Future Work
Distributed Dynamic Partial Order Reduction Based Verification of Threaded Software
Introduction
Background
Overview of Inspect
Definitions
Dynamic Partial Order Reduction
Algorithm
Load Balancing
Worker Routine
Distributed DPOR
Updating the Backtrack Set
Implementation and Experiments
Related Work
Conclusion
Some Solutions to the Ignoring Problem
Formal Background
State Transition Graphs
Partial-Order Reduction
Related Works
Motivations
A Proviso for Safety Properties
A Proviso for Liveness Properties
Experiments
Conclusion
Cartesian Partial-Order Reduction
Introduction
Partial Order Reduction
Main Results
Overview
Basic Definitions
Cartesian Partial Order Reduction
Cartesian Semantics Versus an Optimal Persistent Sets Algorithm
Computing Cartesian Vectors
Model Checking Algorithm
Experimental Evaluation
Related Work
Conclusions
Benchmarks Description
Robots
CMIS
SharedArray
SharedPtr
Indexer
File System
Dining Philosophers
On-the-Fly Dynamic Dead Variable Analysis
Introduction
Related Work
DVA Maximal Reduction
Maximal Dynamic Dead Variable Analysis
Results
Conclusions and Future Work
SAT-Based Summarization for Boolean Programs
Introduction
Background
Bounded Model Checking
Semantics of Boolean Programs
Summarization Using QBF
Universal Summaries
Benchmarks
Conclusion
LTL Satisfiability Checking
Introduction
Theoretical Background
Tools Tested
Explicit Tools
Symbolic Tools
Experimental Methods
Performance Evaluation
Input Formulas
Experimental Results
The Scalability Challenge
Symbolic Approaches Outperform Explicit Approaches
Discussion
An Embeddable Virtual Machine for State Space Generation
Introduction
Virtual Machine Specification
Machine State
Invariants
Byte-Code Semantics
Scheduling
Applications
Promela
An External-Memory Model Checker
NIPS and DiVinE
Model Checking Embedded Systems Software
Related Work
Promela Semantics
Virtual Machines
Conclusions
Benchmarks
Scalable Multi-core LTL Model-Checking
Introduction
Parallel LTL Model-Checking Algorithms
Implementation Techniques
Shared-Memory Platform
Implementing Algorithms in Shared-Memory
Communication
Memory Allocation
Efficient Termination Detection
Implementing OWCTY in Shared-Memory
Experiments
Methodology
Results
Comparison with SPIN
Conclusions
A SystemC/TLM Semantics in Promela and Its Possible Applications
Introduction
Transaction Level Modeling with SystemC
Subset of SystemC
A Simple Example
Expressing SystemC Semantics in Promela
General Ideas
Intuitive Idea: Representation with Automata
Detailed Encoding
Validation of the Semantics
Alternative Encoding
Verification
Generic Properties
Checking Assertions
Benchmarks
Comments on Performance
Related Work
Further Work and Conclusion
Towards Model Checking Spatial Properties with SPIN
Introduction
Spatial Logic for Spin
Computational Model
Logic Syntax
Semantics
Examples
Applications
Model Checking
Basic Algorithm
Spatial Equivalences
Exploiting Simulations
Experiments
Conclusion
Model Extraction for ARINC 653 Based Avionics Software
Introduction
Model Extraction with Well-Defined APIs
The ARINC API for Avionics Software: APEX Interface
Modelling Processes
Modelling the Process Scheduling
Modelling Time
Life-Cycle of Time Events
Implementing and Using Time Events
Experimental Results
Testing the Model of the API
Related Work
Conclusions
Code of the Example
Test Case Checking SET_PRIORITY
BEEM: Benchmarks for Explicit Model Checkers
Introduction
Experimental Work in Model Checking
BEEM
Summary
C.OPEN and ANNOTATOR: Tools for On-the-Fly Model Checking C Programs
Introduction
Software Architecture
Conclusion and Future Work
ACSAR: Software Model Checking with Transfinite Refinement
Introduction
A Motivating Example
Loop Abstraction Approach
How Does ACSAR Abstract Loops?
ACSAR in Short
Experimental Evaluation
Instrumenting C Programs with Nested Word Monitors
Introduction
Language Description
Implementation and Case Studies
Author Index