リアルタイム分散協調システム設計のためのプロトコル合成に関する研究

点击翻译按钮获取中文摘要

近年,計算機ネットワークの発展に伴い,信頼性の高い分散協調システムの設計開発技法の確立が望まれている.このための一つの手法として,分散協調システム全体の要求仕様を形式的に記述し,要求仕様通りに動作する各ノード(計算機)の動作仕様(どのようなタイミングでどのノードとどのようなデータや同期用メッセージを交換しながら自ノードの動作を実行すべきかを記述したもの,プロトコル仕様と呼ばれる)を自動生成するためのプロトコル合成法の研究が進められている.一般に分散協調システムを設計する場合,繁雑なノード間の通信や同期制御などを行うプロトコル仕様を設計者自身が記述するのは繁雑であり間違いも起こりやすい.分散システムの設計法として,設計者は要求仕様のみを記述し,その仕様からプロトコル仕様を自動生成出来ることが望ましい.従来,多くのプロトコル合成法が考案されているが,これらの合成法では,分散環境でのプログラムの実行順序の制御に焦点が絞られてきた.しかし,リアルタイム分散協調システムでは時間制約が課される場合が多い.本研究では,時間制約を含む要求仕様からのプロトコル合成法を考案すると共に,考案した手法に基づいてプロトコル仕様を自動導出する処理系を作成し,その有効性を評価検討した.要求仕様としては,非隣接間の時間制約を整数線形不等式の論理結合で記述できるようなクラスを考えた.また,整数線形計画法の手法を用いて後続の処理がデッドロックしない範囲で,できるだけ自由度のある時間制約を先行する処理に与える工夫を行っている.