Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-26028
Titel: Formal verification of a small real-time operating system
Sonstige Titel: Formale Verifikation eines kleinen Echtzeitbetriebssystems
Verfasser: Schmidt, Mareike Dorothee
Sprache: Englisch
Erscheinungsjahr: 2011
SWD-Schlagwörter: Echtzeitsystem
Verifikation
Implementierung
Freie Schlagwörter: Olos
Echtzeitbetriebssystem
sicherheitskritische Anwendungen
automotive
real-time operating system
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: 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.
Grundlage dieser Arbeit ist ein verteiltes Echtzeitsystem, welches mehrere elektronische Kontrolleinheiten (ECUs) mit einem Kommunikationsbus verbindet. Jede dieser Kontrolleinheiten besteht aus einer Schnittstelle zum Bus (ABC) und einem Prozessor, welcher das Echtzeitbetriebssystem Olos und mehrere Anwendungen ausführt. Olos organisiert die Ausführungszeit der Anwendungen auf dem Prozessor und steuert deren Kommunikation mit dem Bus. Die Anwendungen haben die Möglichkeit, über sogenannte Systemaufrufe mit dem Betriebssystem zu kommunizieren. Diese stehen den Anwendungen, die in höheren Programmiersprachen geschrieben sind, in Form von Bibliotheksfunktionen zur Verfügung. Zuerst stellen wir den Entwurf und die Implementierung von Olos und den notwendigen Bibliotheksfunktionen vor. Danach beschreiben wir das abstrakte Modell einer vollständigen ECU, welches die Schnittstelle zum Bus (ABC), Prozessmodelle und das Verhalten des Betriebssystems Olos festlegt. Wir formulieren ein Simulationstheorem zwischen dem abstrakten ECU Modell und einem Modell mit eingebetteter konkreter Olos-Implementierung. Der Beweis dieser Aussage liefert uns die Implementierungskorrektheit von Olos. Im letzten Teil der Arbeit benutzen wir dieses Ergebnis als Grundlage für einen Ansatz, mit dem durchgängig Anwendungen verifiziert werden können, die unter Olos auf einer elektronischen Kontrolleinheit ausgeführt werden.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-38447
hdl:20.500.11880/26084
http://dx.doi.org/10.22028/D291-26028
Erstgutachter: Paul, Wolfgang J.
Tag der mündlichen Prüfung: 12-Apr-2011
SciDok-Publikation: 15-Apr-2011
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
MS11.pdf1,4 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.