Model Checking of Automotive Control Software: An Industrial Approach

Masahiro MATSUBARA; Tatsuhiro TSUCHIYA

doi:10.1587/transinf.2019FOP0002

Model Checking of Automotive Control Software: An Industrial Approach

Masahiro MATSUBARA, Tatsuhiro TSUCHIYA

Full Text Views

0

Cite this

Summary :

In automotive control systems, the potential risks of software defects have been increasing due to growing software complexity driven by advances in electric-electronic control. Some kind of defects such as race conditions can rarely be detected by testing or simulations because these defects manifest themselves only in some rare executions. Model checking, which employs an exhaustive state-space exploration, is effective for detecting such defects. This paper reports our approach to applying model checking techniques to real-world automotive control programs. It is impossible to directly model check such programs because of their large size and high complexity; thus, it is necessary to derive, from the program under verification, a model that is amenable to model checking. Our approach uses the SPIN model checker as well as in-house tools that facilitate this process. One of the key features implemented in these tools is boundary-adjustable program slicing, which allows the user to specify and extract part of the source code that is relevant to the verification problem of interest. The conversion from extracted code into Promela, SPIN's input language, is performed using one of the tools in a semi-automatic manner. This approach has been used for several years in practice and found to be useful even when the code size of the software exceeds 400 KLOC.

Publication: IEICE TRANSACTIONS on Information Vol.E103-D No.8 pp.1794-1805

Publication Date: 2020/08/01

Publicized: 2020/03/30

Online ISSN: 1745-1361

DOI: 10.1587/transinf.2019FOP0002

Type of Manuscript: Special Section PAPER (Special Section on Formal Approaches)

Category: Formal Approaches

Authors

Masahiro MATSUBARA
Hitachi Automotive Systems, Ltd.,Osaka University
Tatsuhiro TSUCHIYA
Osaka University

Keyword

model checking, program slicing, automotive control systems, SPIN model checker

Cite this

Copy

Masahiro MATSUBARA, Tatsuhiro TSUCHIYA, "Model Checking of Automotive Control Software: An Industrial Approach" in IEICE TRANSACTIONS on Information, vol. E103-D, no. 8, pp. 1794-1805, August 2020, doi: 10.1587/transinf.2019FOP0002.
Abstract: In automotive control systems, the potential risks of software defects have been increasing due to growing software complexity driven by advances in electric-electronic control. Some kind of defects such as race conditions can rarely be detected by testing or simulations because these defects manifest themselves only in some rare executions. Model checking, which employs an exhaustive state-space exploration, is effective for detecting such defects. This paper reports our approach to applying model checking techniques to real-world automotive control programs. It is impossible to directly model check such programs because of their large size and high complexity; thus, it is necessary to derive, from the program under verification, a model that is amenable to model checking. Our approach uses the SPIN model checker as well as in-house tools that facilitate this process. One of the key features implemented in these tools is boundary-adjustable program slicing, which allows the user to specify and extract part of the source code that is relevant to the verification problem of interest. The conversion from extracted code into Promela, SPIN's input language, is performed using one of the tools in a semi-automatic manner. This approach has been used for several years in practice and found to be useful even when the code size of the software exceeds 400 KLOC.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2019FOP0002/_p

Copy

@ARTICLE{e103-d_8_1794,
author={Masahiro MATSUBARA, Tatsuhiro TSUCHIYA, },
journal={IEICE TRANSACTIONS on Information},
title={Model Checking of Automotive Control Software: An Industrial Approach},
year={2020},
volume={E103-D},
number={8},
pages={1794-1805},
abstract={In automotive control systems, the potential risks of software defects have been increasing due to growing software complexity driven by advances in electric-electronic control. Some kind of defects such as race conditions can rarely be detected by testing or simulations because these defects manifest themselves only in some rare executions. Model checking, which employs an exhaustive state-space exploration, is effective for detecting such defects. This paper reports our approach to applying model checking techniques to real-world automotive control programs. It is impossible to directly model check such programs because of their large size and high complexity; thus, it is necessary to derive, from the program under verification, a model that is amenable to model checking. Our approach uses the SPIN model checker as well as in-house tools that facilitate this process. One of the key features implemented in these tools is boundary-adjustable program slicing, which allows the user to specify and extract part of the source code that is relevant to the verification problem of interest. The conversion from extracted code into Promela, SPIN's input language, is performed using one of the tools in a semi-automatic manner. This approach has been used for several years in practice and found to be useful even when the code size of the software exceeds 400 KLOC.},
keywords={},
doi={10.1587/transinf.2019FOP0002},
ISSN={1745-1361},
month={August},}

Copy

TY - JOUR
TI - Model Checking of Automotive Control Software: An Industrial Approach
T2 - IEICE TRANSACTIONS on Information
SP - 1794
EP - 1805
AU - Masahiro MATSUBARA
AU - Tatsuhiro TSUCHIYA
PY - 2020
DO - 10.1587/transinf.2019FOP0002
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E103-D
IS - 8
JA - IEICE TRANSACTIONS on Information
Y1 - August 2020
AB - In automotive control systems, the potential risks of software defects have been increasing due to growing software complexity driven by advances in electric-electronic control. Some kind of defects such as race conditions can rarely be detected by testing or simulations because these defects manifest themselves only in some rare executions. Model checking, which employs an exhaustive state-space exploration, is effective for detecting such defects. This paper reports our approach to applying model checking techniques to real-world automotive control programs. It is impossible to directly model check such programs because of their large size and high complexity; thus, it is necessary to derive, from the program under verification, a model that is amenable to model checking. Our approach uses the SPIN model checker as well as in-house tools that facilitate this process. One of the key features implemented in these tools is boundary-adjustable program slicing, which allows the user to specify and extract part of the source code that is relevant to the verification problem of interest. The conversion from extracted code into Promela, SPIN's input language, is performed using one of the tools in a semi-automatic manner. This approach has been used for several years in practice and found to be useful even when the code size of the software exceeds 400 KLOC.
ER -