Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-26012
Titel: On the formal foundation of a verification approach for system-level concurrent programs
Verfasser: Daum, Matthhias
Sprache: Englisch
Erscheinungsjahr: 2010
SWD-Schlagwörter: Programmverifikation
Scheduling
Freie Schlagwörter: verification
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: Though program verification is known and used since decades, the verification of a complete computer system still remains a grand challenge. In essence, this challenge stems from the interaction of various programs. Different techniques have been proposed for the verification of communicating programs. Common to all, however, is that they rely on several (usually implicit) assumptions about the underlying system. Typically, such assumptions include compiler correctness, scheduler fairness, and a certain noninterference between the local program behavior and its environment. This thesis aims at discharging these assumptions for the processes of the microkernel Vamos. More specifically, this work formally justifies the abstraction from a kernel model with explicit, deterministic scheduling to a concurrent process system with non-deterministic but temporally fair scheduling. Our formal results form the foundation of a verification approach for system-level concurrent programs. We outline this approach on example properties of a user-mode operating system.
Obwohl es schon jahrzehntelang Programmverifikation gibt, wird die Verifikation eines kompletten Computersystems auch heute noch als eine große Herausforderung angesehen. Im Wesentlichen ergibt sich diese Herausforderung aus der vielfältigen Interaktion von Programmen. Verschiedene Techniken wurden für die Verifikation kommunizierender Programme vorgeschlagen. Alle haben jedoch gemein, dass sie sich auf mehrere (meist implizite) Annahmen über das zugrunde liegende System stützen. In der Regel sind solche Annahmen Compiler-Korrektheit, Scheduler-Fairness und eine gewisse Störfreiheit des lokalen Programmverhaltens vom Verhalten seiner Umgebung. Die vorliegende Dissertation beschäftigt sich mit der Entlastung dieser Annahmen für die Prozesse des Mikrokerns Vamos. Genauer gesagt, rechtfertigt diese Arbeit formal die Abstraktion von einem Kernmodell mit explizitem, deterministischem Scheduling zu einem nebenläufigen Prozesssystem mit nicht-deterministischem, aber temporal fairem Scheduling. Die formalen Ergebnisse bilden die Grundlage eines Verifikationsansatzes für nebenläufige, systemnahe Programme. Dieser Ansatz wird am Beispiel von Eigenschaften eines User-Mode-Betriebssystems erläutert.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-34718
hdl:20.500.11880/26068
http://dx.doi.org/10.22028/D291-26012
Erstgutachter: Paul, Wolfgang J.
Tag der mündlichen Prüfung: 28-Jun-2010
SciDok-Publikation: 22-Dez-2010
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 
Dissertation_6233_Daum_Matt_2010.pdf1,06 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.