Towards Verification of a Service Orchestration Language

Recently, Orc is proposed as a powerful yet elegant language for distributed and concurrent programming which provides computational services such as distributed communication and data manipulation via sites. With a few concurrency primitives, programmers are able to orchestrate the invocation of sites to achieve a goal, and meanwhile, manage timeouts, priorities, and failures. To guarantee the correctness of Orc models, effective verification support is desirable. In this work, we present an automatic approach to verify different properties against Orc models using model checking techniques. To further improve the performance, advanced reduction techniques, like partial order reduction, are proposed.