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

Derivation of Executable Code from Formal Protocol Specifications Written in LOTOS / Valenzano, Adriano; Sisto, Riccardo; Ciminiera, Luigi. - STAMPA. - (1991), pp. 346-352. (Intervento presentato al convegno Tenth Annual International Phoenix Conference on Computers and Communications tenutosi a Scottsdale, Arizona, USA nel March 1991) [10.1109/PCCC.1991.113832].

Derivation of Executable Code from Formal Protocol Specifications Written in LOTOS

VALENZANO, ADRIANO;SISTO, Riccardo;CIMINIERA, Luigi
1991

Abstract

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
1991
0818621338
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11583/2500031
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo