| 研究概要 |
平行分散アルゴリズム,認証プロトコルなどの問題領域において蓄積してきた振舞仕様の検証事例を,「適切な抽象度を持った振舞仕様の作成」ならびに「探索型と推論型の検証法の融合」の観点から分析し,以下の成果を得た.
1.適切な抽象度を持った振舞仕様の作成に関しては,どのような性質を解析・検証したいのかが仕様の抽象度の決定に大きく影響する点に着目し,以下の成果を得た.
(1)ブール代数や自然数などの,基本データ型は,いかなる抽象度の振舞仕様においても,特にその解析・検証において重要な役割を演ずることが明らかになった.これを受け,ブール代数や自然数を,その検証法(具体的にはCafeOBJの証明譜)と共に,基本ライブラリとして整理した.
(2)振舞仕様の安全性の検証が,状態遷移の回数に関する帰納法で行える事は,今までに蓄積した例題から実証されていた.これを発展させ,典型的な帰納法の検証パターンを整理体系化し,それに基づき帰納法の検証をモジュール化する技術を開発した.
2.探索型検証と推論方検証の融合に関しては,CafeOBJで書かれた振舞仕様をSMVまたはMaudeなどのモデルチェック器に変換する方法に焦点を当て.以下の成果を得た.
(1)SMVモデルチェッカに変換可能な観測遷移機械(OTS)のクラスを同定し,CafeOBJで記述されたOTS仕様からSMVへの変換プログラムを開発した.将来的には,この変換プログラムを使って,検証しようとしている命題が成立しないことを端的に示す反例の発見に役立てる計画である.
(2)cafeOBJで記述されたOTS仕様を,Maude言語のモデルチェッカに変換する変換システムの検討を行い,SMVへの変換に比べより効果的な検証補助になりうる可能性が高いとの知見を得た.
|
