Abstract:In this paper, based on the LOTOS specification language, the authors present the transformation which starts from the functional specification and the distributed properties of target system to the corresponding modular specification. The authors present the tagged specification to represent the complex distributed properties of the full LOTOS specifications and study the decomposition transformation of full LOTOS specification which using the broadcasting communication gates in the system's internal coordinating communications and directly decomposing the multiple subsets.