Formal verification of overhead accounting in an avionics RTOS

This paper describes our work modeling key portions of the safety-critical software infrastructure in an integrated modular avionics (IMA) platform in an effort to analytically establish correctness of important aspects of its design. In particular, we use model checking to verify timing properties of the Deos™ real-time operating system in the presence of various advanced scheduling features. We focus here on the addition of scheduler overhead processing time to the Deos model and analyzing its effect on the time partitioning property and the internal assertions (function preconditions) in the model. Our model includes advanced scheduling features (dynamic threads, slack recovery, aperiodic interrupts) and explicitly models the scheduler operations at the same level of detail as the source code. Our findings support the use of formal methods to verify key properties of safety-critical systems that would be difficult or impossible to establish otherwise.