Details page | Paper / Information search system

Search

Search help

Summary & Details

Model Checking of Automotive Software with CBMC

CBMCによる車載ソフトウェアのモデル検査

Delivery: Available on this site

Format: PDF

Price: Non-members (tax incl.)：￥1,100 Members (tax incl.)：￥880

Publication code: 20265032

Paper/Info type: Proceedings (Spring)

No.7-26

Pages: 1-6(Total 6 p)

Date of publication: May 2026

Publisher: JSAE

Language: Japanese

Event: 2026 JSAE Annual Congress (Spring)

Detailed Information

Author(J)	1) 三治真也, 2) 黄文鴻
Author(E)	1) Shinya Miharu, 2) Wenhung Huang
Affiliation(J)	1) デンソー, 2) デンソー
Affiliation(E)	1) DENSO, 2) DENSO
Abstract(J)	車載ソフトウェアの大規模化・複雑化に伴い，既存検証プロセスでは発見困難なバグが増加している．本研究ではモデル検査に着目し，車載ソフトウェアの検証プロセスへの適用手法を提案する．また，社内事例を用いて適用性を評価した結果，および今後の展望について報告する． Translation
Abstract(E)	As automotive software becomes larger and more complex, bugs that are difficult to detect with existing verification processes are increasing. This study focuses on model checking and proposes a method for applying it to the verification process of automotive software. Furthermore, we report the results of evaluating its applicability using internal case studies, as well as future prospects.

About search

How to use the search box

You can enter up to 5 search conditions. The number of search boxes can be increased or decreased with the "+" and "-" buttons on the right.

If you enter multiple words separated by spaces in one search box, the data that "contains all" of the entered words will be searched (AND search).

Example) X (space) Y → "X and Y (including)"

How to use "AND" and "OR" pull-down

If "AND" is specified, the "contains both" data of the phrase entered in the previous and next search boxes will be searched. If you specify "OR", the data that "contains" any of the words entered in the search boxes before and after is searched.

Example) X AND Y → "X and Y (including)" X OR Z → "X or Z (including)"

If AND and OR searches are mixed, OR search has priority.

Example) X AND Y OR Z → X AND (Y OR Z)

If AND search and multiple OR search are mixed, OR search has priority.

Example) W AND X OR Y OR Z → W AND (X OR Y OR Z)

How to use the search filters

Use the "search filters" when you want to narrow down the search results, such as when there are too many search results. If you check each item, the search results will be narrowed down to only the data that includes that item.

The number in "()" after each item is the number of data that includes that item.

Search tips

When searching by author name, enter the first and last name separated by a space, such as "Taro Jidosha".