Model Checking Software
Preface
Organization
Table of Contents
From Model Checking to a Temporal Proof
Introduction
Preliminaries
Checking the Validity of a Formula over a Program
Constructing a Temporal Logic Proof
An Automatic Ranking Function
Conclusions
References
Model Checking if Your Life Depends on It a View from Intel's Trenches
Model-Checking Infinite State-Space Systems with Fine-Grained Abstractions Using SPIN
Introduction
Preliminaries
Finite Total Orders
Multiple-Valued Sets and Relations
Chi LTL
Multiple-Valued Languages and Automata
Multiple-Valued Languages
Multiple-Valued Automata
Composition
Conversion between Chi LTL and Chi B{accent 127 u}chi Automata
Chi LTL Model-Checking
The Model-Checking Problem
Decision Procedure for Chi LTL Model-Checking
Chi LTL Model-Checking in SPIN
Conclusion
References
Implementing LTL Model Checking with Net Unfoldings
Introduction
Petri Nets
Automata Theoretic Approach to Model Checking LTL
Basic Definitions on Unfoldings
Tableau System
Generating the Tableau
Experimental Results
Conclusions
References
Directed Explicit Model Checking with HSF-SPIN
Introduction
Automata-Based Model Checking
Searching for Safety Property Violations
Searching for Liveness Property Violations
Classification of Never Claims
Improved Nested Depth-First-Search
A* and Improved-Nested-DFS
Heuristics for Errors in Protocols
Precompiling State Distance Tables
The Formula-Based Heuristics
The Model Checker HSF-SPIN
Experimental Results
Experiments on Detecting Deadlocks
Experiments on Detecting Violation of System Invariants
Experiments on Detecting Assertion Violations
Experiments on Detecting Violation of LTL Properties
Performance of HSF-SPIN
Conclusion
References
Addressing Dynamic Issues of Program Model Checking
Introduction
Complexity of the State
The Representation of the State
Collapsing the State
Optimizing the Backtrack
Exploiting Symmetries
Garbage Collection
Distributed Memory
Improvements
Partitioning
Static Partitioning
Dynamic Partitioning
Conclusions
References
Automatically Validating Temporal Safety Properties of Interfaces
Introduction
Overview
Property Specification
Refinement Algorithm
Example
Initial Boolean Program
Model Checking the Boolean Program
Predicate Discovery over Error Path
The Second Boolean Program
C2BP: A Predicate Abstractor for C
BEBOP: A Model Checker for Boolean Programs
NEWTON: A Predicate Discoverer
NT Device Drivers: Case Study
Property 1
Property 2
Related Work
Conclusions
References
Verification Experiments on the MASCARA Protocol
Introduction
The Context
The IF Language and Validation Environment
The MASCARA Protocol
Verification of the MASCARA Protocol
The Experimental System
Properties
Verification Methodology
Complexity
Verification Results
Conclusion and Perspectives
References
Using SPIN for Feature Interaction Analysis - A Case Study
Introduction
Related Work
Approach
Background -- Features and Interactions
Basic Call Service
Basic Call Service Properties in LTL
Basic Call Service in Promela
Unoptimised Code
Options and State-Space Reduction Techniques
Basic Call Service Validation
Features
Features
Temporal Properties for Features
The Features in Promela
Implementation of Features: The $Feature_lookup$ Inline
Feature Validation
Static Analysis
Dynamic Analysis
Dynamic Analysis -- Feature Interaction Results
Automatic Model Generation and Feature Interaction
Conclusions and Future Directions
References
Behavioural Analysis of the Enterprise JavaBeansTM Component Architecture
Introduction
Enterprise {JavaBeans}
The Component Architecture
Behavioural Specifications
Formalization
Issues and Approach
Promela Model
Behavioural Analysis
Entity Beans
Session Beans
Discussion
Comparisons
Conclusion
References
p2b: A Translation Utility for Linking Promela and Symbolic Model Checking (Tool Paper)
Introduction
How p2bfuturelet next Works
SMV Code Generated by p2bfuturelet next
Supported Constructs
Specifying Variable Ranges
Benchmark Examples
The Dining Philosophers Problem
A Mutual Exclusion Protocol over Asynchronous Channels
Conclusion
References
Transformations for Model Checking Distributed Java Programs
Introduction
Centralization
RMI Removal
Pseudo-Cryptography
Implementation and Case Study
References
Distributed LTL Model-Checking in SPIN
Introduction
Distributed SPIN
Problems with Extending the Distributed SPIN
Distributed Model-Checking Algorithm
Dependency Structure
Manager Process
The Algorithm
Complexity and Effectiveness
Conclusions and Future Research
References
Parallel State Space Construction for Model-Checking
Introduction
Definitions
Parallel Generation of LTSs
Construction of Partitioned LTSs
Merging of Partitioned LTSs into Monolithic LTSs
Experimental Results
Speedup
Choosing a Good Partition Function
Using Communication Buffers
Conclusion and Future Work
References
Model Checking Systems of Replicated Processes with Spin
Introduction
Permutation of Processes
Our Goal
New Keywords for Promela
Requirements
Abstraction Based on Process Permutations
Syntactic Definition
Semantic Definition
Permutations of States
Abstraction
Pragmatic Abstraction
Permutable Specification
Computation of the Reduced System
The Pseudo-Sorting Algorithm
Efficiency Depends on the Variable Declaration Order
Layered Model
Conclusions
Appendix
References
A SPIN-Based Model Checker for Telecommunication Protocols
Introduction
Why ASN.1?
Why SPIN?
EASN Language
Related Work
Outline of Paper
EASN, the Verification Tool
Encoding State Efficiently
Outline of EASN System Design
EASN Modules
EASN System from an User Perspective
ASN.1 to C++ Translation
EASN System: Implementation
SPIN and Its Subsystemscite {8}
EASN and Its Subsystems
Ensuring Consistency - Incrementally
Incremental Hashing
Correctness of Implementation {it vis-a-vis} SPIN
Results and Conclusions
Performance of EASN vs SPIN
Future Work
References
Modeling and Verifying a Price Model for Congestion Control in Computer Networks Using Promela/Spin
Introduction
Overall Design of the Pricing Model
The Mathematical Priority Pricing Model
Model 1 (Demand Equilibrium Model)
Model 2 (Dynamic Priority Pricing Model)
Design and Architecture
Channel, User Processes, and Strategies
Administrator Process and Strategy
Simulation and Verification
Simulation of Channel, User, and Administrator Processes
Verification of Convergence to Equilibrium (Proposition 1)
Verification of Dynamic Priority Pricing (Proposition 2)
Discussion
Contribution of PROMELA/SPIN in Model 1
Contribution of PROMELA/SPIN in Model 2
Limitations
Conclusion
References
A Model Checking Project at Philips Research
Introduction
Relevance of the Project
Proposed Solutions
Extracting a Promela Program from a YAPI Program
Extracting a Verification Model Directly from a YAPI Program, on-the-Fly
Another Reason to Investigate TorX
Related Work
Conclusions
References
Applications of Model Checking at Honeywell Laboratories
Introduction
Automatic Synthesis of Real-Time Controllers
Real-Time Scheduler of the MetaH Executive
Fault-Tolerant Ethernet Protocol
Time Partitioning in Integrated Modular Avionics
Synchronization Protocol for Avionics Communication Bus
References
Coarse-Granular Model Checking in Practice
Motivation
The Agent Building Center
System-Level Testing of Telephony Systems
A Personalized E-Commerce Shop
A Role-Based Editorial System
Conclusions
References
Author Index