Article

Real-time rewriting semantics of orc

Authors:

José MeseguerAuthors Info & Claims

PPDP '07: Proceedings of the 9th ACM SIGPLAN international conference on Principles and practice of declarative programming

Pages 131 - 142

https://doi.org/10.1145/1273920.1273938

Published: 14 July 2007 Publication History

Abstract

Orc is a language proposed by Jayadev Misra [19] for orchestration of distributed services. Orc is very simple and elegant, based on a few basic constructs, and allows succinct and understandable programming of sophisticated applications. However, because of its real-time nature and the different priorities given to internal and external events in an Orc program, giving a formal operational semantics that captures the real-time behavior of Orc programs is nontrivial and poses some interesting challenges. In this paper we propose such a real-time operational Orc semantics, that captures the informal operational semantics given in [19]. This operational semantics is given as a rewrite theory in which the elapse of time is explicitly modeled. The priorities between internal and external events are also modeled in two alternative ways: (i) by a rewrite strategy; and (ii) by adding extra conditions to the semantic rules. Since rewriting logic has efficient implementations such as Maude, we also get, directly out of the semantic definitions, both an Orc interpreter and an LTL model checker for Orc programs.

References

[1]

M. AlTurki. A rewriting logic approach to the semantics of Orc. Master's thesis, University of Illinois at Urbana-Champaign, USA, December 2005.

[2]

M. AlTurki and J. Meseguer. Rewriting logic semantics of Orc. Technical report, Department of Computer Science, UIUC, Urbana-Champaign, USA, 2007.

[3]

J. Baeten and C. Middelburg. Process algebra with timing: Real time and discrete time, 2000.

Digital Library

[4]

J. C. M. Baeten and J. A. Bergstra. Real time process algebra. Formal Asp. Comput., 3(2):142--188, 1991.

[5]

R. Bruni and J. Meseguer. Semantic foundations for generalized rewrite theories. Theor. Comput. Sci., 360(1-3):386--414, 2006.

Digital Library

[6]

L. Chen. An interleaving model for real-time systems. In TVER '92: Proceedings of the Second International Symposium on Logical Foundations of Computer Science, pages 81--92, London, UK, 1992. Springer-Verlag.

Digital Library

[7]

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. Talcott. All About Maude: A High-Performance Logical Framework. To be published by Springer, 2007.

Digital Library

[8]

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. Talcott. Maude manual (version 2.3). January 2007. http://maude.cs.uiuc.edu/maude2-manual/maude-manual.pdf.

[9]

W. R. Cook and J. Misra. A structured orchestration language. July 2005. http://www.cs.utexas.edu/users/wcook/Drafts/OrcCookMisra05.pdf.

[10]

S. Eker, N. Martí-Oliet, J. Meseguer, and A. Verdejo. Deduction, strategies, and rewriting. In Proceedings of STRATEGIES '06, August 2006.

[11]

M. Hennessy and T. Regan. A process algebra for timed systems. Inf. Comput., 117(2):221--239, 1995.

Digital Library

[12]

T. Hoare, G. Menzel, and J. Misra. A tree semantics of an orchestration language. August 2004. Also available at http://www.cs.utexas.edu/users/psp/Semantics.Orc.pdf.

[13]

D. Kitchin, W. R. Cook, and J. Misra. A language for task orchestration and its semantic properties. In CONCUR, pages 477--491, 2006.

Digital Library

[14]

J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci., 96(1):73--155, 1992.

Digital Library

[15]

J. Meseguer. Membership algebra as a logical framework for equational specification. In F. Parisi-Presicce, editor, Proc. WADT '97, pages 18--61. Springer LNCS 1376, 1998.

Digital Library

[16]

J. Meseguer and C. Braga. Modular rewriting semantics of programming languages. In AMAST, pages 364--378, 2004.

[17]

J. Meseguer and G. Rosu. Rewriting logic semantics: From language specifications to formal analysis tools. In Proc. Intl. Joint Conf. on Automated Reasoning IJCAR'04, Cork, Ireland, July 2004, pages 1--44. Springer LNAI 3097, 2004.

[18]

