Towards Formal Verification of Orchestration Computations Using the 핂 Framework
Towards Formal Verification of Orchestration Computations Using the 핂 Framework
复制标题
DOI：
10.1007/978-3-319-19249-9_4
复制
发表时间：
2015-06
期刊：
影响因子：
--
通讯作者：
Musab A. Alturki;Omar Alzuhaibi
中科院分区：
文献类型：
--
作者：
Musab A. Alturki;Omar Alzuhaibi
编排提供了并发计算的通用模型。 Orc 提供了一种最小但富有表现力的编排理论，其中计算是通过站点调用及其通过一些组合器的编排来建模的。使用 Orc，对编排正确性的形式验证相当于设计 Orc 的可执行形式语义并利用现有工具支持。尽管它简单而优雅，但为 Orc 提供正式的语义来精确捕获其预期行为绝非易事，这主要是由于并发性、时序以及内部和外部操作之间的区别带来的挑战。本文提出了一种基于语义的方法，用于使用该框架正式验证 Orc 编排。与 Orc 之前开发的操作语义不同，语义并不直接基于 Orc 的 SOS 规范给出的交错语义。相反，它基于启用的并发重写。它还利用各种设施来达到干净、最小和优雅的语义规范。为了证明所提出方法的有用性，我们描述了一个简单机器人案例研究的规范，并提供了初步的形式验证结果。
Orchestration provides a general model of concurrent computations. A minimal yet expressive theory of orchestration is provided by Orc, in which computations are modeled by site calls and their orchestrations through a few combinators. Using Orc, formal verification of correctness of orchestrations amounts to devising an executable formal semantics of Orc and leveraging existing tool support. Despite its simplicity and elegance, giving formal semantics to Orc capturing precisely its intended behaviors is far from trivial primarily due to the challenges posed by concurrency, timing and the distinction between internal and external actions. This paper presents a semantics-based approach for formally verifying Orc orchestrations using theframework. Unlike previously developed operational semantics of Orc, thesemantics is not directly based on the interleaving semantics given by Orc’s SOS specification. Instead, it is based on concurrent rewriting enabled by. It also utilizes variousfacilities to arrive at a clean, minimal and elegant semantic specification. To demonstrate the usefulness of the proposed approach, we describe a specification for a simple robotics case study and provide initial formal verification results.