|
平成21年度は、並行システムの理論(プロセス代数)CSPのための定理証明器CSP-Proverの利便性の改善と、記号処理による並行システム解析支援ツールCONPASUの研究と実装を行った。以下、各成果について説明する。
1.CSP-Proverの改善:
CSP-Proverは汎用定理証明器Isabelle上に実装したCSP理論であり、無限状態システムの特性を証明できる特徴があるが、その証明には人手が必要であり、その利便性の向上が課題になっていた。平成21年度はCSP-Proverの証明戦略を改善してCSP研究会で発表するとともに、その最新版をwebsiteから公開した。また、CSP-Proverのデータ表現の強化と、動作表現の拡張を行った成果が論文誌に採録された(ENTCS)。
2.CONPASU-toolの試作:
CSP-Proverの利便性は改善されてきているが、その証明手続きを完全に自動化することは困難である。そこで、定理証明器の記号処理的な証明方法とモデル検査器の自動検査方法の長所をもつ並行システム解析支援ツールCONPASUの研究開発に着手した。CONPASUは並行システムのモデルからその形式仕様を自動的に生成することを目標にしており、CSP-Proverの証明自動化を補助する外部ツールとしても使えると考えている。平成21年度は仕様の自動生成に必要な並行動作の逐次化機能をJavaで試作した。変数を有限値で具体化する代わりに記号処理を採用しているため、変域無限のデータも扱える特徴がある。その成果をPPL研究会とCSP研究会で発表した。
3.CSPの普及:
本研究の基礎として使われているCSP理論の普及を目指し、並行システムの検証と実装に関するチュートリアルを開発現場の技術者向けに行った。ここで受講生から得られた知見を本研究のツール開発にフィードバックできただけでなく、今後、本ツールの利用者獲得にもつながると期待している。
4.CSPの適用例:
CSPの適用例として、UMLのシーケンス図の検証に関する研究を行っている。平成21年度は、複数のシーケンス図を合成するための方法をCSPで形式的に検討するとともに、その方法をツール化してCST研究会にて発表した。
|
