Content

•  
  Introduction
•  
   Flawless Design of Complex Systems
•  
   Formal Specifications and their Verification
•  
   Slicing for Verification
•  
   Contributions
•  
   Thesis Structure
•  
   Background: Program Slicing
•  
  Foundations of Program Slicing
•  
   Slicing Based on Data Flow Equations
•  
   Slicing Based on Dependence Graphs
•  
  Classification of Slicing Approaches
•  
   Type of Slicing: Static or Dynamic
•  
   Direction of Slicing: Forward or Backward
•  
   Type of Slice: Executable or Non-Executable
•  
   Type of Slicing Criterion
•  
   Target Language
•  
   Area of Application
•  
  Further Techniques Aiming at State Space Reduction
•  
   High-Level Techniques
•  
   Low-Level Techniques
•  
   Integrated Formal Specifications
•  
   Object-Z Specifications
•  
   Example: Tic-Tac-Toe
•  
   Semantics of Object-Z Specifications
•  
   CSP-OZ Specifications
•  
   Example: Untimed Air Conditioner System
•  
   Semantics of CSP-OZ Specifications
•  
   CSP-OZ-DC Specifications
•  
   Example: Timed Air Conditioner System
•  
   Semantics of CSP-OZ-DC Specifications
•  
   Dependence Analysis
•  
   Object-Z Specifications
•  
   Control Flow Graph
•  
   Dependence Graph
•  
   Example: Tic-Tac-Toe Dependence Graph
•  
  CSP-OZ Specifications
•  
   Control Flow Graph
•  
   Dependence Graph
•  
   Example: Untimed Air Conditioner Dependence Graph
•  
  CSP-OZ-DC Specifications
•  
   Control Flow Graph
•  
   Dependence Graph
•  
   Example: Timed Air Conditioner Dependence Graph
•  
   Specification Slices
•  
   Slicing Criterion
•  
   Dependence Graph Backwards Slice
•  
   Object-Z Specification Slices
•  
   Example: Tic-Tac-Toe Specification
•  
   CSP-OZ Specification Slices
•  
   Example: Air Conditioner Slice
•  
   CSP-OZ-DC Specification Slices
•  
   Example: Timed Air Conditioner System Slice
•  
   Classification of the Slicing Approach
•  
   Slicing Correctness
•  
  Relating Slicing Results with Specification Elements
•  
   Projection Relation between Interpretations
•  
   Transitions of CSP Process Projections
•  
   CSP Transition Sequences
•  
   Irrelevant Events
•  
   Irrelevant DC Formulae
•  
   Projection Relation Established by Slicing
•  
   Stuttering Invariance of Test Formulae
•  
  Stuttering Invariance of State/Event Interval Logic
•  
   State/Event Interval Logic
•  
   Projection of Event-Labelled Kripke Structures
•  
   Tool Support and Experimental Evaluation
•  
   Syspect --- Modelling Environment for CSP-OZ-DC
•  
   Class Diagrams
•  
   State Machines
•  
   Component Diagrams
•  
   DC Counterexample Formulae
•  
   DC Test Formulae and Syspect Verification
•  
   Specification Export
•  
  Slicing Implementation within Syspect
•  
   Syspect Slicing Plug-In
•  
   Control Flow Graph
•  
   Dependence Graph
•  
   Slicing Report
•  
  Benchmarks and Case Studies
•  
   Tic-Tac-Toe
•  
   Cash Register
•  
   Untimed Air Conditioner
•  
   Timed Air Conditioner System
•  
   Elevator
•  
   ETCS-EM Case Study
•  
   Airport Specification
•  
   Summary of Experimental Results
•  
  Conclusion
•  
   Summary
•  
   Perspectives
•  
   Bibliography
•  
   List of Figures
•  
   List of Tables
•  
   Index