|
本年度は、通信プロセス指向プログラミング環境の視覚的インタフェースおよび証明手法の拡張について研究を行った。視覚的インタフェースについては、通信プロセスの抽象的モデルであるラベル付き遷移系を直観的に画面上に表示し、検証するツールを作成した。具体的な形式的体系としては、MilnerのCCSを対象とする。本ツールの作成において問題となった点は、プロセス代数における合成の扱いである。プロセス代数における合成演算は状態の組合せによる増大を招く。このため、組合せを展開した形では、状態数が増加し、視覚的に表現しても直観的な理解は難しくなる。
このため、本研究で作成したツールでは、各モジュール毎に分解した形で表示する。さらに、本ツールでは、仕様と実現がテスト等価性の意味で等価でない場合、その原因となる状態を表示する。この際、各モジュールに分解した形で表示することによってより直観的に理解することができる。しかし、以下にあげる問題があった。
●原因となる状態が各モジュールの組合せとなること。
●組合せによって発散が発生すること。
●仕様と等価にするための修正の組合せが一意でないこと。
これらの問題を解決するため、CCSの展開定理を拡張し、合成演算の展開の際にサブモジュール情報を保存する方法を示した。この拡張定理をもとに検証ツールを作成した。
ツールの作成により、合成演算を展開せずに扱うことの有効性が確認できた。しかし、合成演算の扱いは本質的に複雑であり、ユーザに対してはより直観的な提示が必要である。
実際のコード生成については、π計算についての検討を行ったが、動的な構造を効果的にコードに変換することについては、オペレーティングシステムとのインタフェースにおいて困難な点が多く、プロトタイプを作成するにとどまった。
|
