WEKO3
アイテム
シミュレーション関係に基づくLOTOS仕様の検証アルゴリズム
https://ipsj.ixsq.nii.ac.jp/records/121926
https://ipsj.ixsq.nii.ac.jp/records/1219266a633ec4-35b1-4769-8b6b-399690c994b6
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
KJ00001343618.pdf (173.8 kB)
|
|
| Item type | National Convention(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 1992-09-28 | |||||
| タイトル | ||||||
| タイトル | シミュレーション関係に基づくLOTOS仕様の検証アルゴリズム | |||||
| タイトル | ||||||
| 言語 | en | |||||
| タイトル | A Verification Algorithm for LOTOS Specifications based on the Simulation Relation | |||||
| 言語 | ||||||
| 言語 | jpn | |||||
| 資源タイプ | ||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||
| 資源タイプ | conference paper | |||||
| 著者所属 | ||||||
| AIC | ||||||
| 著者所属 | ||||||
| AIC | ||||||
| 著者所属 | ||||||
| 東北大学 | ||||||
| 著者所属(英) | ||||||
| en | ||||||
| Advanced Intelligent Communication System Laboratories | ||||||
| 著者所属(英) | ||||||
| en | ||||||
| Advanced Intelligent Communication System Laboratories | ||||||
| 著者所属(英) | ||||||
| en | ||||||
| Tohoku University | ||||||
| 論文抄録 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | 近年、プロトコルなど通信システムの厳密な仕様化を行うために、各種の形式的記述技法(FDT:Formal Dedcription Techniques)が提案されている。このFDTの1つとして開発されたLOTOS(Language Of Temporal Orderimg Specification)は、数学的モデルをベースとしており記述・検証能力が高いため、その活用が期待されている。例えば、開発工程において弱双模倣(Weak-bisimulation)関係の概念を適用することにより、LOTOSで記述された上位レベルと下位レベルの2つの仕様間の無矛盾性の検証を行い、仕様が正しく詳細化されているかどうかを確認することが可能である。しかし、仕様の段階的な開発においては、複数の上位レベルの仕様を組み合わせて下位レベルの仕様を開発する場合や、下位レベルの仕様に上位レベルの仕様には含まれていない例外処理などの付加的な情報を加える場合がありうる。このような場合には、上記の弱双模倣等価関係は成立せず、むしろ片方向のシミュレーション関係を検証の概念として用いることが適当である。本報告では、まずシミュレーション関係の概念を示し、次にその判定アルゴリズムを示す。さらに適用例として、この判定アルゴリズムに基づいたLOTOS仕様の検証システムの槻要を示す。 | |||||
| 書誌レコードID | ||||||
| 収録物識別子タイプ | NCID | |||||
| 収録物識別子 | AN00349328 | |||||
| 書誌情報 |
全国大会講演論文集 巻 第45回, 号 ネットワーク, p. 169-170, 発行日 1992-09-28 |
|||||
| 出版者 | ||||||
| 言語 | ja | |||||
| 出版者 | 情報処理学会 | |||||
