Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

10-2011

Abstract

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, we 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. Evaluation shows that CPOR is more effective in reducing the state space than classic partial order reduction methods.

Keywords

Model Check, State Object, Operational Semantic, Linear Temporal Logic, Label Transition System

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October 26-28

First Page

98

Last Page

114

ISBN

9783642245589

Identifier

10.1007/978-3-642-24559-6_9

Publisher

Springer Link

City or Country

Durham, UK

Additional URL

https://doi.org/10.1007/978-3-642-24559-6_9

Download

Share

COinS