| 研究概要 |
平成20年度は, 代数仕様言語CafeOBJ上で実現したモジュラーな書換えシステムに基づく検証システムの事例研究を通し, その有効性を確かめた. また構築し検証システムの発展のため, 以下の各項目について研究を行った. それぞれ研究成果を電子情報通信学会論文誌に発表した.
(1) 等式仕様の実行エンジンの基礎理論 : 項書換えに基づく等式推論エンジンの基礎となる項のマッチング技術を提案した. 項の簡約の効率化には不必要な書き換えをできるだけ避け, 必要に応じて(オンデマンドに)書き換えを行う必要がある.本提案のオンデマンドマッチングは, システムに応じてユーザがマッチング順序を切り替え可能なこと, すべての書き換え規則を同時に比較すること, などの特徴を持ち, 既存の関連技術ではうまく扱えないシステムを扱うことが可能となった.
(2) 検証システムの融合技術 : システムを抽象度の高い振る舞いのレベルで捉えて仕様を記述する振舞仕様からより具体的に捉える書換仕様への変換手法を提案した. 振舞仕様では証明譜に基づく対話的な検証手法が行われ, 書換仕様では綱羅探索やモデル検査による全自動検索が行われる.振舞仕様を制限する形で具体的な書換仕様に変換することで, 検証したい性質に対する反例の発見など検証の手助けを得ることが可能になった.
(3) 形式仕様からの実装を支援するツール開発 : 記号計算による仕様の形式検証では, 設計レベルの安全性を数学的に保証できたとしても, 最終成果物となる実装の安全性は保証されない. 実装レベルの安全性には, ソフトウェアテストの技術が有効である. 本研究では, 検証済みの形式仕様から実装(スケルトン)への自動変換およびテスト自動生成を行うツールを開発した, 検証結果を利用することで, 安全性を保証するためのテストケース群を系統的に得ることが可能となった.
以上により, 効率的な検証エンジン, 種々の検証システムの融合, 仕様から実装への変換技術などを支援する検証システム・形式言語につながる重要な研究成果が得られた.
|
