IDEALS Home University of Illinois at Urbana-Champaign logo The Alma Mater The Main Quad

Rewriting Logic Semantics of Orc

Show full item record

Bookmark or cite this item: http://hdl.handle.net/2142/11410

Files in this item

File Description Format
PDF Rewriting Logic Semantics of Orc.pdf (757KB) (no description provided) PDF
Title: Rewriting Logic Semantics of Orc
Author(s): AlTurki, Musab; Meseguer, Jose
Subject(s): programming languages computer science
Abstract: Orc is a language for \emph{orchestration} of web services developed by J. Misra that offers simple, yet powerful and elegant, constructs to succinctly program sophisticated web orchestration 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 report, we first propose a real-time operational Orc semantics, that captures the informal operational semantics given in [26]. This operational semantics is given as a rewrite theory $\mathcal{R}^{sos}_{Orc}$ in which the elapse of time is explicitly modeled. This is followed by presenting a much more efficient \emph{reduction semantics} of Orc, which is provably equivalent to the SOS semantics. A detailed proof of strong bisimilarity of the two semantic specifications is then given. In both theories, the priorities between internal and external events and the \emph{time-synchronous} execution strategy used are modeled in two alternative ways: (i) by a rewrite strategy; and (ii) by adding extra equational conditions to the semantic rules. We show experiments demonstrating the much better performance of the reduction semantics when compared to the SOS semantics. We view this reduction semantics as a key intermediate stage towards a future, provably correct distributed implementation of Orc. We describe a distributed, object-based view of the Orc model and its specification. Using the Maude rewriting logic language, we also illustrate how the distributed semantics can be used to endow Orc with useful formal analysis capabilities, including an LTL model checker and search for violations of invariants. We illustrate these formal analysis features by means of two applications: an online auction system and a meeting scheduler, both of which are modeled as distributed systems of actors that perform Orc computations.
Issue Date: 2007-11
Genre: Technical Report
Type: Text
URI: http://hdl.handle.net/2142/11410
Other Identifier(s): UIUCDCS-R-2007-2918
Rights Information: You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).
Date Available in IDEALS: 2009-04-22
 

This item appears in the following Collection(s)

Show full item record

Item Statistics

  • Total Downloads: 120
  • Downloads this Month: 3
  • Downloads Today: 0

Browse

My Account

Information

Access Key