Service-Oriented Computing (SOC) is a promising paradigm for developing enterprise software systems. The initial concepts of service-orientation have been described in the research and industry literature and software tools for assisting in the development of Service-Oriented (SO) applications are becoming more widely used. Nonetheless, a precise description of what constitutes a SO system is yet to be formally defined, and the design principles of SOC are not well understood. Therefore, this paper proposes a formal mathematical model covering design artefacts in service-oriented systems and their structural and behavioural properties. This model promotes a better understanding of SO concepts, and in particular, enables the definition of structural software metrics in an unambiguous, formal manner. Finally, although the proposed model is generic, it can be customised to support particular technologies as shown in this paper where the model was tailored for BPEL4WS implementation.