Modeling the execution of LOTOS specifications by cooperating extended finite state machines

The paper proposes an abstract execution model for LOTOS specifications, which is based on a number of cooperating extended finite state machines, applies to whatever LOTOS specification, with the only exclusion of those containing non well guarded recursion, and is suitable for a distributed implementation. Every machine represents a process, which does not necessarily correspond to one of the process definitions the specification is composed of. The machine instances (that is to say processes) can access variables, which correspond to LOTOS value identifiers, and can dynamically create new machine instances, thus enabling any infinite behaviour to be modeled. Synchronisation among the machines is achieved by a distributed algorithm which implements the multi-way rendezvous of LOTOS. The paper shows how the model is derived from LOTOS specifications and how it is executed