通信プロセスモデルに基づく発展的プログラミングの研究

本年度は、通信プロセス指向プログラミング環境の証明手法の拡張について研究を行った。通信プロセスモデルに基づく実時間システムのプログラミング構築において、従来の方法および並行して進めているシステム構築から合成演算の扱いが重要であるという知見が得られている。このため、本年度は合成演算に注目し、特に、モデル検査を分割して効率的に行う手法について研究を行った。通信プロセスモデルにおける合成演算はP|Qのように書き、プロセスPとプロセスQが同期通信を行いながら並行に実行されることを表す。P|Qの性質を証明する場合、Pの性質とQの性質を独立に検査できれば、効率的に性質の証明ができる。しかし、一般にPとQは互いに相互作用しながら計算が進行するため、全く独立には検査できない。しかし、式の構造を再帰的に解析することにより、可能な相互作用をあらかじめ性質に反映させることによってできるだけ独立に証明を行う方法を示した。ここで、性質は拡張されたHennessy-Milner論理によって表す。この方法は一般的には従来の方法と変わらない手間が必要であるが、分岐全般に渡らない性質については有効な証明方法であることがわかった。本年度の研究は簡単のため、直接時間を扱わない体系についてまず行ったが、同様の方法は時間を導入したシステムにおいても適用可能である。

本年度は、通信プロセス指向プログラミング環境の証明手法の拡張について研究を行った。通信プロセスモデルに基づく実時間システムのプログラミング構築において、従来の方法および並行して進めているシステム構築から合成演算の扱いが重要であるという知見が得られている。このため、本年度は合成演算に注目し、特に、モデル検査を分割して効率的に行う手法について研究を行った。通信プロセスモデルにおける合成演算はP|Qのように書き、プロセスPとプロセスQが同期通信を行いながら並行に実行されることを表す。P|Qの性質を証明する場合、Pの性質とQの性質を独立に検査できれば、効率的に性質の証明ができる。しかし、一般にPとQは互いに相互作用しながら計算が進行するため、全く独立には検査できない。しかし、式の構造を再帰的に解析することにより、可能な相互作用をあらかじめ性質に反映させることによってできるだけ独立に証明を行う方法を示した。ここで、性質は拡張されたHennessy-Milner論理によって表す。この方法は一般的には従来の方法と変わらない手間が必要であるが、分岐全般に渡らない性質については有効な証明方法であることがわかった。本年度の研究は簡単のため、直接時間を扱わない体系についてまず行ったが、同様の方法は時間を導入したシステムにおいても適用可能である。