Decomposition for compositional verification / Björn Metzler. 2010
Content
- Introduction
- A Vision of Correct Software
- Formal Methods and their Combination
- Compositional Verification
- Contributions
- Thesis Structure
- Background: Integrated Formal Methods
- Background: Compositional Reasoning
- Approaches to the State Space Explosion
- Compositional Reasoning
- Assume Guarantee Proof Rules
- Obstacles to the Application of Assume Guarantee Reasoning
- Learning for Compositional Verification
- Assume-Guarantee Reasoning for CSP
- Related Work
- Decomposition of a Specification
- Overview
- Cut of a Dependence Graph
- Fragmentation of the Control Flow Graph
- Correctness Criteria for the Fragmentation
- Definition of a Cut
- Candy Machine Revisited: Cut of the Dependence Graph
- Decomposing CSP-OZ Specifications
- Intermediate Definition of the Decomposition
- Preservation of the Data Dependences
- Preservation of the Control Flow
- Renaming for the Decomposition
- Definition of the Decomposition
- Candy Machine Revisited: Decomposition
- Improvement of the Decomposition
- Decomposition for the General Case: Number Swapper
- Related Work
- Correctness of the Decomposition
- Ensuring Correct Synchronisation
- Correctness for the CSP Part
- Correctness for the Object-Z Part
- Correctness of the Renaming for the Decomposition
- CSP Laws for Parallel Composition
- Proof of the Main Theorem
- Finding Reasonable Decompositions
- Decomposition Heuristics
- First Heuristic: Cut Size
- Second Heuristic: Even Distribution
- Third Heuristic: Few Transmission
- Fourth Heuristic: Few Addressing
- Evaluation of Decomposition Heuristics
- Candy Machine Revisited: Evaluation of Cuts
- Case Study: Two Phase Commit Protocol
- Discussion
- Related Work
- Implementation and Experimental Results
- Syspect
- Decomposition Framework for Syspect
- Decomposition Plug-In
- Mass Validation
- Model Checking with FDR2 and the CSPLChecker
- Counterexample Analysis
- Overall Workflow
- Experimental Results
- Conclusion
- Glossary of Symbols
- Bibliography
- List of Figures
- List of Tables
- Index