Verification of Orchestration Systems Using Compositional Partial Order Reduction
Orc is a computation orchestration language which is designed to specify computational services, such as distributed communication and data manipulation, in a concise and elegant way. Four concurrency primitives allow programmers to orchestrate site calls to achieve a goal, while managing timeouts, priorities, and failures. To guarantee the correctness of Orc model, effective verification support is desirable. Orc has a highly concurrent semantics which introduces the problem of state-explosion to search-based verification methods like model checking. In this paper, the authors present a new method, called Compositional Partial Order Reduction (CPOR), which aims to provide greater state-space reduction than classic partial order reduction methods in the context of hierarchical concurrent processes.