制約指向モデルで記述された対称性を持つ並行システムの要求仕様に対する形式的検証とプロトコル合成

スポンサーリンク

概要

論文の詳細を見る
本研究では、グループワークなどネットワークを介した対称性を持つ並行システムの仕様記述のための制約指向モデルと効率の良いデッドロックの検出法、ならびに、システム全体の動作仕様(サービス仕様)から各ノードの動作仕様群(プロトコル仕様)を自動導出するための一つのプロトコル合成法を提案する。提案する手法では、記述スタイルは制約指向モデルを採用し、並行システム全体の動作仕様を色つきペトリネットの集合とその間の同期指定で記述する。また、状態間の同値関係を自動的に検出して高速に可達性判定を行う検証系を作成した。また、提案モデルにおけるプロトコル合成法を考案し実装を行った。
一般社団法人情報処理学会の論文
2001-03-21

著者

関連論文

もっと見る

スポンサーリンク