{'fraction_non_alphanumeric': 0.019736842105263157, 'fraction_numerical': 0.0, 'mean_word_length': 4.7421383647798745, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Modeling and Verification of the RUBIS μ−Kernel with SPIN

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 models of the system, the scenarios and the properties in Promela and linear temporal logic. Two kinds of models 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 models of an operating system such as RUBIS.