Rewriting Logic
Semantics of Orc
Musab AlTurki and José Meseguer
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.