本年は、従来から継続していた通信プロセスモデルの組込みソフトウェアによるモデル化とその解析技術に関する研究の発表、コレオグラフィーに基づく分散システムの記述体系として家電ネットワークの振舞いをモデル化した。さらに、高信頼な実現のための関数型言語による実現手法についても研究を行った。 具体的内容は以下の通りである。 (1)AIBOロボットソフトウェアの振舞いをプロセス計算体系の一つであるπ計算によってモデル化し、デッドロックの発生の可能性をモデル上で検出する手法を示した。動作コンポーネントの分割により、実際的な時間でデッドロックの検出が可能であることを示した。 (2)ネットワーク家電の振舞いをプロセス計算に基づいて記述した。全体的な振舞いから個々の家電機器の振舞いを分割して導出することが可能であることを示し、さらに、実際の記述に対しては優先度を導入して意味論と分割手法を拡張した。 (3)π計算の記述を直接的に関数型言語Haskellに変換する手法を示した。πmonadoによってπ項をそのまま入力として、プログラムの整合性をHaskell型システムによって直接的に記述可能になっている。本年は、実際的なネットワークアプリケーションを記述してその有効性に対して検討を行った。 これらの技法を統合していくことで、本研究の目的であるコレオグラフィーによる分散環境における高信頼なソフトウェアの実現が可能である。今後は、家電ネットワークと車載ソフトウェアに対する応用を主眼に研究を進める計画である。
|