TY - JOUR
T1 - New approach for protocol synthesis based on LOTOS
AU - Bista, Bhed Bahadur
AU - Cheng, Zixue
AU - Togashi, Atsushi
AU - Shiratori, Norio
PY - 1994/10
Y1 - 1994/10
N2 - In communication protocols, the behaviour of a protocol entity is related to the behaviour of another protocol entity as they communicate under sets of communication rules (protocols). Thus, it is desirable to concentrate on the design of one protocol entity and generate the corresponding protocol entity automatically. Furthermore, it is desirable that the protocol is formal, precise and unambiguous that is, it is described using FDTs (Formal Description Techniques). In this paper, we propose a protocol synthesis algorithm in which, from a LOTOS specification of a single given entity, LOTOS specification of the corresponding peer entity is generated automatically. Unlike previous works, where FSMs (Finite State Machines) were used to synthesize protocols, we use LOTOS, which is one of FDTs developed by ISO, in our proposed synthesis algorithm. We prove that the generated protocol is logical errors free, collectively represented as deadlock free, if the given entity is in certain forms which are natural in the context of communication protocols.
AB - In communication protocols, the behaviour of a protocol entity is related to the behaviour of another protocol entity as they communicate under sets of communication rules (protocols). Thus, it is desirable to concentrate on the design of one protocol entity and generate the corresponding protocol entity automatically. Furthermore, it is desirable that the protocol is formal, precise and unambiguous that is, it is described using FDTs (Formal Description Techniques). In this paper, we propose a protocol synthesis algorithm in which, from a LOTOS specification of a single given entity, LOTOS specification of the corresponding peer entity is generated automatically. Unlike previous works, where FSMs (Finite State Machines) were used to synthesize protocols, we use LOTOS, which is one of FDTs developed by ISO, in our proposed synthesis algorithm. We prove that the generated protocol is logical errors free, collectively represented as deadlock free, if the given entity is in certain forms which are natural in the context of communication protocols.
UR - http://www.scopus.com/inward/record.url?scp=0028530369&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0028530369&partnerID=8YFLogxK
M3 - Article
AN - SCOPUS:0028530369
VL - E77-A
SP - 1646
EP - 1655
JO - IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences
JF - IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences
SN - 0916-8508
IS - 10
ER -