Sciweavers

CADE
2008
Springer

Model Stack for the Pervasive Verification of a Microkernel-based Operating System

14 years 11 months ago
Model Stack for the Pervasive Verification of a Microkernel-based Operating System
Abstract. Operating-system verification gains increasing research interest. The complexity of such systems is, however, challenging and many endeavors are limited in some respect: Some projects focus on a particular aspect like memory safety, not pursuing functional correctness. Others restrict their verification efforts to a single layer of software, assuming correctness of those below. Only few projects aim at pervasive formal verification of a computer system over several software layers. In our paper, we present an approach to the formal specification of a microkernel-based operating system at several layers and glance on our verification experience with this model stack. From our experience, we conclude that pervasiveness entails more than just cumulative verification efforts on several layers. In fact, it is a challenging task to integrate models and proofs into a uniform, coherent theory.
Jan Dörrenbächer, Matthias Daum, Sebasti
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where CADE
Authors Jan Dörrenbächer, Matthias Daum, Sebastian Bogan
Comments (0)