Using π-calculus to formalize UML activity diagram for business process modeling

UML has become the de facto standard for object-oriented software development. It provides rich notations for representing and analyzing architecture and behaviors of systems. Among these notations, the UML activity diagram is well-known for describing a system´s dynamic behaviors. One of its main purposes is to model software processes and business processes, and represent control flows among activities. As a semi-formal notation, the UML activity diagram has no publicly agreed formal semantics. In this paper, the alternative approach of using π-calculus to formalize UML activity diagrams is presented. Therefore, activity models can have rich process semantics. Its main advantages are: (1) according to weak bisimulation in π-calculus two process models can be checked for equivalence, thus facilitating the optimization of business processes or software processes. (2) The process model can be verified as to whether it satisfies certain properties, such as safety and liveness, by means of π-calculus analytical tools. (3) Correct criteria for the process model are expressed with modal Mμ-calculus, such as the correct termination of processes. Therefore, the process model can be automatically verified with the help of π-calculus analytical tools.