Safety analysis of Trampoline OS using model checking: An experience report

Model checking is an effective technique used to identify subtle problems in software safety. Its comprehensive search method on system state space provides high-level confidence regarding verification results, and its automated counterexample generation facility is a useful tool for tracing potential safety bugs. However, this comprehensiveness requires a large amount of resources and is often too expensive to be applied in practice. This work reports our experience with the software safety analysis of the Trampoline operating system using model checking. Trampoline OS is an open source operating system for automotive electronic/electrical devices based on the OSEK/VDX international standard. We present methods for converting the Trampoline kernel code into formal models and a series of experiments using an incremental verification approach. The conversion methods include functional modularization and treatment for hardware-dependent code, such as context-switching behavior. The incremental verification approach aims at increasing the level of confidence in the verification even when comprehensiveness cannot be provided due to the limitations of the hardware resource. We also report on a safety bug found in the Trampoline kernel during the experiments.