Online model checking mechanism and its applications / by Yuhong Zhao. Paderborn
Inhalt
- 1 Introduction
- 2 Preliminaries
- 2.1 Fault, Error and Failure
- 2.2 Behavioral Model
- 2.3 Property Specification
- 2.4 LTL Model Checking
- 2.5 Bounded Model Checking (BMC)
- 3 Related Work
- 4 Online Model Checking Mechanism
- 4.1 Online Model Checking
- 4.1.1 Problem Statement
- 4.1.2 Online Model Checking for Safety Properties
- 4.1.3 Online Model Checking for Liveness Properties
- 4.1.4 Discussion
- 4.1.5 Prototype Implementation and Experimental Results
- 4.2 Accelerating Online Model Checking
- 4.2.1 Reducing Workload
- 4.2.2 Online Symbolic Model Checking
- 4.2.3 Parallel Computing
- 4.2.4 Prototype Implementation and Experimental Results
- 4.3 Summary
- 5 Model Generation and Source Code Instrumentation
- 6 Integration of Online Model Checking with RTOS
- 6.1 Integration Framework
- 6.2 ORCOS
- 6.3 Prototype Implementation
- 6.4 Evaluation
- 6.5 Discussion
- 6.6 Summary
- 7 Case Study
- 7.1 TCAS
- 7.2 Source Code
- 7.3 Mapping Functions
- 7.4 Abstract Model
- 7.5 Experimental Results
- 7.6 Summary
- 8 Online Model Checking for Hybrid Systems
- 8.1 Motivation
- 8.2 Hybrid Automaton
- 8.3 Online Falsification Problem
- 8.4 Offline Backward Reachable Set Computation
- 8.5 Online Forward Reachability Checking
- 8.6 Experimental Results
- 8.7 Related Work
- 8.8 Conclusion
- 9 Conclusion and Future Work
- A Case Study: TCAS
- List of Figures
- List of Tables
- List of Publications
- Bibliography