On Specifying Protocols Based on LOTOS and Temporal Logic
スポンサーリンク
概要
- 論文の詳細を見る
We propose a method which can construct LOTOS specifications of communication systems from temporal properies described in Extended branching time temporal logic (EBTL) in this paper. Description of LOTOS, one of Formal Description Techniques, is based on behaviors of systems so that LOTOS permits strict expression. However, it is difficult to express temporal properties explicitly. On the other hand, Temporal logic is based on properties of systems. Thus temporal logic permits direct expression of temporal properties which can be understood intuitively. Accordingly, temporal logic is more useful than FDTs on the first step of systems specification. This method is effective in this point of view. Specifications obtained using this method can have a structured style. When temporal properties are regarded as constraints about temporal order among actions of systems, those specification can have a constraint oriented style. This method is based on sequential composition of Labelled Transition Systems (LTSs) which are semantics of LOTOS. EBTL is also defined on LTSs. In general, many LTSs satisfy the same temporal property. To obtain such the minimal LTS, the standard form of LTSs corresponding to EBTL operators are defined. Those standard LTSs are mainly tailored to the field of communication protocol. We also show conditions that original temporal properties are preserved in case of sequential composition of standard LTSs. In addition, applying this method to the Abracadabra Protocol, we show that this method can construct specifications of concrete protocols effectively.
- 社団法人電子情報通信学会の論文
- 1994-08-25
著者
-
TAKAHASHI Kaoru
Sendai National College of Technology
-
KATO Yasushi
Sendai National College of Technology
-
Takahashi K
The Sendai National College Of Technology
-
Ando Toshihiko
Sendai National College Of Technology
-
Takahashi Kaoru
AIC Systems Labs.
関連論文
- Composition of Service and Protocol Specifications in Asynchronous Communication System(Networks)
- Progressive pulmonary calcification after successful renal transplantation
- State Machine Specification with Reusability(Concurrent Systems)(Concurrent Systems and Hybrid Systems)
- Specification and Analysis of the Contract Net Protocol Based on State Machine Model(Special Section on Concurrent System Technology and Its Application to Multiple Agent Systems)
- On Constructing n-Entities Communication Protocol and Service with Alternative and Concurrent Functions(Special Section on Concurrent System Technology and Its Application to Multiple Agent Systems)
- Specification of a Concurrent System Based on Propositional Logic (特集:マルチメディア通信と分散処理)
- Composition of Protocol Functions(Special Section on Concurrent Systems Technology)
- Specification and Validation of a Dynamically Reconfigurable System(Special Section on Concurrent Systems Technology)
- A Concurrent Calculus with Geographical Constraints(Special Section on Concurrent Systems Technology)
- Making Changes in Formal Protocol Specifications
- A Topological Framework of Stepwise Specification for Concurrent Systems (Special Section on Description Models for Concurrent Systems and Their Applications)
- On Specifying Protocols Based on LOTOS and Temporal Logic
- A Consideration Of Integrated System Management In OSI Environment
- An Improvement of The Protocol Synthesis Algorithm
- Performance Analysis on the Controllable Slotted DS-CDMA with an Allocating Buffer for Collided Traffic(Satellite Communications)
- A Compositional Approach for Constructing Communication Services and Protocols (Special Section on Concurrent Systems Technology)
- An Error Detection Method for Recursive Processes for LOTOS Instruction and Its Support System
- A Flexible Verifier of Temporal Properties for LOTOS
- Modeling, Verification and Testing of Web Applications Using Model Checker