Please wait a minute...
Frontiers of Computer Science

ISSN 2095-2228

ISSN 2095-2236(Online)

CN 10-1014/TP

Postal Subscription Code 80-970

2018 Impact Factor: 1.129

Front. Comput. Sci.    2014, Vol. 8 Issue (5) : 709-725    https://doi.org/10.1007/s11704-014-3385-2
RESEARCH ARTICLE
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
 Download: PDF(457 KB)  
 Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks
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
 Cite this article:   
Qin LI,Yongxin ZHAO,Huibiao ZHU, et al. A UTP semantic model for Orc language with execution status and fault handling[J]. Front. Comput. Sci., 2014, 8(5): 709-725.
 URL:  
https://academic.hep.com.cn/fcs/EN/10.1007/s11704-014-3385-2
https://academic.hep.com.cn/fcs/EN/Y2014/V8/I5/709
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
[1] Yanhong HUANG,Jifeng HE,Huibiao ZHU,Yongxin ZHAO,Jianqi SHI,Shengchao QIN. Semantic theories of programs with nested interrupts[J]. Front. Comput. Sci., 2015, 9(3): 331-345.
[2] Shuling WANG, Qin SHU, Yijing LIU, Zongyan QIU, . A semantic model of confinement and Locality Theorem[J]. Front. Comput. Sci., 2010, 4(1): 28-46.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed