プロセス代数の応用に関する研究

プロセス代数は,特に同期型通信システムのモデルとして有効であることが認識されているにもかかわらず,LOTOS以外実用面にまだほとんど応用されていない.本研究では,プロセス代数の理論を特に等価性に基づいて,同期型通信システムの検証などに応用するとともに,その応用面での可能性について考察した.通信システムの検証においては,対象とする状態数が爆発的に増加してしまうという大きな問題点が従来から指摘されて未解決となっている.本研究では,この問題に対する一つのアプローチとして,等価性の概念を用いて状態空間をそれと等価な状態数の少ないものへと変換し,変換後の状態空間に対して従来の検証法を適用することにより効率的に検証を行う手法を開発した.さらに,この変換を自動的に行うアルゴリズムを開発し,そのシステムを開発中である.また,大規模な仕様に関してはそれを適切にモジュール化することが重要な問題であるが,この問題に関しても等価性の立場から,複雑な仕様を簡単な幾つかの仕様が結合した形式に等価変換するための手法について考察した.その結果,強bisimulation等価の概念を用いると複雑な仕様をある程度自動的にモジュール化することが可能であった.しかし,強bisimulation等価の概念は等価性としては制限が強すぎ,仕様に柔軟性が失われるため,もう少し制限の緩い等価性を用いた融通性のある変換法の開発が今後の課題である.

プロセス代数は,特に同期型通信システムのモデルとして有効であることが認識されているにもかかわらず,LOTOS以外実用面にまだほとんど応用されていない.本研究では,プロセス代数の理論を特に等価性に基づいて,同期型通信システムの検証などに応用するとともに,その応用面での可能性について考察した.通信システムの検証においては,対象とする状態数が爆発的に増加してしまうという大きな問題点が従来から指摘されて未解決となっている.本研究では,この問題に対する一つのアプローチとして,等価性の概念を用いて状態空間をそれと等価な状態数の少ないものへと変換し,変換後の状態空間に対して従来の検証法を適用することにより効率的に検証を行う手法を開発した.さらに,この変換を自動的に行うアルゴリズムを開発し,そのシステムを開発中である.また,大規模な仕様に関してはそれを適切にモジュール化することが重要な問題であるが,この問題に関しても等価性の立場から,複雑な仕様を簡単な幾つかの仕様が結合した形式に等価変換するための手法について考察した.その結果,強bisimulation等価の概念を用いると複雑な仕様をある程度自動的にモジュール化することが可能であった.しかし,強bisimulation等価の概念は等価性としては制限が強すぎ,仕様に柔軟性が失われるため,もう少し制限の緩い等価性を用いた融通性のある変換法の開発が今後の課題である.