de
en
Schliessen
Detailsuche
Bibliotheken
Projekt
Impressum
Datenschutz
Schliessen
Publizieren
Besondere Sammlungen
Digitalisierungsservice
Hilfe
Impressum
Datenschutz
zum Inhalt
Detailsuche
Schnellsuche:
OK
Ergebnisliste
Titel
Titel
Inhalt
Inhalt
Seite
Seite
Im Werk suchen
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.3.1 Linear Temporal Logic
2.3.2 Büchi Automaton
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
5.1 Embedded Control Applications
5.2 Model Generation
5.3 Source Code Instrumentation
5.3.1 MISRA C
5.3.2 Control Flow Graph
5.3.3 Graph Partitioning
5.4 Summary
6 Integration of Online Model Checking with RTOS
6.1 Integration Framework
6.2 ORCOS
6.3 Prototype Implementation
6.4 Evaluation
6.4.1 Overhead Analysis
6.4.2 Overhead Measurement
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
9.1 Conclusion
9.2 Future Work
A Case Study: TCAS
A.1 RA Component of TCAS
A.2 Monitored Variables and Mapping Functions
A.3 Abstract Model
List of Figures
List of Tables
List of Publications
Bibliography
Die detaillierte Suchanfrage erfordert aktiviertes Javascript.