時間ペトリネットの拡張モデルを用いたプロトコル合成

スポンサーリンク

概要

論文の詳細を見る
動作の実行時刻に制約のある分散システムのサービス仕様(システム全体が1計算機で実行されるとしたときのその計算機の仕様)から計算機間の通信遅延を考慮してもその制約を満足するプロトコル仕様(実際の計算機ごとの仕様の組)を自動合成する手法を提案する。提案手法では、多くのリアルタイムシステムの仕様記述、検証に用いられている時間ペトリネットに基づくモデルを用い、従来手法において必要とされていた計算機間での同期時計を必要としないプロトコル仕様を合成できる。また、状態変数を含むサービス仕様からの合成もできる。サービス仕様を満足するプロトコル仕様が存在するかどうかを判定することや、存在する場合にある評価基準のもとで最適なプロトコル仕様であるかどうかを保証することは容易ではないが、本手法ではそれらの問題を線形計画問題に帰着し、それらを機械的に判定、求解する工夫をしている。本手法を用いることで、計算機間の通信遅延を直接計算することなく仕様記述が行えると考えられる。
1998-03-15

著者

関連論文

もっと見る

スポンサーリンク