J. Meseguer and G. Rosu. The rewriting logic semantics project. Theoretical Computer Science, 2007. To appear (preliminary version in Proc. SOS'05), http://fsl.cs.uiuc.edu/pubs/meseguer-rosu-2006-tcs.pdf.

Digital Library

[19]

J. Misra. Computation orchestration: A basis for wide-area computing. In M. Broy, editor, Proc. of the NATO Advanced Study Institute, Engineering Theories of Software Intensive Systems, NATO ASI Series, Marktoberdorf, Germany, 2004.

[20]

J. Misra and W. R. Cook. Computation orchestration: A basis for wide-area computing. Journal of Software and Systems Modeling, May 2006.

[21]

P. D. Mosses. Modular structural operational semantics. J. Log. Algebr. Program., 60-61:195--228, 2004.

[22]

X. Nicollin and J. Sifakis. The algebra of timed processes ATP: Theory and application. Information and Computation, 114(1):131--178, 1994.

Digital Library

[23]

P. C. Ölveczky and J. Meseguer. Specification of real-time and hybrid systems in rewriting logic. Theoretical Computer Science, 285:359--405, 2002.

Digital Library

[24]

P. C. Ölveczky and J. Meseguer. Real-Time Maude 2.1. Electr. Notes Theor. Comput. Sci., 117:285--314, 2005.

Digital Library

[25]

S. Schneider, J. Davies, D. M. Jackson, G. M. Reed, J. N. Reed, and A. W. Roscoe. Timed CSP: Theory and practice. In Proceedings of the Real-Time: Theory in Practice, REX Workshop, pages 640--675, London, UK, 1992. Springer-Verlag.

Digital Library

[26]

M.-O. Stehr. CINNI - A generic calculus of explicit substitutions and its application. Proceedings Third International Workshop on Rewriting Logic and its Applications, WRLA 2000, Kanazawa, Japan, September 18--20, 2000, volume 36 of Electronic Notes in Theoretical Computer Science, pages 71--92. Elsevier, 2000. http://www.elsevier.nl/locate/entcs/volume36.html.

Cited By

Li QZhao YZhu HHe J(2014)A UTP semantic model for Orc language with execution status and fault handlingFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-014-3385-28:5(709-725)Online publication date: 1-Oct-2014
https://dl.acm.org/doi/10.1007/s11704-014-3385-2
Dong JLiu YSun JZhang X(2014)Towards verification of computation orchestrationFormal Aspects of Computing10.1007/s00165-013-0280-926:4(729-759)Online publication date: 1-Jul-2014
https://dl.acm.org/doi/10.1007/s00165-013-0280-9
Lepri DÁbrahám EÖlveczky P(2012)Timed CTL model checking in real-time maudeProceedings of the 9th international conference on Rewriting Logic and Its Applications10.1007/978-3-642-34005-5_10(182-200)Online publication date: 24-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-34005-5_10
Show More Cited By

Index Terms

Real-time rewriting semantics of orc
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
    2. Program semantics
      1. Operational semantics

Recommendations

Reduction Semantics and Formal Analysis of Orc Programs

Orc is a language for orchestration of web services developed by J. Misra that offers simple, yet powerful and elegant, constructs to program sophisticated web orchestration applications. The formal semantics of Orc poses interesting challenges, because ...
Two case studies of semantics execution in Maude: CCS and LOTOS

We explore the features of rewriting logic and, in particular, of the rewriting logic language Maude as a logical and semantic framework for representing and executing inference systems. In order to illustrate the general ideas we consider two ...
Maude MSOS Tool

Modular structural operational semantics (MSOS) is a new framework that allows structural operational semantics (SOS) specifications to be made modular in the sense of not imposing the redefinition of transition rules, which is the case in SOS ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PPDP '07: Proceedings of the 9th ACM SIGPLAN international conference on Principles and practice of declarative programming

July 2007

240 pages

ISBN:9781595937698

DOI:10.1145/1273920

General Chair:
Michael Leuschel
University of Düsseldorf, Germany
,
Program Chair:
Andreas Podelski
University of Freiburg, Germany

Copyright © 2007 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 July 2007

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

PPDP07

Sponsor:

PPDP07: Principles and Practice of Declarative Programming

July 14 - 16, 2007

Wroclaw, Poland

Acceptance Rates

Overall Acceptance Rate 230 of 486 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
234
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 29 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Li QZhao YZhu HHe J(2014)A UTP semantic model for Orc language with execution status and fault handlingFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-014-3385-28:5(709-725)Online publication date: 1-Oct-2014
https://dl.acm.org/doi/10.1007/s11704-014-3385-2
Dong JLiu YSun JZhang X(2014)Towards verification of computation orchestrationFormal Aspects of Computing10.1007/s00165-013-0280-926:4(729-759)Online publication date: 1-Jul-2014
https://dl.acm.org/doi/10.1007/s00165-013-0280-9
Lepri DÁbrahám EÖlveczky P(2012)Timed CTL model checking in real-time maudeProceedings of the 9th international conference on Rewriting Logic and Its Applications10.1007/978-3-642-34005-5_10(182-200)Online publication date: 24-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-34005-5_10
Tan TLiu YSun JDong J(2011)Verification of orchestration systems using compositional partial order reductionProceedings of the 13th international conference on Formal methods and software engineering10.5555/2075089.2075101(98-114)Online publication date: 26-Oct-2011
https://dl.acm.org/doi/10.5555/2075089.2075101
Ölveczky P(2011)Semantics, simulation, and formal analysis of modeling languages for embedded systems in real-time MaudeFormal modeling10.5555/2074591.2074615(368-402)Online publication date: 1-Jan-2011
https://dl.acm.org/doi/10.5555/2074591.2074615
Meseguer JRoşu G(2011)The rewriting logic semantics projectProceedings of the 18th international conference on Fundamentals of computation theory10.5555/2034214.2034215(1-37)Online publication date: 22-Aug-2011
https://dl.acm.org/doi/10.5555/2034214.2034215
Tan TLiu YSun JDong J(2011)Verification of Orchestration Systems Using Compositional Partial Order ReductionFormal Methods and Software Engineering10.1007/978-3-642-24559-6_9(98-114)Online publication date: 2011
https://doi.org/10.1007/978-3-642-24559-6_9
Meseguer JRoşu G(2011)The Rewriting Logic Semantics Project: A Progress ReportFundamentals of Computation Theory10.1007/978-3-642-22953-4_1(1-37)Online publication date: 2011
https://doi.org/10.1007/978-3-642-22953-4_1
Li QZhu HHe J(2010)A denotational semantical model for Orc languageProceedings of the 7th International colloquium conference on Theoretical aspects of computing10.5555/1881833.1881844(106-120)Online publication date: 1-Sep-2010
https://dl.acm.org/doi/10.5555/1881833.1881844
Bae KÖlveczky P(2010)Extending the Real-Time Maude Semantics of Ptolemy to Hierarchical DE ModelsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.36.336(46-66)Online publication date: 21-Sep-2010
https://doi.org/10.4204/EPTCS.36.3
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents