| 研究概要 |
平成20年度では、並行システム検証ツール(定理証明器)CSP-Proverの使い易さの改善を目指し、操作的意味論の実装、証明コマンドの強化、CSP-Proverの拡張等を行った。以下、各成果について説明する。
1.操作的意味論の試験的実装と適用実験:CSP-Prover上にプロセス代数CSPの操作的意味論、到達可能状態導出アルゴリズム、弱双模倣等価性判定アルゴリズムを実装し、テスト用の例題に適用した結果について研究会で発表した(TPP,PPL)。この適用実験によって、検証自動化の可能性を確認することができたが、その検証時間が予想以上にかかることも判明した。平成21年度は、より効率的な等価性判定アルゴリズムの調査/研究を行う。
2.証明コマンドの強化:理論上は必須ではないが、証明の自動化に向けて補助的な規則を証明し、それらを証明コマンドに組み込んで証明の自動化を進めた。その証明コマンドをスケーラブル(プロセス数可変)な自己組織化分散システムの検証に適用してその効果を確認し、本成果を条件付き採録となっていた論文に追加して発表した(JSSST)。
3.CSP-Proverの拡張:本科研費研究のベースとなっているCSP-Proverはスウォンジー大学(ウェールズ、UK)との共同研究で開発しているツールであり、CSP-Proverの改善は本研究の成果にもつながる。CSP-Proverのデータ表現の強化と、動作表現の拡張を行い発表した(AVoCS 2件)。
4.検証技術:本科研費研究の基本理論として使われているプロセス代数CSPの普及を目指し、CSP研究会でその概要を紹介した(CSP)。また、大規模システムの検証についての発表も行った(PPL)。
|
