Verifying OSEK/VDX Applications: A Sequentialization-Based Model Checking Approach

Haitao ZHANG  Toshiaki AOKI  Yuki CHIBA  

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E98-D   No.10   pp.1765-1776
Publication Date: 2015/10/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.2015EDP7043
Type of Manuscript: PAPER
Category: Software System
Keyword: 
OSEK/VDX applications,  Formal Software Verification,  deterministic scheduler,  sequentialization,  

Full Text: PDF>>
Buy this Article




Summary: 
OSEK/VDX, a standard for an automobile OS, has been widely adopted by many manufacturers to design and develop a vehicle-mounted OS. With the increasing functionalities in vehicles, more and more complex applications are be developed based on the OSEK/VDX OS. However, how to ensure the reliability of developed applications is becoming a challenge for developers. To ensure the reliability of developed applications, model checking as an exhaustive technique can be applied to discover subtle errors in the development process. Many model checkers have been successfully applied to verify sequential software and general multi-threaded software. However, it is hard to directly use existing model checkers to precisely verify OSEK/VDX applications, since the execution characteristics of OSEK/VDX applications are different from the sequential software and general multi-threaded software. In this paper, we describe and develop an approach to translate OSEK/VDX applications into sequential programs in order to employ existing model checkers to precisely verify OSEK/VDX applications. The value of our approach is that it can be considered as a front-end translator for enabling existing model checkers to verify OSEK/VDX applications.