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

1998 Fiscal Year Annual Research Report

• Project/Area Number: 10139219
• Research Institution: Nagoya University
• Principal Investigator: 結縁 祥治 名古屋大学, 情報メディア教育センター, 助教授 (70230612)
• Keywords: 並行計算モデル / CCS / モデル検査 / 通信プロセスモデル / Hennessy-Milner論理 / 不動点意味論 / 証明系 / 弱双模倣関係

Research Abstract

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

Research Products

• [Publications] 結縁祥治: "テスト等価性に基づいた視覚的LTSモデル操作によるプロセス代数デバッガ" 電子情報通信学会技術報告コンピューテーション. COMP 97-89. 17-24 (1998)
• [Publications] 結縁祥治: "通信プロセスに対する文脈変換手法を用いたモデル検査" 電子情報通信学会技術報告コンピュテーション. COMP 98-82. 81-88 (1999)