時制論理を用いた並列性を含むLOTOS仕様の導出

• Item type: SIG Technical Reports(1)
• 公開日: 1992-12-14
• タイトル: 時制論理を用いた並列性を含むLOTOS仕様の導出
• タイトル / 言語: en
• タイトル: Derivation of LOTOS Specification Including Parallelism Using Temporal Logic
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 仙台電波工業高等専門学校
• 著者所属: 仙台電波工業高等専門学校
• 著者所属: 東北大学電気通信研究所
• 著者所属: 東北大学応用情報学研究センター
• 著者所属(英): en
• 著者所属(英): Sendai National College of Technology
• 著者所属(英): en
• 著者所属(英): Sendai National College of Technology
• 著者所属(英): en
• 著者所属(英): Research Institute of Electrical Communication, Tohoku University
• 著者所属(英): en
• 著者所属(英): Research Center for Applied Information Sciences, Tohoku University
• 著者名: 安藤, 敏彦; 加藤, 靖; 高橋, 薫; 野口, 正一
• 著者名(英): Toshihiko, Ando; Yasushi, Kato; Kaoru, Takahashi; Shoichi, Noguchi
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 形式記述技法の一つであるLOTOSでは安全性，生存性等の大局的な時間的性質を陽に記述することはできない．そこで本論文では，ラベル付き遷移システムから得られるアクション系列集合をモデルとする時制論理を用いることにより，時間的性質を陽に記述し，与えられた時間的性質からLOTOS仕様を導出する方法を提案する．この方法では，構成的な手続きを用いており，仕様をあるクラスに制限することができる．また，並列プロセスを記述することも可能なので，全体のプロセスを小さなサブプロセスに分割することで，仕様化が容易になる．また，この方法がプロトコルの仕様化にも有効であることを示す．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: It is not easy to describe global temporal properties, such as safety property and/or liveness property, explicitly in LOTOS, one of the formal description techniques. So, we propose the compositional method that derives a LOTOS specification from temporal properties. Temporal properties are described based on the temporal logic of which the model is a set of action sequences induced from a labelled transition system. It is able to obtain a desirable class of specifications using this method. It also becomes easy to specify a large process because this method can derive parallel processes. We show an application of this method to a protocol as an example.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10112981
• 書誌情報: 情報処理学会研究報告ソフトウェア工学（SE）; 巻 1992, 号 100(1992-SE-089), p. 33-40, 発行日 1992-12-14
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会