tイベントによる形式的仕様記述言語LOTOSへの時間概念の導入

概要

論文の詳細を見る
厳密な仕様を記述するために、各種の形式的記述技法(FDT:Formal Description Techniques)が提案されている。LOTOSもその1つで、ISO(国際標準化機構)で標準化がなされ、実行系も存在する形式的仕様記述言語である。LOTOSの形式的意味モデルはラベルつき付遷移システム(LTS)と呼ばれる有向グラフで与えられ、データを含まないBasic-LOTOSでLTSが有限であるものについてはLOTOS仕様の等価性(Weak-bisimulation)を機械的に判定するアルゴリズムも考案されている。しかし、LOTOSではイベント間の時間の間隔については考慮されていないためdelyやwait-until timeoutなどの時間に関連した仕様の記述が難しい。このため、LOTOSに時間の概念を導入する試みが多くなされてきている。その方法は時間をイベントとして扱う方法とタイムスタンブを用いる方法の大きく2通りに分かれている。後者の方法では時刻をデータとして定義して扱うため、データを扱わないというBasic-LOTOSの枠組を越えている。本稿では時刻の経過を表すtイベントという特別なイベントを導入する方法で拡張を行なう。この場合、2つの有限LTSの等価性の判定はBasic-LOTOSで用いられている方法で行なうことができる。
一般社団法人情報処理学会の論文
1993-09-27