SDL記述のプロトコル検証のためのモデル

概要

論文の詳細を見る
信頼性の高い通信システムを設計するためには、信号の送受信規則(プロトコル)の正当性を仕様の段階で検証するプロトコル検証は重要な技術である。しかし、多くのプロトコル検証技術は単純なプロトコルモデル(状態遷移モデル)の上で研究され、SDLの様な拡張有限状態機械(EFSM)に基づく仕様記述言語で記述されたプロトコルには簡単に適用できないという問題点がある。プロトコル検証における最も基本的なモデルは、プロセス(Process)間のチャネル(channel)を通してやりとりされる信号(signal)の送信(send)及び受信(receive)によりプロセスの状態(state)が遷移するFSMに基づく状態遷移モデルである。本稿では、これを基本プロトコルモデルと呼ぶ。多くのプロトコル検証技術は、この基本プロトコルモデルをもとに研究されている。ー方、実システムのプロトコルは、SDLなどのEFSMに基づく仕様記述言語を用いて記述されることが多い。そこで、基本プロトコルモデルをもとに研究されたプロトコル検証技術をEFSMに基づく仕様記述言語で記述された仕様に容易に適用可能とするため、新しいプロトコルモデルを提示し、このプロトコルモデルに変換する方法を提案する。本稿では、EFSMに基づく仕様記述言語としてSDLを例にとり、SAVE機能を中心にプロトコルモデルに変換する方法を示す。
一般社団法人情報処理学会の論文
1993-09-27

SDL記述のプロトコル検証のためのモデル

スポンサーリンク

概要

著者

関連論文

スポンサーリンク