
The concurrent nature of these systems and its complexity, together with the diversity, specificity, and difficulty to manage make necessary the use of formal models to design them. It will be show that Petri Nets can be used for this purpose if some methodological considerations are introduced. In this sense, the methodology is based on three basic steps. The first step propose an abstraction process of the system to be designed allowing to obtain modular models that they are structurally characterised. After that, specific liveness results are obtained for this class of models in such a way that they can be used in the third step that it is devoted to the synthesis of live models.