Derivation of Executable Code from Formal Protocol Specifications Written in LOTOS

A novel tool for generating implementation prototypes of communication protocols and concurrent systems specified using the ISO LOTOS language is presented. LOTOS specifications are analyzed and translated into C functions that are executed by cooperating processes in the UNIX environment. The set of LOTOS process definitions is first translated into a suitable number of extended finite state machines (EFSMs). The proposed method makes it possible to circumvent the problem of deriving unbounded EFSMs and to obtain a sort of control on the process number/size tradeoff at the same time. The problem of implementing the LOTOS multi-way rendezvous mechanism for process synchronization is solved by an algorithm based on message passing. An example of prototype derivation is also introduced showing the form of C code generated by translating a simple specification