2024-03-28T20:55:40Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:000144412022-10-21T05:24:51Z00581:00781:00788
時制論理に基づくプロトコルのLOTOS仕様の合成Compositional LOTOS Specification of Protocol Based on Temporal Logicjpn特集:マルチメディア通信と分散処理http://id.nii.ac.jp/1001/00014441/Journal Articlehttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=14441&item_no=1&attribute_id=1&file_no=1Copyright (c) 1993 by the Information Processing Society of Japanプロトコルの記述と変換仙台電波工業高等専門学校仙台電波工業高等専門学校東北大学電気通信研究所東北大学応用情報学研究センター安藤, 敏彦加藤, 靖高橋, 薫野口, 正一プロトコル等、通信システムの仕様を曖昧なく記述するために、種々の形式記述技法が開発されている。これらの形式記述技法は数学的に厳密な取り扱いができる反面、記述が局所的であるために、仕様の大局的な振る舞いを陽に表現することができないという欠点がある。そのため、形式記述技法で記述された仕様が安全性、生存性等の時間的性質を満足しているかどうかを直観的に判断することは一般に困難である。一方、時系列上の性質を表現するために構成された論理体系が時制論理である。時制論理を用いると時間的性質を陽に表現することができ、大局的な振る舞いを理解しやすい。本論文では、形式記述技法の一つであるLOTOSを取り上げ、その意味を表すラベル付き遷移システム上で拡張分岐時制論理を定義する。そして、この論理で記述された時間的性質から、それを満足するLOTOS記述を導出する方法を提案する。さらに、より詳細な時間的性質を加えることで仕様を詳細化する方法も併せて提案する。これにより、時制論理を基礎とする段階的な仕様化が達成できる。また、時間的性質としてプロトコルの生存性を与えると、あるクラスのプロトコルのLOTOS仕様が得られ、この方法がプロトコルの仕様を与える上で有効であることを示す。AN00116647情報処理学会論文誌346126812801993-06-151882-77642009-06-29