Soundness Verification of Business Processes Specified in the Pi-Calculus
Recent research in the area of business process management (BPM) introduced the application of a process algebra—the π-calculus—for the formal description of business processes and interactions among them. Especially in the area of service-oriented archit
- PDF / 519,933 Bytes
- 18 Pages / 430 x 660 pts Page_size
- 96 Downloads / 159 Views
stract. Recent research in the area of business process management (BPM) introduced the application of a process algebra—the π-calculus— for the formal description of business processes and interactions among them. Especially in the area of service-oriented architectures, the key architecture for today’s BPM systems, the π-calculus—as well as other process algebras—have shown their benefits in representing dynamic topologies. What is missing, however, are investigations regarding the correctness, i.e. soundness, of process algebraic formalizations of business processes. Due to the fact that most existing soundness properties are given for Petri nets, these cannot be applied. This paper closes the gap by giving characterizations of invariants on the behavior of business processes in terms of bisimulation equivalence. Since bisimulation equivalence is a well known concept in the world of process algebras, the characterizations can directly be applied to π-calculus formalizations of business processes. In particular, we investigate the characterization of five major soundness properties, i.e. easy, lazy, weak, relaxed, and classical soundness.
1
Introduction
Process algebras, which are algebraic frameworks for the study of concurrent processes, recently gained extended attention in the area of business process management (BPM), e.g. [1,2,3,4,5,6,7]. This is especially true within the area of service-oriented architecture (SOA) [8], which is today’s standard architectural style for realizing BPM solutions [9,10]. What the existing approaches lack, however, is a distinguished investigation on correctness properties for the business processes they describe. By correctness properties, we refer to the different kinds of soundness that have been introduced in the workflow management domain and later on refined. In particular, these are the original soundness definition by van der Aalst [11], nowadays denoted as classical soundness, relaxed soundness by Dehnert [12], and weak soundness by Martens [13]. Noteworthy, all these properties cannot directly be applied to process algebraic formalizations of business processes, since they are characterized using Petri nets. Furthermore, liveness and boundedness are used to prove business processes formalized with Petri nets to be sound; both techniques which are not available for process algebraic verification. R. Meersman and Z. Tari et al. (Eds.): OTM 2007, Part I, LNCS 4803, pp. 6–23, 2007. c Springer-Verlag Berlin Heidelberg 2007
Soundness Verification of Business Processes Specified in the Pi-Calculus
7
Table 1. Comparison of the different kinds of soundness
Possibility of termination Support for lazy activities Deadlock freedom Participation of all activities
Easy Lazy Weak Relaxed Classical + + + + + + + + + + + + +
The focus of our research is on the application of a special kind of process algebra—the π-calculus—to the domain of business process management [14,15]. This calculus is of special interest, since it supports a direct representation of dynamic binding as found in
Data Loading...
