Imperial College London
Alternate

Professor Jeff Magee

Faculty of Engineering, Department of Computing

Emeritus Professor of Computing
 
 
 
//

Contact

 

+44 (0)20 7594 8601j.magee Website

 
 
//

Assistant

 

Mrs Clare Pearson +44 (0)20 7594 8601

 
//

Location

 

2.06Faculty BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Foster:2007:10.1145/1287624.1287657,
author = {Foster, H and Emmerich, W and Kramer, J and Magee, J and Rosenblum, D and Uchitel, S},
doi = {10.1145/1287624.1287657},
pages = {225--234},
title = {Model checking service compositions under resource constraints},
url = {http://dx.doi.org/10.1145/1287624.1287657},
year = {2007}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - 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 account. We evaluate the approach by applying it to the above application and are able to demonstrate that a change in allocation of services to hosts is indeed safe, a result that we are able to confirm experimentally in the deployed system. The approach is supported by a tool suite, known as WS-Engineer, providing automated process translation, architecture and model-checking views. Copyright 2007 ACM.
AU  - Foster,H
AU  - Emmerich,W
AU  - Kramer,J
AU  - Magee,J
AU  - Rosenblum,D
AU  - Uchitel,S
DO  - 10.1145/1287624.1287657
EP  - 234
PY  - 2007///
SP  - 225
TI  - Model checking service compositions under resource constraints
UR  - http://dx.doi.org/10.1145/1287624.1287657
ER  -
Download