Case study in coalgebraic specification: Memory management in the Fiasco microkernel

This page describes the PVS sources that contain proofs and examples for my report on the Fiasco case study of applying coalgebraic specification to the memory management of the Fiasco mikrokernel.

General Information

Abstract of the paper

This case study applies coalgebraic specification and verification techniques to the Fiasco microkernel developed at Dresden University of Technology. A part of the memory management of Fiasco was specified in the Coalgebraic Class Specification Language CCSL. With the support of a modern theorem prover (namely PVS) it was possible to check the source code of Fiasco against this specification. It turns out that, on the basis of coalgebras and with the use of state of the art tools like PVS and CCSL, it becomes feasible to verify practically used operation-system software.

About the contents

CCSL is a specification language for classes of object-oriented languages. Fisaco is a mikrokernel operating system that is written in C++. The originator of Fiasco, Michael Hohmuth is a close friend of mine. These were the prerequisite. Six month later I learnt how virtual memory works on the Intel 32-bit architecture and I verified machanically an important property of the Fiasco sources. This directory contains all relevant files of the case study. These web pages describe how to run the proofs on your computer.

Technicalities

The sources of the case study are plain ASCII files, so you can view them with any program you want. But if you actually want to run the proofs, the situation is more difficult.

The case study was developed with PVS version 2.2, patch level 1.46. At the moment PVS version 2.3 patch level 36 is available. But PVS 2.3 still contains lots of bugs that are triggered by the case study. Look at the PVS problem page to see if the PVS team made any progress in fixing bugs. PVS is available at http://pvs.csl.sri.com. PVS 2.2. is still available via ftp at ftp://pvs.csl.sri.com/pub/pvs/pvs2.2/ (mirrored at ftp://ftp.informatik.uni-ulm.de/pub/KI/pvs/pvs2.2). PVS 2.2 does not run on my Debian Linux box. But there are no problems on RedHat Linux and on Solaris.

Once you got PVS 2.2 running download the distribution and unzip and untar it. To typecheck everything start PVS in the new directory, and type

M-x load-file pvs-batch.el

(This issues type-check commands for 14 files and will take quite a while.) Then, you can prove everything by issuing prove-importchain in theory Alles, file all.pvs.

The VFiasco Project

This case study was preliminary work for the VFiasco project, which will start this year.

Detailed description of the files in this directory Jump to my home page Download the distribution Download the technical report on the case study VFiasco Project

last changed on 21 Jun 2001 by Hendrik