ログインしてください

文献・情報検索システム

日本語

ENGLISH

ヘルプ

ログインしてください

  • 詳細情報

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

Model Checking of Automotive Software with CBMC

書誌事項

著者1) 三治 真也, 2) 黄 文鴻
著者(英)1) Shinya Miharu, 2) Wenhung Huang
勤務先1) デンソー, 2) デンソー
勤務先(英)1) DENSO, 2) DENSO
抄録車載ソフトウェアの大規模化・複雑化に伴い,既存検証プロセスでは発見困難なバグが増加している.本研究ではモデル検査に着目し,車載ソフトウェアの検証プロセスへの適用手法を提案する.また,社内事例を用いて適用性を評価した結果,および今後の展望について報告する.
抄録(英)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.

翻訳

検索について

閉じる

検索ボックスの使い方

検索条件は最大5件まで入力可能です。検索ボックスの数は右側の「+」「−」ボタンで増減させることができます。
一つの検索ボックス内に、複数の語句をスペース(全角/半角)区切りで入力した場合、入力した語句の“すべてを含む”データが検索されます(AND検索)。
例)X(スペース)Y →「XかつY(を含む)」

「AND」「OR」プルダウンの使い方

「AND」を指定すると、前後の検索ボックスに入力された語句の“双方を含む”データが検索されます。また、「OR」を指定すると、前後の検索ボックスに入力された語句の“いずれかを含む”データが検索されます。
例)X AND Y →「XかつY(を含む)」  X OR Z →「XまたはZ(を含む)」
AND検索とOR検索が混在する場合は、OR検索が優先されます。
例)X AND Y OR Z → X AND (Y OR Z)
AND検索と複数のOR検索が混在する場合も、OR検索が優先されます。
例)W AND X OR Y OR Z → W AND (X OR Y OR Z)

検索フィルタの使い方

検索結果の件数が多すぎる場合など、さらに絞り込みしたいときに「検索フィルタ」を使います。各項目にチェックを入れると、その項目が含まれるデータのみに検索結果が絞り込まれます。
各項目後ろの「()」内の数字は、その項目が含まれるデータの件数です。

検索のコツ

著者名で検索するときは、「自動車 太郎」のように、姓名をスペースで区切って入力してください。