Rewriting logic semantics of Orc

Orc is a language for 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 RsosOrc in which the elapse of time is explicitly modeled. This is followed by presenting a much more efficient 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 time