Formal Treatment of Data Structures in Concurrency Models
Nicolas Guelfi, Fabrice Mourlin · 1996
Data Types). The operational semantics of Lotos is defnied in terms of labelled transition system. Lotos can be used to specify all the allowed behaviour of a system (the set of all behaviours that can be observed during execution of a conforming implementation). Lotos permits this without describing how an implementation might be achieved, or by describing particular mechanisms that achieve the required behaviour. Lotos is therefore appropriate for the specification of a composition of processes which have input, output. A specification Lotos is structured syntactically in term of a header line, global type definitions, a global behaviour 6 expression followed by type definitions and process definitions: Specification spec-name [gate-list ] (param list): function type definitions Behaviour behaviour expression Where type definition process definition endspec spec-name indicates the name of the specification, gate list is the names of interactions points of the specificatio...