Assume-Guarantee形式による実時間ソフトウェアの演繹的詳細化検証手法
スポンサーリンク
概要
- 論文の詳細を見る
実時間ソフトウェアは外部環境との相互作用があり, タイミング制約が厳しく, 並行プロセスにより構成される.このために, 仕様やプログラムが正しいことを保証することは重要である.本論文では, 実時間ソフトウェアの仕様やプログラムの一般的なモデルである, Pnueliらのクロック遷移モジュール上において, 詳細化演繹的検証手法を提案する.なお, 提案する演繹的詳細化検証手法では, 状態空間の組み合わせ爆発を抑制するために, receptivenessを保証しながら, Assume-Guarantee形式による検証を実現する.最後に, 事例により, 本提案手法の有効性を示す.
- 一般社団法人電子情報通信学会の論文
- 2001-01-15
著者
関連論文
- ビデオ会議システムを用いた遠隔教育(教育における映像情報技術)
- プログラムスライシングによるプログラムのモデル検査手法
- 演繹的モデル検査による自動詳細化検証手法
- OSスケジューラプログラムの自動検証の実験的研究
- 制御ソフトウェアの開発方法論 : 制御理論と計算機科学の横断的設計アプローチ
- E-commerceソフトウェアの形式的開発方法論
- Assume-Guarantee形式による実時間ソフトウェアの演繹的詳細化検証手法
- 実時間システムの演繹的検証と自動検証の実験的研究
- 実時間システムの演繹的検証