IEICE TRANSACTIONS on Information
Verifying OSEK/VDX Applications: A Sequentialization-Based Model Checking Approach
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.
- Publication
- IEICE TRANSACTIONS on Information Vol.E98-D No.10 pp.1765-1776
- Publication Date
- 2015/10/01
- Publicized
- 2015/07/06
- Online ISSN
- 1745-1361
- DOI
- 10.1587/transinf.2015EDP7043
- Type of Manuscript
- PAPER
- Category
- Software System
Authors
Haitao ZHANG
Japan Advanced Institute of Science and Technology (JAIST)
Toshiaki AOKI
Japan Advanced Institute of Science and Technology (JAIST)
Yuki CHIBA
Japan Advanced Institute of Science and Technology (JAIST)
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Haitao ZHANG, Toshiaki AOKI, Yuki CHIBA, "Verifying OSEK/VDX Applications: A Sequentialization-Based Model Checking Approach" in IEICE TRANSACTIONS on Information,
vol. E98-D, no. 10, pp. 1765-1776, October 2015, doi: 10.1587/transinf.2015EDP7043.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2015EDP7043/_p
Copy
@ARTICLE{e98-d_10_1765,
author={Haitao ZHANG, Toshiaki AOKI, Yuki CHIBA, },
journal={IEICE TRANSACTIONS on Information},
title={Verifying OSEK/VDX Applications: A Sequentialization-Based Model Checking Approach},
year={2015},
volume={E98-D},
number={10},
pages={1765-1776},
abstract={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.},
keywords={},
doi={10.1587/transinf.2015EDP7043},
ISSN={1745-1361},
month={October},}
Copy
TY - JOUR
TI - Verifying OSEK/VDX Applications: A Sequentialization-Based Model Checking Approach
T2 - IEICE TRANSACTIONS on Information
SP - 1765
EP - 1776
AU - Haitao ZHANG
AU - Toshiaki AOKI
AU - Yuki CHIBA
PY - 2015
DO - 10.1587/transinf.2015EDP7043
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E98-D
IS - 10
JA - IEICE TRANSACTIONS on Information
Y1 - October 2015
AB - 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.
ER -
English
