A NEW APPROACH FOR PROTOCOL SYNTHESIS BASED ON LOTOS

In communication protocols, the behaviour of a protocol entity is rela ted to the behaviour of another protocol entity as they communicate un der sets of communication rules (protocols). Thus, it is desirable to concentrate on the design of one protocol entity and generate the corr esponding protocol entity automatically. Furthermore, it is desirable that the protocol is formal, precise and unambiguous that is, it is de scribed using FDTs (Formal Description Techniques). In this paper, we propose a protocol synthesis algorithm in which, from a LOTOS specific ation of a single given entity, LOTOS specification of the correspondi ng peer entity is generated automatically. Unlike previous works, wher e FSMs (Finite State Machines) were used to synthesize protocols, we u se LOTOS, which is one of FDTs developed by ISO, in our proposed synth esis 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.