1993年6月15日
時制論理に基づくプロトコルのLOTOS仕様の合成
情報処理学会論文誌
- ,
- ,
- ,
- 巻
- 34
- 号
- 6
- 開始ページ
- 1268
- 終了ページ
- 1280
- 記述言語
- 日本語
- 掲載種別
- 出版者・発行元
- 一般社団法人情報処理学会
プロトコル等、通信システムの仕様を曖昧なく記述するために、種々の形式記述技法が開発されている。これらの形式記述技法は数学的に厳密な取り扱いができる反面、記述が局所的であるために、仕様の大局的な振る舞いを陽に表現することができないという欠点がある。そのため、形式記述技法で記述された仕様が安全性、生存性等の時間的性質を満足しているかどうかを直観的に判断することは一般に困難である。一方、時系列上の性質を表現するために構成された論理体系が時制論理である。時制論理を用いると時間的性質を陽に表現することができ、大局的な振る舞いを理解しやすい。本論文では、形式記述技法の一つであるLOTOSを取り上げ、その意味を表すラベル付き遷移システム上で拡張分岐時制論理を定義する。そして、この論理で記述された時間的性質から、それを満足するLOTOS記述を導出する方法を提案する。さらに、より詳細な時間的性質を加えることで仕様を詳細化する方法も併せて提案する。これにより、時制論理を基礎とする段階的な仕様化が達成できる。また、時間的性質としてプロトコルの生存性を与えると、あるクラスのプロトコルのLOTOS仕様が得られ、この方法がプロトコルの仕様を与える上で有効であることを示す。
- リンク情報
-
- CiNii Articles
- http://ci.nii.ac.jp/naid/110002722497
- CiNii Books
- http://ci.nii.ac.jp/ncid/AN00116647
- URL
- http://id.nii.ac.jp/1001/00014441/
- ID情報
-
- ISSN : 1882-7764
- CiNii Articles ID : 110002722497
- CiNii Books ID : AN00116647