Soundness Verification of Business Processes Specified in the Pi-Calculus
Recent research in the area of Business Process Management (BPM) introduced the application of process algebra - the pi-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 pi-calculus - as well as other process algebras - has 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.