Premium
Model checking Trampoline OS: a case study on safety analysis for automotive software
Author(s) -
Choi Yunja
Publication year - 2014
Publication title -
software testing, verification and reliability
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.216
H-Index - 49
eISSN - 1099-1689
pISSN - 0960-0833
DOI - 10.1002/stvr.1482
Subject(s) - computer science , trampoline , context (archaeology) , model checking , automotive industry , software , software engineering , functional safety , embedded system , reliability engineering , operating system , programming language , engineering , aerospace engineering , paleontology , computer network , biology
SUMMARY Model checking is an effective technique used to identify subtle problems in software safety using a comprehensive search algorithm. However, this comprehensiveness requires a large number of resources and is often too expensive to be applied in practice. This work strives to find a practical solution to model‐checking automotive operating systems for the purpose of safety analysis, with minimum requirements and a systematic engineering approach for applying the technique in practice. The paper presents methods for converting the Trampoline kernel code into formal models for the model checker SPIN, a series of experiments using an incremental verification approach, and the use of embedded C constructs for performance improvement. The conversion methods include functional modularization and treatment for hardware‐dependent code, such as memory access for context switching. The incremental verification approach aims at increasing the level of confidence in the verification even when comprehensiveness cannot be provided because of the limitations of the hardware resource. We also report on potential safety issues found in the Trampoline operating system during the experiments and present experimental evidence of the performance improvement using the embedded C constructs in SPIN. Copyright © 2012 John Wiley & Sons, Ltd.