並列プログラムに現れる非同期型通信のプロセス代数による解析・検証

2002 Fiscal Year Annual Research Report

• Project/Area Number: 14540121
• Research Institution: Ehime University
• Principal Investigator: 大塚 寛 愛媛大学, 理学部, 助教授 (30203839)
• Keywords: 協調型言語 / プロセス代数 / 軌跡 / モデル検証 / 可達性解析

Research Abstract

今年度の研究では、一般の並列プロセスを制限された協調型言語を用いて記述し、タプル空間の状態遷移とプロセスの軌跡によるモデル検証を試み、その評価として実験を中心に従来方法との比較を行った。
モデル検証は調べたい性質が満たされているか否かを、有限状態機械(FSM)の状態空間を探索することによって調べる。この探索は可達性解析、すなわち与えられた初期状態から到達できる各状態において論理テストを行うことが基本となるが、ここで問題になるのは"状態空間爆発問題"である。特に一般の並列プロセスをモデル化した複数個のFSMが通信しあいながら並列に動作する状況では、FSMの並列合成において状態空問の直積をとることにより、状態空問の爆発が起こる。そこで本研究では一般の並列プロセスではなく、協調型言語のin, out, rd操作を持つ各直列プロセスとタプル空間の組み合わせを対象としたモデル検証について検討した。具体的には以下の手順ですすめた。
1.プロセス間の通信を、プロセスとプロセスの間に配置したタプル空間の通信に置き換える。
2.プロセス間の通信を、in, out, rd操作とタプル空間の状態の組による軌跡によってモデル化する。
今回の実験に合わせてデッドロックが起こる(安全性が満たされない)ような状況の軌跡による記述を行った。
3.相手側のプロセスの軌跡とタプル空間の状態遷移を組み合わせ、これと手元のプロセスの軌跡により状態空間の爆発を抑えてモデル検証を行う。ただしこれはまだ実験のみで、理論的根拠は示すには至っていない。
2.を中心とした内容は研究集会「2002年度冬のLAシンポジウム」で、3.を中心とした内容は情報処理学会「第65回全国大会」で口頭報告した。