SMT-based bounded model checking for OSEK/VDX applications

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

doi:10.1109/APSEC.2013.49

SMT-based bounded model checking for OSEK/VDX applications

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

15 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 check the developed applications is becoming a challenge for developers. Although some invaluable formal methods have been proposed to check actual software, these methods cannot be directly employed to check OSEK/VDX applications. In this paper, we describe and develop an approach to check OSEK/VDX applications using SMT-based bounded model checking. We also implement a prototype tool and conduct many experiments on several examples. The experiment results show that our approach can completely check the properties associated with (i) variables, (ii) mutual exclusion, (iii) service API, and (iv) tasks execution sequences of developed applications.

Original language	English
Title of host publication	APSEC 2013 - Proceedings of the 20th Asia-Pacific Software Engineering Conference
Editors	Pornsiri Muenchaisri, Gregg Rothermel
Publisher	IEEE Computer Society
Pages	307-314
Number of pages	8
ISBN (Electronic)	9781479921430
ISBN (Print)	9780769549224
DOIs	https://doi.org/10.1109/APSEC.2013.49
State	Published - 2013
Externally published	Yes
Event	20th Asia-Pacific Software Engineering Conference, APSEC 2013 - Bangkok, Thailand Duration: 2 Dec 2013 → 5 Dec 2013

Publication series

Name	Proceedings - Asia-Pacific Software Engineering Conference, APSEC
Volume	1
ISSN (Print)	1530-1362

Conference

Conference	20th Asia-Pacific Software Engineering Conference, APSEC 2013
Country/Territory	Thailand
City	Bangkok
Period	2/12/13 → 5/12/13

Keywords

Bounded model checking
OSEK/VDX
SMT

Access to Document

10.1109/APSEC.2013.49

Cite this

Zhang, H., Aoki, T., Lin, H. H., Zhang, M., Chiba, Y., & Yatake, K. (2013). SMT-based bounded model checking for OSEK/VDX applications. In P. Muenchaisri, & G. Rothermel (Eds.), APSEC 2013 - Proceedings of the 20th Asia-Pacific Software Engineering Conference (pp. 307-314). Article 6805420 (Proceedings - Asia-Pacific Software Engineering Conference, APSEC; Vol. 1). IEEE Computer Society. https://doi.org/10.1109/APSEC.2013.49

@inproceedings{b6cf357fe89e4c6c8a08703b4d81f594,

title = "SMT-based bounded model checking for 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 check the developed applications is becoming a challenge for developers. Although some invaluable formal methods have been proposed to check actual software, these methods cannot be directly employed to check OSEK/VDX applications. In this paper, we describe and develop an approach to check OSEK/VDX applications using SMT-based bounded model checking. We also implement a prototype tool and conduct many experiments on several examples. The experiment results show that our approach can completely check the properties associated with (i) variables, (ii) mutual exclusion, (iii) service API, and (iv) tasks execution sequences of developed applications.",

keywords = "Bounded model checking, OSEK/VDX, SMT",

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

note = "Publisher Copyright: {\textcopyright} 2013 IEEE.; 20th Asia-Pacific Software Engineering Conference, APSEC 2013 ; Conference date: 02-12-2013 Through 05-12-2013",

year = "2013",

doi = "10.1109/APSEC.2013.49",

language = "英语",

isbn = "9780769549224",

series = "Proceedings - Asia-Pacific Software Engineering Conference, APSEC",

publisher = "IEEE Computer Society",

pages = "307--314",

editor = "Pornsiri Muenchaisri and Gregg Rothermel",

booktitle = "APSEC 2013 - Proceedings of the 20th Asia-Pacific Software Engineering Conference",

address = "美国",

}

Zhang, H, Aoki, T, Lin, HH, Zhang, M, Chiba, Y & Yatake, K 2013, SMT-based bounded model checking for OSEK/VDX applications. in P Muenchaisri & G Rothermel (eds), APSEC 2013 - Proceedings of the 20th Asia-Pacific Software Engineering Conference., 6805420, Proceedings - Asia-Pacific Software Engineering Conference, APSEC, vol. 1, IEEE Computer Society, pp. 307-314, 20th Asia-Pacific Software Engineering Conference, APSEC 2013, Bangkok, Thailand, 2/12/13. https://doi.org/10.1109/APSEC.2013.49

SMT-based bounded model checking for OSEK/VDX applications. / Zhang, Haitao; Aoki, Toshiaki; Lin, Hsin Hung et al.
APSEC 2013 - Proceedings of the 20th Asia-Pacific Software Engineering Conference. ed. / Pornsiri Muenchaisri; Gregg Rothermel. IEEE Computer Society, 2013. p. 307-314 6805420 (Proceedings - Asia-Pacific Software Engineering Conference, APSEC; Vol. 1).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - SMT-based bounded model checking for OSEK/VDX applications

AU - Zhang, Haitao

AU - Aoki, Toshiaki

AU - Lin, Hsin Hung

AU - Zhang, Min

AU - Chiba, Yuki

AU - Yatake, Kenro

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 check the developed applications is becoming a challenge for developers. Although some invaluable formal methods have been proposed to check actual software, these methods cannot be directly employed to check OSEK/VDX applications. In this paper, we describe and develop an approach to check OSEK/VDX applications using SMT-based bounded model checking. We also implement a prototype tool and conduct many experiments on several examples. The experiment results show that our approach can completely check the properties associated with (i) variables, (ii) mutual exclusion, (iii) service API, and (iv) tasks execution sequences of developed applications.

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 check the developed applications is becoming a challenge for developers. Although some invaluable formal methods have been proposed to check actual software, these methods cannot be directly employed to check OSEK/VDX applications. In this paper, we describe and develop an approach to check OSEK/VDX applications using SMT-based bounded model checking. We also implement a prototype tool and conduct many experiments on several examples. The experiment results show that our approach can completely check the properties associated with (i) variables, (ii) mutual exclusion, (iii) service API, and (iv) tasks execution sequences of developed applications.

KW - Bounded model checking

KW - OSEK/VDX

KW - SMT

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

U2 - 10.1109/APSEC.2013.49

DO - 10.1109/APSEC.2013.49

M3 - 会议稿件

AN - SCOPUS:84929621962

SN - 9780769549224

T3 - Proceedings - Asia-Pacific Software Engineering Conference, APSEC

SP - 307

EP - 314

BT - APSEC 2013 - Proceedings of the 20th Asia-Pacific Software Engineering Conference

A2 - Muenchaisri, Pornsiri

A2 - Rothermel, Gregg

PB - IEEE Computer Society

T2 - 20th Asia-Pacific Software Engineering Conference, APSEC 2013

Y2 - 2 December 2013 through 5 December 2013

ER -

Zhang H, Aoki T, Lin HH, Zhang M, Chiba Y, Yatake K. SMT-based bounded model checking for OSEK/VDX applications. In Muenchaisri P, Rothermel G, editors, APSEC 2013 - Proceedings of the 20th Asia-Pacific Software Engineering Conference. IEEE Computer Society. 2013. p. 307-314. 6805420. (Proceedings - Asia-Pacific Software Engineering Conference, APSEC). doi: 10.1109/APSEC.2013.49

SMT-based bounded model checking for OSEK/VDX applications

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this