Modularization of a specification in LOTOS

An algorithm for transforming LOTOS specifications from monolithic style to constraint-oriented style is proposed. The objective of this transformation is to decompose monolithic LOTOS behavior into two processes composed by the parallel operator. In order to make the behaviors observed congruent before and after the decomposition, the algorithm creates an additional process from the given specification and adds to the decomposed processes using a parallel operator. The additional process consists of n interleaved subprocesses (n ⩾ 1). There are no internal interaction gates between decomposed processes and the added process. The interactions among them occur only at the visible gates. This transformation has the following applications: (1) modularization or decomposition of a specification, (2) restructuring of complex specifications, and (3) derivation of protocol specifications from service specifications