An approach for checking OSEK/VDX applications

Haitao Zhang; Toshiaki Aoki; Kenro Yatake; Min Zhang; Hsin Hung Lin

doi:10.1109/QSIC.2013.62

An approach for checking OSEK/VDX applications

Haitao Zhang, Toshiaki Aoki, Kenro Yatake, Min Zhang, Hsin Hung Lin

Research output: Contribution to conference › Paper › peer-review

3 Scopus citations

Abstract

With the growing demands for automotive auxiliary functions, more and more complex applications have been developed based on OSEK/VDX OS. However, how to completely check developed applications is becoming a challenge for developers. In this paper, we describe and develop an approach to check developed applications based on the SMT-based BMC. We have implemented a prototype tool and conducted some experiments. The experiments results show that our approach can be completely used to check the properties associated with (i) variables, (ii) mutual exclusion, (iii) service API and (iv) tasks execution sequences.

Original language	English
Pages	113-116
Number of pages	4
DOIs	https://doi.org/10.1109/QSIC.2013.62
State	Published - 2013
Externally published	Yes
Event	13th International Conference on Quality Software, QSIC 2013 - Nanjing, Jiangsu, China Duration: 29 Jul 2013 → 30 Jul 2013

Conference

Conference	13th International Conference on Quality Software, QSIC 2013
Country/Territory	China
City	Nanjing, Jiangsu
Period	29/07/13 → 30/07/13

Keywords

Bounded Model Checking
OSEK/VDX
SMT

Access to Document

10.1109/QSIC.2013.62

Cite this

@conference{2180f06f74774d37bb9cc503b8a43db5,

title = "An approach for checking OSEK/VDX applications",

abstract = "With the growing demands for automotive auxiliary functions, more and more complex applications have been developed based on OSEK/VDX OS. However, how to completely check developed applications is becoming a challenge for developers. In this paper, we describe and develop an approach to check developed applications based on the SMT-based BMC. We have implemented a prototype tool and conducted some experiments. The experiments results show that our approach can be completely used to check the properties associated with (i) variables, (ii) mutual exclusion, (iii) service API and (iv) tasks execution sequences.",

keywords = "Bounded Model Checking, OSEK/VDX, SMT",

author = "Haitao Zhang and Toshiaki Aoki and Kenro Yatake and Min Zhang and Lin, \{Hsin Hung\}",

year = "2013",

doi = "10.1109/QSIC.2013.62",

language = "英语",

pages = "113--116",

note = "13th International Conference on Quality Software, QSIC 2013 ; Conference date: 29-07-2013 Through 30-07-2013",

}

TY - CONF

T1 - An approach for checking OSEK/VDX applications

AU - Zhang, Haitao

AU - Aoki, Toshiaki

AU - Yatake, Kenro

AU - Zhang, Min

AU - Lin, Hsin Hung

PY - 2013

Y1 - 2013

N2 - With the growing demands for automotive auxiliary functions, more and more complex applications have been developed based on OSEK/VDX OS. However, how to completely check developed applications is becoming a challenge for developers. In this paper, we describe and develop an approach to check developed applications based on the SMT-based BMC. We have implemented a prototype tool and conducted some experiments. The experiments results show that our approach can be completely used to check the properties associated with (i) variables, (ii) mutual exclusion, (iii) service API and (iv) tasks execution sequences.

AB - With the growing demands for automotive auxiliary functions, more and more complex applications have been developed based on OSEK/VDX OS. However, how to completely check developed applications is becoming a challenge for developers. In this paper, we describe and develop an approach to check developed applications based on the SMT-based BMC. We have implemented a prototype tool and conducted some experiments. The experiments results show that our approach can be completely used to check the properties associated with (i) variables, (ii) mutual exclusion, (iii) service API and (iv) tasks execution sequences.

KW - Bounded Model Checking

KW - OSEK/VDX

KW - SMT

UR - https://www.scopus.com/pages/publications/84885576665

U2 - 10.1109/QSIC.2013.62

DO - 10.1109/QSIC.2013.62

M3 - 论文

AN - SCOPUS:84885576665

SP - 113

EP - 116

T2 - 13th International Conference on Quality Software, QSIC 2013

Y2 - 29 July 2013 through 30 July 2013

ER -

An approach for checking OSEK/VDX applications

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this