制御系ECU調停器の検証における演繹的アプローチについて

• Item type: SIG Technical Reports(1)
• 公開日: 2008-06-12
• タイトル: 制御系ECU調停器の検証における演繹的アプローチについて
• タイトル / 言語: en
• タイトル: Verifications of an arbiter for electronic control units with an interactive theorem prover
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 東京工業大学大学院情報理工学研究科／産業技術総合研究所システム検証研究センター
• 著者所属: （株）豊田中央研究所
• 著者所属: （株）豊田中央研究所
• 著者所属(英): en
• 著者所属(英): Tokyo Institute of Technology / Institute of Advanced Industrial Science and Technology
• 著者所属(英): en
• 著者所属(英): Toyota Central R&D Labs., Inc.
• 著者所属(英): en
• 著者所属(英): Toyota Central R&D Labs., Inc.
• 著者名: 湯浅, 能史; 足立, 正和; 佐野, 範佳
• 著者名(英): Yoshifumi, Yuasa; Masakazu, Adachi; Noriyoshi, Sano
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 組み込みソフトウェアの検証技術としては、従来のソフトウェアテストに加えて、近年ではモデル検査法も注目されている。これらは、入力例に対する振る舞いを調べて確認する、いわば実証的な検証法である。これと双璧をなす古典的な形式検証技術として、定理証明による演繹的手法が知られているが、事例報告は現状では少い。本研究では、車載システム検証の一事例として、電子制御ユニット(ECU)の調停器の幾つかの性質を、対話的定理証明器 Agda を用いて演繹的に検証したので、それについて報告する。
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: As a method for verifying embedded softwares, various software tests are widely used. Some model checking methods also have become popular in recent years. All these are inductive methods in the sense that we verify a program by tracing and examining many (or all) executions with it. On the other hand, not many cases of verifications of embedded softwares by deductive methods are reported. In this paper, we report a case study of verifications of automotive softwares by deductive methods. We show some basic properties of an arbiter for electronic control units with an interactive theorem prover Agda.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10112981
• 書誌情報: 情報処理学会研究報告ソフトウェア工学（SE）; 巻 2008, 号 55(2008-SE-160), p. 41-47, 発行日 2008-06-12
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会