An abstract execution model for basic LOTOS

The paper presents some techniques that can be used for translating a LOTOS (language of temporal ordering specification) specification into an efficient implementation. In particular, it focuses attention on basic LOTOS, the control part of LOTOS, and presents a simple algorithm to derive an abstract machine based on a set of labelled transition systems from a basic LOTOS specification. The transition systems define interacting processes. The problem of the unbounded number of states is considered and solved, by allowing dynamic creation and destruction of processes and by adopting an appropriate construction procedure for the transition systems. The synchronisation of the processes, according to the LOTOS multi-way rendezvous mechanism, is obtained by means of a procedure based on message transfers among the processes, thus enabling a distributed implementation