TY  - THES
T1  - OS verification extended : on the formal verification of device drivers and the correctness of client/server software
A1  - Alkassar,Eyad
Y1  - 2009/09/15
N2  - This thesis tackles two important challenges in OS verication: The formal verification of device drivers and the correctness of client/server software. Device drivers are an integral part of system software. Not only high-level functionality such as le I/O depends on devices. Even basic OS features, such as demand paging, need correctly implemented drivers. In this thesis, we show how to pervasively integrate devices and their drivers into a language stack reaching from the level of assembly up to high-level languages. This stack is leveraged for the formal verification of a simple hard disk driver, which is subsequently embedded into Verisoft's micro kernel. To the best of our knowledge, this marks the rst formal functional verication of a device driver against a realistic device and system model. Remote procedure calls (RPCs) lie at the heart of any client/server software. In the second part of this thesis, we present a specication of an RPC mechanism and we outline how to verify an implementation of this mechanism at the code level. The formalization is based on a model of user processes running concurrently under a simple OS, which provides inter-process communication and portmapper system calls. A simple theory of non interference permits us to use conventional sequential program analysis between system calls. To the best of our knowledge this is the first
treatment of the correctness of an entire RPC mechanism at the code level.
KW  - Betriebssystem
KW  - Verifikation
KW  - Treiber <Programm>
KW  - Festplatte
KW  - Client-Server-Konzept
KW  - Implementierung
KW  - RPC
CY  - Saarbrücken
PB  - Universitäts- und Landesbibliothek
AD  - Postfach 151141, 66041 Saarbrücken
UR  - http://scidok.sulb.uni-saarland.de/volltexte/2009/2420
ER  -