|
 ABSTRACT
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.
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
| |
1
|
Active-Endpoints. Activebpel engine, 2005. Available at: http://www.activebpel.org.
|
| |
2
|
Tony Andrews, Francisco Curbera, Hitesh Dholakia, Yaron Goland, Johannes Klein, Frank Leymann, Kevin Liu, Dieter Roller, Doug Smith, Satish Thatte, Ivana Trickovic, and Sanjiva Weerawarana. Business process execution language for web services version 1.1, 2004.
|
| |
3
|
David Booth, Hugo Haas, Francis McCabe, Eric Newcomer, Michael Champion, Chris Ferris, and David Orchard. Web services architecture, w3c working group note 11 february 2004, 2004. Available at: http://www.w3.org/TR/ws-arch/.
|
| |
4
|
T. Bultan and A. Betin-Can. Scalable Software Model Checking Using Design for Verification. In Proceedings of the IFIP Working Conference on Verified Software: Theories, Tools, Experiments, volume 989, Zurich, Switzerland, 2005.
|
| |
5
|
Chakrabarti, A., Alfaro, L.D., Henzinger, T.A., and Stoelinga, M. Resource interfaces. In Third International Conference on Embedded Software (EMSOFT 2003). ACM Press, 2003.
|
| |
6
|
Eric M. Dashofy, Andre Van der Hoek, and Richard N. Taylor. A highly-extensible, xml-based architecture description language. wicsa, 00:103, 2001.
|
| |
7
|
W. Emmerich, B. Butchart, L. Chen, B. Wassermann, and S. L. Price. Grid Service Orchestration using the Business Process Execution Language (BPEL). Journal of Grid Computing, 3(3-4):283--304, 2005.
|
| |
8
|
H. Foster, S. Uchitel, J. Magee, and J. Kramer. Model-based Verification of Web Service Compositions. In Proc. of the 18th IEEE Int. Conference on Automated Software Engineering, pages 152--161. IEEE CS Press, 2003.
|
| |
9
|
|
| |
10
|
Xiang Fu, Tevfik Bultan, and Jianswen Su. Wsat: A tool for formal analysis of web services. In 16th International Conference on Computer Aided Verification (CAV), Boston, MA, 2004.
|
| |
11
|
C. Goyette. Xml applied to product line software development, 2005. Available from: Figure 11: The WS-Engineer Tool Environment http://www.mcc.com/projects/ssepp/papers.
|
| |
12
|
Rachid Hamadi and Boualem Benatallah. A petri net-based model for web services composition. In 3rd IEEE International Conference On Web Services (ICWS), San Diego, CA, 2004.
|
| |
13
|
Jonathan Haymann. The application of a resource logic to the non-temporal analysis of processes acting on resources (hpl-2003-194). 2003. Available at: http://www.hpl.hp.com/techreports/2003.
|
| |
14
|
W. S. Lee, A. S. McGough, S. Newhouse, and J. Darlington. A Standard Based Approach to Job Submission through Web Services. In S. Cox, editor, Proc. of the UK e-Science All Hands Meeting, Nottingham, UK, pages 901--905. UK EPSRC, 2004.
|
| |
15
|
|
| |
16
|
|
| |
17
|
|
| |
18
|
OMG. Unified modelling language (uml) 2.1.1 specification, 2007. Available from: www.uml.org.
|
| |
19
|
Chun Ouyang , Eric Verbeek , Wil M. P. van der Aalst , Stephan Breutel , Marlon Dumas , Arthur H. M. ter Hofstede, Formal semantics and analysis of control flow in WS-BPEL, Science of Computer Programming, v.67 n.2-3, p.162-198, July, 2007
[doi> 10.1016/j.scico.2007.03.002]
|
 |
20
|
Irfan Pyarali , Marina Spivak , Ron Cytron , Douglas C. Schmidt, Evaluating and Optimizing Thread Pool Strategies for Real-Time CORBA, Proceedings of the ACM SIGPLAN workshop on Languages, compilers and tools for embedded systems, p.214-222, August 2001, Snow Bird, Utah, United States
|
| |
21
|
F. Raimondi, J. Skene, L. Chen, and W. Emmerich. Efficient monitoring of web service slas (research note rn/07/01). 2007. Available at: http://www.hpl.hp.com/techreports/2003.
|
| |
22
|
|
| |
23
|
The-Apache-Software-Foundation. Apache-tomcat 5.5, 2005. Available at: http://tomcat.apache.org/.
|
| |
24
|
Chris Tofts. Efficiently modelling resource in a process algebra (hpl-2003-181). 2003. Available at: http://www.hpl.hp.com/techreports/2003.
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
D.2