On Specifying Protocols Based on LOTOS and Temporal Logic

Toshihiko ANDO  Yasushi KATO  Kaoru TAKAHASHI  

Publication
IEICE TRANSACTIONS on Communications   Vol.E77-B   No.8   pp.992-1006
Publication Date: 1994/08/25
Online ISSN: 
DOI: 
Print ISSN: 0916-8516
Type of Manuscript: PAPER
Category: Signaling System and Communication Protocol
Keyword: 
protocol specification,  formal specification technique,  

Full Text: PDF(1009.8KB)>>
Buy this Article




Summary: 
We propose a method which can construct LOTOS specifications of communication systems from temporal properties 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.