実時間システムの演繹的検証と自動検証の実験的研究

スポンサーリンク

概要

論文の詳細を見る
実時間システムは外部環境と相互作用があり, タイミング制約が厳しく, 並行プロセスにより構成される.このため仕様が正しいことを保証することが重要である.本論文では, 時間ステートチャートを用いて, 並行性やタイミング制約, 機能の統合的な仕様記述を行う.さらに, Pnueliらのクロック遷移システムにより, 時間ステートチャートの意味を定義する.それを基にして, 演繹的証明により, 時間ステートチャートが安全性や活性を充足することが検証できることを示す.最後に, 時間ステートチャートを抽象化して, 時間オートマシンのシンボリック検証器KRONOSを使い, 自動演繹的検証ができることを示す.そして, 演繹的検証と自動演繹的検証を実験的に評価して, 定量的に, 自動演繹的検証が優れていることを示す.
一般社団法人情報処理学会の論文
2000-05-12

著者

関連論文

スポンサーリンク