Model checking service compositions under resource constraints

When enacting a web service orchestration defined using the Business Process Execution Language (BPEL) we observed various safety property violations. This surprised us considerably as we had previously established that the orchestration was free of such property violations using existing BPEL model checking techniques. In this paper, we describe the origins of these violations. They result from a combination of design and deployment decisions, which include the distribution of services across hosts, the choice of synchronisation primitives in the process and the threading configuration of the servlet container that hosts the orchestrated web services. This leads us to conclude that model checking approaches that ignore resource constraints of the deployment environment are insufficient to establish safety and liveness properties of service orchestrations specifically, and distributed systems more generally. We show how model checking can take execution resource constraints into accou...

• Type: Conference
• Year: 2007
• Where: SIGSOFT
• Authors: David S. Rosenblum, Howard Foster, Jeff Kramer, Jeff Magee, Sebastián Uchitel, Wolfgang Emmerich
• Keywords: Model Checking, Model Checking Approaches, Safety Property Violations, SIGSOFT 2007, Software Engineering