Modeling and Verification of the RUBIS μ−Kernel with SPIN
Grégory Duval, Jacques Julliand · 2002
This experience was lead at the Laboratoire Informatique de Besancon and its aim was the modeling and verification of the RUBIS kernel, a multitasking multiprocessor operating system. An other aim of this study was to find out a method to formalize and to verify such systems. The first results are given. A modeling approach is used and we formalize the of the system, the scenarios and the properties in Promela and linear temporal logic. Two kinds of are produced, the so-called abstract models and detailed models which are model-checked with the SPIN tool. An exhaustive verification of the intertask communication features of RUBIS was carried out. It revealed several problems in the management of error return codes. This paper gives hints of a method to construct and formalize the of an operating system such as RUBIS.