研究内容

高信頼ネットワークコンピューティングのための並行計算モデル

概要：ネットワークコンピューティングとはネットワークで相互に接続された多数の計算機上で並行に分散実行される計算のことである。インターネットをはじめとする計算機ネットワークは現在の社会において欠かすことのできない基盤となり、ネットワークコンピューティングを実現する並行分散システムには高い信頼性が求められる。ネットワークコンピューティングにおける特徴は、実行前の入力と実行終了後の出力だけでなく、実行途中に発生する入出力でプログラムの振舞いを捉えなければならない点にある。さらに、分散実行においては全体を同期するメカニズムを与えることが困難であるので実行順序の非決定性に基づくプログラムの非決定性が本質的に存在する。本研究は、以上のような特徴を持つネットワークコンピューティングを従来とは異なる計算モデルで体系化することで、ネットワークコンピューティングの振舞いを定式化し、ネットワークシステムの信頼性を向上させることを目的とする。このために、通信プロセスモデルに基づくネットワークソフトウェアの定式化と解析技術の開発を行なっている。

研究テーマ：
(1) 通信プロセスモデルの時間拡張
通信プロセスモデルは、複数のプロセスが相互に同期通信を行いながら計算が進行する計算モデルである。本研究では、通信プロセスモデルとして90年代から研究が進められているπ計算を対象とする。従来のπ計算には実行において時間の概念が明示的に導入されていない。時間経過を意味に明示的に導入することでネットワークソフトウェアをより正確にモデル化する。時間を含めた体系におけるプロセスの等価性と代数的構造としての合同性について研究を進めている。
(2) Webアプリケーションの振舞いモデル
Webアプリケーションは、URLによる要求に対して各コンポーネントが状態を持ちながら並行に実行される。このとき、コンポーネントの合成において、入出力にもとづく関数合成よりも一般的な通信プロセスモデルに基づく合成によって全体の構成を捉える技法について研究する。このモデル化によって振舞いモデルを構築することでモデル検査などの手法に基づいてWebアプリケーションの信頼性向上を図ることができる。
(3) 通信プロセスモデルに基づく計算機言語
通信プロセスモデルのメカニズムに基づく高抽象度の言語とターゲット環境に対応する低抽象度の言語への変換を研究することによって並行プログラムにおける振舞いの動作解析技法を開発している。ここでは、プログラミング言語の意味論解析と言語処理系の開発を並行して行っている。
(4) 組込ソフトウェアの形式的計算モデル
組込システムのためのソフトウェアは高度化が進み、実時間の並行プロセスの集合体として構築されるようになっている。特に組込システムでは資源および計算パワーにおいて制約が大きい。通信プロセスモデルに基づいたモデル化を与えることで、詳細な動作解析のための基盤技術を開発する。

今後の展開：本研究では、通信プロセスモデルを核となる計算モデルとして、Webアプリケーションなどの実際的なネットワークコンピューティングにおいて信頼性のあるプログラムを実現するための基本的モデルを提案する。今後、特に注目する応用として以下の２つのシステムに注目する。
Webアプリケーションの動作モデルとしての定式化：現存するWebアプリケーションの振舞いを通信モデルにもとづいて定式化して（特に非決定的な）問題点を指摘できるようにすること、さらに、本モデルに基づいたWebアプリケーションの構成手法について研究する。
組込ソフトウェアの定式化：小規模のシステムにおいて、その振舞いをできるだけ詳細にモデル化することを目標とする。機械的な検証を可能とするために、検証したい性質のための抽象化技法を研究する。