Rewriting Logic Semantics of Orc

AlTurki, Musab; Meseguer, José

Permalink

https://hdl.handle.net/2142/11410 Copy

Description

Title

Rewriting Logic Semantics of Orc

Author(s)

• AlTurki, Musab
• Meseguer, José

Issue Date

2007-11

Keyword(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.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11410

Copyright and License 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).

Owning Collections