|
|
A UTP semantic model for Orc language with execution status and fault handling |
Qin LI, Yongxin ZHAO( ), Huibiao ZHU, Jifeng HE |
Software Engineering Institute, East China Normal University, Shanghai 200062, China |
|
|
Abstract The Orc language is a concurrency calculus proposed to study the orchestration patterns in service oriented computing. Its special features, such as high concurrency and asynchronism make it a brilliant subject for studying web applications that rely on web services. The conventional semantics for Orc does not contain the execution status of services so that a program cannot determine whether a service has terminated normally or halted with a failure after it published some results. It means that this kind of failure cannot be captured by the fault handler. Furthermore, such a semantic model cannot establish an order saying that a program is better if it fails less often. This paper employs UTP methods to propose a denotational semantic model for Orc that contains execution status information. A failure handling semantics is defined to recover a failure execution back to normal. A refinement order is defined to compare two systems based on their execution failures. Based on this order, a system that introduces a failure recovery mechanism is considered better than one without. An extended operational semantics is also proposed and proven to be equivalent to the denotational semantics.
|
Keywords
Orc language
service oriented computing
unifying theories of programming
denotational semantics
operational semantics
|
Corresponding Author(s):
Yongxin ZHAO
|
Issue Date: 11 October 2014
|
|
1 |
G Alonso, H Kuno, F Casati, V Machiraju. Web Services: Concepts, Architectures and Applications. Springer, 2003
|
2 |
G Andrews. Foundations of Multithreaded, Parallel, and Dis-tributed Programming. Addison-Wesley, 2000
|
3 |
V S Sunderam. Pvm: A framework for parallel distributed computing. Concurrency: practice and experience, 1990, 2(4): 315−339
https://doi.org/10.1002/cpe.4330020404
|
4 |
W Emmerich, B Butchart, L Chen, B Wassermann, S L Price. Grid service orchestration using the business process execution language (bpel). Journal of Grid Computing, 2005, 3(3/4): 283−304
https://doi.org/10.1007/s10723-005-9015-3
|
5 |
M Koshkina, F Breugel. Modelling and verifying web service orchestration by means of the concurrency workbench. ACM SIGSOFT Software Engineering Notes, 2004, 29(5): 1−10
https://doi.org/10.1145/1022494.1022526
|
6 |
G Ferrari, R Guanciale, D Strollo. JSCL: A middleware for service coordination. In: Proceedings of Formal Techniques for Networked and Distributed Systems. 2006, 46− 60
|
7 |
M Klusch. Semantic web service coordination. In: Proceedings of CASCOM: Intelligent Service Coordination in the Semantic Web. 2008, 59−104
|
8 |
A Lazovik, F Arbab. Using reo for service coordination. In: Proceedings of International Conference on Service-Oriented Computing, 2007, 398−403
|
9 |
T Erl. Service-Oriented Architecture (SOA): Concepts, Technology, and Design. Prentice Hall PTR, 2005
|
10 |
M Armbrust, A Fox, R Griffith, A D Joseph, R Katz, A Konwinski, G Lee, D Patterson, A Rabkin, I Stoica, M Zaharia. A view of cloud computing. Communications of the ACM, 2010, 53(4): 50−58
https://doi.org/10.1145/1721654.1721672
|
11 |
M Armbrust, A Fox, R Griffith, A D Joseph, R Katz, A Konwinski, G Lee, D Patterson, A Rabkin, I Stoica, M Zaharia. Above The Clouds: A Berkeley View of Cloud Computing. Technical Report, EECS Department, University of California, Berkeley, 2009
|
12 |
J Misra. A programming model for the orchestration of web services. In: Proceedings of 2nd International Conference on Software Engineering and Formal Methods. 2004, 28−30
|
13 |
J Misra, W R Cook. Computation orchestration. Journal of Software and System Modeling, 2007, 6(1): 83−110
https://doi.org/10.1007/s10270-006-0012-1
|
14 |
D Kitchin, W R Cook, J Misra. A language for task orchestration and its semantic properties. Lecture Notes in Computer Science, 2006, 477−491
https://doi.org/10.1007/11817949_32
|
15 |
W R Cook, S Patwardhan, J Misra. Workflow patterns in Orc. Lecture Notes in Computer Science, 2006, 82−96
https://doi.org/10.1007/11767954_6
|
16 |
Orc Language Project. Orc User Guide v2.1.0.
|
17 |
Orc Language Project. Orc Program Language Demo.
|
18 |
D Kitchin, A Quark, W R Cook, J Misra. The orc programming language. Lecture Notes in Computer Science, 2009, 1−25
https://doi.org/10.1007/978-3-642-02138-1_1
|
19 |
C A R Hoare, J F He. Unifying Theories of Programming. Prentice Hall International Series in Computer Science. 1998
|
20 |
Q Li, H B Zhu, J F He. A denotational semantical model for orc language. In: Proceeding of the 7th International Colloquium on Theoretical Aspects of Computing. 2010, 106−120
|
21 |
T Nipkow. Programming and proving in isabelle/hol. Technical report, University of Cambridge, 2013
|
22 |
M Wenzel. The isabelle/isar reference manual. Technical report, University of Cambridge, 2013
|
23 |
S Owre, JM Rushby, N Shankar. Pvs: A prototype verification system. Lecture Notes in Computer Science, 1992, 607: 748−752
https://doi.org/10.1007/3-540-55602-8_217
|
24 |
A Tarski. A lattice-theoretical fix point theorem and its applications. Pacific Journal of Mathematics, 1955, 5(2): 285−309
https://doi.org/10.2140/pjm.1955.5.285
|
25 |
D Fensel, C Bussler. The web service modeling framework {WSMF}. Electronic Commerce Research and Applications, 2002, 1(2): 113−137
https://doi.org/10.1016/S1567-4223(02)00015-7
|
26 |
J F He, H B Zhu, G G Pu. A model for BPEL-like languages. Frontiers of Computer Science in China, 2007, 1(1): 9−19
https://doi.org/10.1007/s11704-007-0002-7
|
27 |
I Wehrman, D Kitchin, WR Cook, J Misra. Properties of the timed operational and denotational semantics of orc. Technical report, Department of Computer Science, The University of Texas at Austin, 2007
|
28 |
A Matsuoka, D Kitchin. A semantics for exception handling in orc. 2009
|
29 |
T Hoare. A tree semantics of an orchestration language. In: Proceedings of NATO Advanced Study Institute, Engineering Theories of Software Intensive Systems. 2004
|
30 |
D Vardoulakis, M Wand. A compositional trace semantics for orc. Coordination Models and Languages, 2008, 5052: 331−346
https://doi.org/10.1007/978-3-540-68265-3_21
|
31 |
I Wehrman, D Kitchin, W R Cook, J Misra. A timed semantics of orc. Theoretical Computer Science, 2008, 402(2/3): 234−248
https://doi.org/10.1016/j.tcs.2008.04.037
|
32 |
J S Dong, Y Liu, J Sun, X Zhang. Verification of computation orchestration via timed automata. Lecture Notes in Computer Science, 2006, 4260: 226−245
https://doi.org/10.1007/11901433_13
|
33 |
M AlTurki, J Meseguer. Real-time rewriting semantics of orc. In: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2007, 131−142
|
34 |
M AlTurki, J Meseguer. Reduction semantics and formal analysis of orc programs. Electronic Notes in Theoretical Computer Science, 2008, 200(3): 25−41
https://doi.org/10.1016/j.entcs.2008.04.091
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
|
Shared |
|
|
|
|
|
Discussed |
|
|
|
|