時制論理に基づくプロトコルのLOTOS仕様の合成

• 安藤, 敏彦

• 加藤, 靖

• 高橋, 薫

• 野口, 正一

書誌事項

タイトル別名

• Compositional LOTOS Specification of Protocol Based on Temporal Logic
• プロトコルの記述と変換

抄録

プロトコル等、通信システムの仕様を曖昧なく記述するために、種々の形式記述技法が開発されている。これらの形式記述技法は数学的に厳密な取り扱いができる反面、記述が局所的であるために、仕様の大局的な振る舞いを陽に表現することができないという欠点がある。そのため、形式記述技法で記述された仕様が安全性、生存性等の時間的性質を満足しているかどうかを直観的に判断することは一般に困難である。一方、時系列上の性質を表現するために構成された論理体系が時制論理である。時制論理を用いると時間的性質を陽に表現することができ、大局的な振る舞いを理解しやすい。本論文では、形式記述技法の一つであるLOTOSを取り上げ、その意味を表すラベル付き遷移システム上で拡張分岐時制論理を定義する。そして、この論理で記述された時間的性質から、それを満足するLOTOS記述を導出する方法を提案する。さらに、より詳細な時間的性質を加えることで仕様を詳細化する方法も併せて提案する。これにより、時制論理を基礎とする段階的な仕様化が達成できる。また、時間的性質としてプロトコルの生存性を与えると、あるクラスのプロトコルのLOTOS仕様が得られ、この方法がプロトコルの仕様を与える上で有効であることを示す。

収録刊行物

• 情報処理学会論文誌

  情報処理学会論文誌 34 (6), 1268-1280, 1993-06-15

  一般社団法人情報処理学会

キーワード

• 特集：マルチメディア通信と分散処理

詳細情報

• CRID: 1050282812864551168
• NII論文ID: 110002722497
• NII書誌ID: AN00116647
• ISSN: 18827764
• Web Site: http://id.nii.ac.jp/1001/00014441/
• 本文言語コード: ja
• 資料種別: journal article
• データソース種別:
  • IRDB
  • CiNii Articles