Extending and Formalizing UML 2.0 Activity Diagrams for the specification of time-constrained business processes

In real world, most business processes are subject to time constraints. Equally important as the execution of a process is the time in which it is to be performed. A time constrained business process can be defined as a process whose correct behavior depends not only on the results obtained, but also on the time it is carried out. UML has become an important tool for model-driven software development, perhaps partly thanks to its visually oriented modeling concepts, and it is increasingly being used in business process modeling too. In this paper, we extend UML 2.0 Activity Diagrams with time annotations and new modelling constructs inspired of the Timed CSP language. Furthermore, in order to overcome the lack of formal semantics that these diagrams suffer from, we introduce a set of mapping rules to derive formal specifications in terms of Timed CSP processes from models in the extended Activity Diagrams being proposed. Timed CSP has several features that make it well suited to give a formal semantics for extended Activity Diagrams (e.g., compositionality, well defined denotational and operational semantics, etc.). The proposed mapping rules enable checking whether the model described in an Activity Diagram satisfies such properties as timeliness, deadlock freeness, liveness, etc. In order to show the applicability of our approach, we present a case study from a manufacturing domain.