オートマトン理論に基づくリアルタイムソフトウェアの検証システム

概要

論文の詳細を見る
リアルタイムソフトウェアはプロセス構成が複雑でタイミング制約が厳しいために, タイミング制約を含む形式的検証に関する多くの研究が行われている.そこで,我々は時間ステートチャートによる仕様記述と検証の手法について報告した.本手法では,言語包合アルゴリズムにより公平性や正則性の検証を実現したが,検証コストが大きすぎる問題点がある. その原因としては,初期状態からの受理ループ探索や状態遷移関係をリスト構造で表現したことによる.本論文では,検証コストを削減するために,以下の効率的なタイミング検証手法を提案する.(1)タイミング制約の充足性を判定しながら,受理条件を充足する強連結成分を探索して,強連結成分が初期状態から到達可能かどうかを判定することにより,計算コストを削減する.(2)状態遷移関係を二分決定グラフで表現して, タイミング制約の充足性を判定しながら,像計算することにより,計算コストとメモリコストを削減する.本論文では, 上記手法を支援するタイミング検証システムを実現して,その有効性を確認した.
一般社団法人情報処理学会の論文
1996-01-18