Papers

Most of the papers here are available as PDF files. Each paper additionally should link to a BTX file with the bibliography information. Click here for information about BTX. Papers with no BTX file are unpublished.

Verifying a Bus-Arbitration Protocol with PVS
PDF File

This paper demonstatrates how to model a protocol (in particular, the IEEE896 FutureBus arbitration protocol) in PVS using our automaton framework and proves its correctness using execution-fragment based reasoning.

A Taxonomy for Reactive Systems
PS File

With Hanno Wupper.

This paper lays down some consistent terminology for the observational phenomena related to real-time systems.

A Survey: Applying Formal Methods to a Software Intensive System
PDF File

By: Adriaan de Groot, Jozef Hooman, Fabrice Kordon, Emmanuel Pavoit-Adet, Isabelle Mounier, Michel Lemoine, Gervais Gaudiere, Victor Winter and Deepak Kapur

(I'm listed first because I'm alphabetically first; primary author Victor Winter. The case study description is here PS File.)

Analyzing the Light Control with PVS
PDF File

With Jozef Hooman.

This is just an abstract. The original paper is published in the Journal of Universal Computer Science.

Last changed Mon Mar 1 11:55:38 MET 2004