The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
자동차 제어 시스템에서는 전기전자 제어 기술의 발전으로 인해 소프트웨어 복잡성이 증가함에 따라 소프트웨어 결함의 잠재적 위험이 증가하고 있습니다. 경쟁 조건과 같은 일부 종류의 결함은 테스트나 시뮬레이션을 통해 거의 감지되지 않습니다. 이러한 결함은 일부 드문 실행에서만 나타나기 때문입니다. 철저한 상태 공간 탐색을 사용하는 모델 검사는 이러한 결함을 탐지하는 데 효과적입니다. 이 문서에서는 실제 자동차 제어 프로그램에 모델 검사 기술을 적용하는 방법에 대해 보고합니다. 이러한 프로그램은 크기가 크고 복잡하기 때문에 직접 모델링 확인하는 것은 불가능합니다. 따라서 검증 중인 프로그램에서 모델 검사가 가능한 모델을 도출하는 것이 필요합니다. 우리의 접근 방식은 SPIN 모델 검사기와 이 프로세스를 용이하게 하는 내부 도구를 사용합니다. 이러한 도구에 구현된 주요 기능 중 하나는 경계 조정이 가능한 프로그램 슬라이싱으로, 이를 통해 사용자는 관심 있는 검증 문제와 관련된 소스 코드의 일부를 지정하고 추출할 수 있습니다. 추출된 코드를 SPIN의 입력 언어인 Promela로 변환하는 작업은 도구 중 하나를 사용하여 반자동 방식으로 수행됩니다. 이 접근 방식은 실제로 수년 동안 사용되었으며 소프트웨어의 코드 크기가 400KLOC를 초과하는 경우에도 유용한 것으로 밝혀졌습니다.
Masahiro MATSUBARA
Hitachi Automotive Systems, Ltd.,Osaka University
Tatsuhiro TSUCHIYA
Osaka University
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.
부
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
부
@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},}
부
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 -