制御系ECU調停器の検証における演繹的アプローチについて(組込みシステム技術)
スポンサーリンク
概要
- 論文の詳細を見る
組み込みソフトウェアの検証技術としては、従来のソフトウェアテストに加えて、近年ではモデル検査法も注目されている。これらは、入力例に対する振る舞いを調べて確認する、いわば実証的な検証法である。これと双壁をなす古典的な形式検証技術として、定理証明による演繹的手法が知られているが、事例報告は現状では少い。本研究*では、車載システム検証の一事例として、電子制御ユニット(ECU)の調停器の幾つかの性質を、対話的定理証明器Agdaを用いて演繹的に検証したので、それについて報告する。
- 一般社団法人情報処理学会の論文
- 2008-06-12
著者
-
佐野 範佳
(株)豊田中央研究所
-
湯浅 能史
東京工業大学大学院情報理工学研究科
-
足立 正和
(株)豊田中央研究所
-
湯浅 能史
東京工業大学大学院情報理工学研究科:産業技術総合研究所システム検証研究センター
関連論文
- ハイブリッドオートマトンの双模倣関係とその近似計算
- 自動車用コンピュータにおける制御タイミング仕様記述方法の検討
- 制御系ECU調停器の検証における演繹的アプローチについて(組込みシステム技術)
- AS-4-6 I/Oオートマトンのモジュラ制御における調停問題について(離散事象システムとモデル検査,AS-4.組込みシステムの形式的手法,シンポジウム)
- 離散事象システムのモジュラ状態フィードバック制御に対する調停器設計(ペトリネット,離散事象システム,一般)
- LTLで記述されるマニュアルに対するオートメーションサプライズの検出
- 同期型言語を用いたソフトウェア検証 : クルーズコントロールシステムにおける事例紹介(フォーラム)
- 最大デッドロックフリー可制御部分述語の計算とその警報器設計への応用(システムと制御)
- AS-5-3 時間付きオートマトンでモデル化された人間-機械系におけるオートメーションサプライズの一検証法(AS-5. コンカレントシステムとハイブリッドシステムのための形式モデルとその応用, 基礎・境界)
- 制御系ECU調停器の検証における演繹的アプローチについて(組込みシステム技術)
- 離散事象システムにおけるオートメーションサプライズに対する警報器の設計
- 回路変換における照合手法
- 2914 オブジェクト指向型シミュレータを用いた機械加工用設備モデルライブラリ
- 対称性を有する区分的アフィンシステムにおけるリミットサイクルの解析
- A-2-13 対称性を有する区分アファインシステムにおけるリミットサイクルの解析
- プロセスモデリングのための標準スキーマ"EPML"の提案と,シミュレーションプロセスへの応用
- 制御ソフトウェアの開発方法論 : 制御理論と計算機科学の横断的設計アプローチ
- 車載電子制御システムの障害診断手法 : WPMax-SATを利用したCANデータ特異関係の抽出(ディペンダブルシステム,組込み技術とネットワークに関するワークショップETNET2011)
- 車載電子制御システムの障害診断手法 : WPMax-SATを利用したCANデータ特異関係の抽出(ディペンダブルシステム,組込み技術とネットワークに関するワークショップETNET2011)