Soundness verification of business processes specified in the Pi-calculus

摘要: Recent research in the area of business process management (BPM) introduced application a algebra--the π-calculus-- for formal description processes and interactions among them. Especially service-oriented architectures, key architecture today's BPM systems, π-calculus--as well as other algebras--have shown their benefits representing dynamic topologies. What is missing, however, are investigations regarding correctness, i.e. soundness, algebraic formalizations processes. Due to fact that most existing soundness properties given Petri nets, these cannot be applied. This paper closes gap by giving characterizations invariants on behavior terms bisimulation equivalence. Since equivalence known concept world algebras, can directly applied π-calculus In particular, we investigate characterization five major properties, easy, lazy, weak, relaxed, classical soundness.