Executable rewriting logic semantics of Orc and formal analysis of Orc programs

This work proposes a formal executable semantics for Orc in rewriting logic, to support formal verification of Orc programs and to make possible semantics-based correct-by-construction Orc implementations. While being a very simple calculus, Orc has a quite subtle semantics, so that fully capturing all its semantic aspects is highly nontrivial. The two main sources of subtlety are: (i) its real-time semantics, and (ii) the priority of internal computations within an Orc expression over external computations that process responses from external sites. In this paper, we show a simple and elegant way of handling these two sources of subtlety in rewriting logic using an order-sorted type system supporting subtypes and subtype polymorphism, and “tick” rewrite rules for capturing time. Moreover, our rewriting semantics incorporates useful semantic equivalences between Orc programs as equations and equational attributes, making the semantics both more abstract and more efficient. The semantics of Orc is given in two different styles: (i) an SOS style, which is directly based on the original SOS of Orc, whose correctness follows immediately by construction, and (ii) a reduction semantics, which is much more efficiently executable and analyzable, as shown through several experiments, and whose correctness is proved using a strong bisimulation theorem. The paper also presents MOrc, a simulator and model checking tool based on the rewriting semantics of Orc and Real-Time Maude. MOrc facilitates formal verification of Orc programs, and allows for user-defined state predicates and LTL formulas, with no need for any prior knowledge of Maude or its rewriting logic foundations.