The focus of this research is formal validation and verification of the orchestration (the sequencing) of services. This approach uses a Petri net derived formalism called Timed Net Condition Event Systems (TNCES) which has been chosen due to its modular and composable nature. A basis of TNCES modules has been created to represent a set of eight constructs capable of expressing workflow-related features such as multithreading, synchronization, looping and sequencing. A separate bag of modules has been developed as an extension to the core set to enrich its modelling power with ability of describing Boolean and temporal conditions that may arise in conjunction with looping constructs. This paper focuses on the means of automatically generating each TNCES module within the auxiliary set. An example of possible interconnections between the basic types of modules of this set is provided in order to offer a small scale image of the envisioned validation framework.