状態遷移表のモデル検査におけるLTL検証パターン(実装,検証,報告)
スポンサーリンク
概要
- 論文の詳細を見る
ソフトウェア設計の品質向上の技術として形式手法,特にモデル検査が注目されているが,産業界への普及のためには,開発者にとって使いやすいツールの提供が必要である.そこで,筆者らは状態遷移表に基づくモデル検査の支援環境を構築した.本稿では,状態遷移表のモデル検査で使用されるLTL(Linear Temporal logic)の検証パターンについて議論し,モデル検査支援環境による,パターン化されたLTL検査式の自動生成と自動検査の有用性について評価する.
- 2009-03-11