Model Checking Software
18th International SPIN Workshop, Snowbird, UT, USA, July 14-15, 2011, Proceedings
Erschienen am 5. Juli 2011
X, 195 Seiten
978-3-642-22306-8 (ISBN)
Beschreibung
This book constitutes the refereed proceedings of the 18th International SPIN workshop on Model Checking Software, SPIN 2011, held in Snowbird, UT, USA, in July 2011.
The 10 revised full papers presented together with 2 tool demonstration papers and 1 invited contribution were carefully reviewed and selected from 29 submissions. The papers are organized in topical sections on abstractions and state-space reductions; search strategies; PROMELA encodings and extensions; and applications of model checking.
Weitere Details
Weitere Ausgaben
Inhalt
- Title
- Preface
- Organization
- Table of Contents
- Invited Contributions
- Model Checking Cell Fate Decisions
- Abstractions and State-Space Reductions
- Property-Dependent Reductions for the Modal Mu-Calculus
- Introduction
- Background
- Maximal Hiding
- Mu-Calculus Fragment Compatible with brds
- Mu-Calculus Fragment Ldsbr
- Subsuming ActlX
- Subsuming Selective and Weak -Calculus
- Implementation and Experiments
- Conclusion and Future Work
- References
- String Abstractions for String Verification
- Introduction
- A Motivating Example
- String Abstractions
- Regular Abstraction
- Alphabet Abstraction
- Relation Abstraction
- Composing Abstractions
- Heuristics and Refinement for Abstraction Selection
- Handling Complex String Operations
- Implementation and Experiments
- Related Work
- Conclusions
- References
- Parallel Recursive State Compression for Free
- Introduction
- Background
- Parallel Reachability
- Collapse and Tree Compression
- Why Parallelization is Not Trivial
- Tree Database
- Basic Tree Database
- Concurrent Tree Database
- References in the Open Set
- Incremental Tree Database
- Analysis of Compression Ratios
- Experiments
- Compression Ratios
- Performance and Scalability
- Conclusions
- References
- Search Strategies
- Depth Bounded Explicit-State Model Checking
- Introduction
- Background
- Depth Bounding: Warmup
- Efficient Depth Bounding
- Efficient Depth Bounded DFS with Thresholding
- Traces and Frontier Trees
- Empirical Results
- Related Work
- Conclusion
- References
- Randomized Backtracking in State Space Traversal
- Introduction
- Background and Related Work
- Randomized Backtracking
- Evaluation
- Conclusion
- References
- PROMELA Encodings and Extensions
- An Analytic Evaluation of SystemC Encodings in Promela
- Introduction
- Structure of SystemC Design
- Encoding SystemC in Promela
- Basic Building Blocks
- Thread-To-Process Encoding
- Thread-To-Atomic-Block Encoding
- One-Atomic-Block Encoding
- Analytical Comparison of Encodings
- Properties to Verify
- Search Behavior
- Other Existing Encodings
- Experimental Evaluation
- Related Work
- Conclusions and Future Work
- References
- Building Extensible Specifications and Implementations of Promela with AbleP
- Introduction and Motivation
- Use of AbleP and Its Language Extensions
- Using an AbleP Extended Language Framework
- Extending AbleP with Independently Developed Extensions
- Implementing AbleP and Its Language Extensions
- Specification and Composition of Syntax
- Specification and Composition of Semantics
- Solutions to Some Challenges in Promela
- Related Work
- Conclusion
- References
- Applications of Model Checking
- Program Sketching via CTL* Model Checking
- Introduction
- Motivating Example
- Preliminaries
- Syntax and Semantics of CTL*
- Relating Automata to Kripke Structures
- Kripke Structure with Oracles and Implementations
- Implementations for Kripke Structures with Oracles
- Sketching Programs in Practice
- Essentials of the Synchronous Programming Language Quartz
- Examples
- Conclusions
- References
- A Verification-Based Approach to Memory Fence Insertion in Relaxed Memory Systems
- Introduction
- Concurrent Programs and Memory Models
- Representing Sets of Buffer Contents and State Space Exploration
- From SC to TSO
- An Iterative mfence Insertion Algorithm
- Experimental Results
- Conclusions and Comparison with Other Work
- References
- Model Checking Industrial Robot Systems
- Introduction
- Background
- Problem Statement
- Robot Programming Language
- Interlock Algorithm
- Solution
- VKRC to PROMELA Compiler
- PLC Generator
- Fault Description
- Putting the Model Together
- Replay Trace
- Evaluation
- Conclusion and Future Work
- References
- Tool Demonstrations
- EpiSpin: An Eclipse Plug-In for Promela/Spin Using Spoofax
- Introduction
- Background
- EpiSpin
- Static Communication Analyzer
- Testing the Plug-In
- Conclusions and Future Work
- References
- DiPro - A Tool for Probabilistic Counterexample Generation
- Introduction
- Probabilistic Counterexamples
- The DiPro Tool
- Case Study: Airbag System
- Conclusion
- References
- dBug: Systematic Testing of Unmodified Distributed and Multi-threaded Systems
- Introduction
- Tool
- Architecture
- Functionality
- Limitations
- Evaluation
- Conclusion
- References
- Author Index
