異なる並列度をもつ並列プロセス間の変換手法

喜家村 奨 (9851202)


並列処理システムを設計する場合, 設計者はいくつかの部分的な 仕様を結合し, システム全体の振るまいを表す要求仕様を作成する. 仕様は,プロセスと環境間のインタフェイス情報と各成分プロセスの 動作定義からなると考えられる. インタフェイス情報とは, 成分プロセスの総数および各成分プロセスごとに その入出力イベントの集合(アルファベット)を定めたものである. 一方, プロセスの動作定義は遷移システム(LTS)で与えるものとする.
さて, 利用可能プロセス数や入出力ポートの配置などの実装上の制約から, 実装レベル仕様におけるプロセスと環境間のインタフェイス情報はあらか じめ決定されている場合が多い.
そこで,本発表では, 要求仕様および実装レベル仕様 における環境とのインタフェイス情報が与えられたとき, 各実装プロセスの 動作定義を与えるLTSを自動生成する方法について発表する.
また, 要求仕様と生成された実装レベル仕様の動作の等価性を証明, および, 実装レベル仕様において, プロセス間の同期のための内部メッセージ数 や各成分プロセスの状態数を減らす手法についても発表する.