Model Checking Software

Name: Model Checking Software | 18th International SPIN Workshop, Snowbird, UT, USA, July 14-15, 2011, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

18th International SPIN Workshop, Snowbird, UT, USA, July 14-15, 2011, Proceedings

Alex Groce Madanlal Musuvathi(Herausgeber*in)

Springer (Verlag)

Erschienen am 5. Juli 2011

X, 195 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-22306-8 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

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

Systemvoraussetzungen

Als PDF speichern Als Link merken