next up previous
Next: Bibliography Up: High-Confidence Operating Systems 1 Previous: 4 Verifying Models Against

5 Status

We are currently developing tool support for the CCM modeling formalism with the goal of applying HCOS techniques to several variants of Linux, including SMP, Beowulf, and embedded Linux. To date, a prototype has been implemented that consists of a visual front-end for interactive specification using CCMs, and automatic generation of Java code for most CCM features. Other tools developed for the analysis of non-CCM operational models are also being retargeted to CCMs.

Erez Zadok 2002-06-30