The Correctness of a Distributed Real-Time System

In this thesis we review and extend the pervasive correctness proof for an asynchronous distributed real-time system published in [KP07a]. We take a two-step approach: first, we argue about a single electronic control unit (ECU) consisting of a processor (running the OSEKtime-like operating system OLOS) and a FlexRay-like interface called automotive bus controller (ABC). We extend [KP07a] among others by a local OLOS model [Kna08] and go into details regarding the handling of interrupts and the treatment of devices. Second, we connect several ECUs via the ABCs and reason about the complete distributed system, see also [KP07b]. Note that the formalization of the scheduling correctness is reported in [ABK08b]. Through several abstraction layers we prove the correctness of the distributed system with respect to a new lock-step model COA that completely abstracts from the ABCs. By establishing the DISTR model [Kna08] it becomes possible to literally reuse the arguments from the first part of this thesis and therefore to simplify the analysis of the complete distributed system. To illustrate the applicability of DISTR, we have formally proven the top-level correctness theorem in the theorem prover Isabelle/HOL. Throughout the thesis we tie together theorems regarding: processor, ABC, compiler, micro kernel, operating system, and the worst case execution time analysis of applications and systems software. In dieser Arbeit betrachten und erweitern wir den durchgangigen Korrektheitsbeweis fur ein asynchrones verteiltes Echtzeitsystem aus [KP07a]. Wir gehen in zwei Schritten vor: Zuerst betrachten wir eine einzelne elektronische Kontrolleinheit (ECU) bestehend aus einem Prozessor (welcher das OSEKtime ahnliche Betriebsystem OLOS ausfuhrt) und einem FlexRay ahnlichem Interface, auch automobiler Bus Controller (ABC) genannt. Wir erweitern [KP07a] unter anderem um ein lokales OLOS Model [Kna08] und detaillieren die Behandlung von Interrupts sowie den Umgang mit Geraten. Im zweiten Schritt verbinden wir mehrere ECUs durch die ABCs und argumentieren uber das gesamte System, siehe auch [KP07b]. Uber die Formalisierung der Scheduler Korrektheit wird in [ABK08b] berichtet. Uber mehrere Abstraktionsebenen beweisen wir die Korrektheit des verteilten Systems bezuglich eines neuen gleichgetakteten Modells COA in dem vollstandig von den ABCs abstrahiert wird. Durch die Einfuhrung des DISTR Models [Kna08] ist es moglich die Argumente aus dem ersten Teil dieser Arbeit in der Analyse des gesamten verteilten Systems wortlich wieder zu verwenden. Um die Anwendbarkeit von DISTR zu verdeutlichen haben wir formal die oberste Korrektheits-Aussage im Theorembeweiser Isabelle/HOL bewiesen. Im Zuge dieser Arbeit verbinden wir Theoreme bezuglich: Prozessor, ABC, Compiler, Mikrokern, Betriebsystem und der Worst-Case Laufzeit-Analyse von Applikationen und System Software.