TY  - THES
T1  - Formal verification of a small real-time operating system
A1  - Schmidt,Mareike Dorothee
Y1  - 2011/04/15
N2  - The foundation of this thesis is a distributed real-time system that connects several electronic control units (ECUs) with a communication bus. Each ECU consists of a processor executing the real-time operating system OLOS and several applications on the one hand, and an interface to the bus (ABC) on the other hand. OLOS provides application scheduling and controls the communication with the bus. The applications may communicate with OLOS via so-called system calls. For applications written in high-level languages these calls are available in terms of library functions. First, we present the design and the implementation of OLOS and its necessary library functions. Thereafter, we introduce the abstract model of an entire ECU which specifies the interface to the bus (ABC), process models and the behaviour of OLOS. Then, we formulate a simulation theorem between the abstract ECU model and a model that embeds the concrete OLOS implementation. The proof of this theorem provides us with the implementation correctness of OLOS. Based on the formal correctness of our operating system, the last section of this thesis presents an approach to pervasively verify applications that are executed under OLOS on a single ECU.
KW  - Echtzeitsystem
KW  - Verifikation
KW  - Implementierung
CY  - Saarbrücken
PB  - Universitäts- und Landesbibliothek
AD  - Postfach 151141, 66041 Saarbrücken
UR  - http://scidok.sulb.uni-saarland.de/volltexte/2011/3844
ER  -