シミュレーション関係に基づくLOTOS仕様の検証アルゴリズム

概要

論文の詳細を見る
近年、プロトコルなど通信システムの厳密な仕様化を行うために、各種の形式的記述技法(FDT:Formal Dedcription Techniques)が提案されている。このFDTの1つとして開発されたLOTOS(Language Of Temporal Orderimg Specification)は、数学的モデルをベースとしており記述・検証能力が高いため、その活用が期待されている。例えば、開発工程において弱双模倣(Weak-bisimulation)関係の概念を適用することにより、LOTOSで記述された上位レベルと下位レベルの2つの仕様間の無矛盾性の検証を行い、仕様が正しく詳細化されているかどうかを確認することが可能である。しかし、仕様の段階的な開発においては、複数の上位レベルの仕様を組み合わせて下位レベルの仕様を開発する場合や、下位レベルの仕様に上位レベルの仕様には含まれていない例外処理などの付加的な情報を加える場合がありうる。このような場合には、上記の弱双模倣等価関係は成立せず、むしろ片方向のシミュレーション関係を検証の概念として用いることが適当である。本報告では、まずシミュレーション関係の概念を示し、次にその判定アルゴリズムを示す。さらに適用例として、この判定アルゴリズムに基づいたLOTOS仕様の検証システムの槻要を示す。
一般社団法人情報処理学会の論文
1992-09-28

シミュレーション関係に基づくLOTOS仕様の検証アルゴリズム

スポンサーリンク

概要

著者

関連論文

スポンサーリンク