Formal Verification of E-Services and Workflows

Abstract. We study the verification problem for e-service (and workflow) speci-fications, aiming at efficient techniques for guiding the construction of composite e-services to guarantee desired properties (e.g., deadlock avoidance, bounds on resource usage, response times). Based on e-service frameworks such as AZTEC and e-FLow, decision flow language Vortex, we introduce a very simple e-service model for our investigation of verification issues.We first show how three different model checking techniques are applied when the number of processes is limited to a predetermined number.We then introduce pid quantified constraint, a new sym-bolic representation that can encode infinite many system states, to verify systems with unbounded and dynamic process instantiations. We think that it is a versatile technique and more suitable for verification of e-service specifications. If this is combined with other techniques such as abstraction and widening, it is possible to solve a large category of interesting verification problems for e-services.