| 研究概要 |
われわれは,これまで,様相μ計算を用いた抽象化を基礎としたソフトウェア検証技法を研究してきた.その枠組みでは,主に安全性に分類される性質の検証を行えるようになったが,本研究では,それをさらに発展させ,より広い性質の検証をめざしたもので,具体的には,活性に分類される性質が対象となっている.
本年度は,まず,抽象化技法の適用に関する理論的な基礎を整備した.具体的には,クリプキ構造に関する基本的な変換操作を定義し,様相μ計算の論理式で表現される条件について,これらの変換操作に関する,最弱事前条件と最強事後条件が,ふたたび,様相μ計算の論理式で表現されることを証明し,その計算方法をを確立した.このことを用いて,これらの変換に関し,後向きおよび前向きの推論を行うことが可能となった.Hoare論理と組み合わせることで,アルゴリズムの検証ができる.
つづいて,N∞値クリプキ構造における様相μ計算のモデル検査法を開発した.検査法は従来も知られていたが,まず,従来法にあった「含意を含まない」という制限を撤廃し,適用範囲を広げ,さらに,従来法の適用可能な範囲についても,計算量を削減した.また,検査法の正当性証明を改良して,見通しの良いものとした.
本研究全体としては,同じ設定における充足可能性判定手続きを見いだすことが目標である.2値の様相μ計算に関する理論がそうであるように,充足可能性判定を行う手法は,モデル検査法がそのベースとなる可能性が高いと考えられる.その観点から,今回の検査法は重要な一歩である.しかし,現在の検査法には,(今回拡張した範囲について)計算量の評価ができていないという問題がある.今後,この解明が可能なように,アルゴリズム自体を改良する研究をすすめる計画である.
|
