BPMN中的协作与编排一致性
Collaboration vs. choreography conformance in BPMN
AI总结：
本文提出一种基于形式化操作语义和C4工具的方法论与框架，用于检查BPMN编排图与协作图之间的一致性，以促进形式化方法的实际应用。
摘要：
BPMN 2.0标准是一种广泛使用的半形式化表示法，用于从不同视角对分布式信息系统进行建模。该标准提供了一组图表来表示这些视角。编排图表示系统组件之间交互的全局约束，而不暴露其内部结构。相反，协作图允许描绘组件（也称为流程）在与其它组件集成时的内部行为，从而表示分布式系统的一种可能实现。本文提出了一种设计方法论和形式化框架，用于检查编排与协作之间的一致性。具体而言，本文为BPMN编排图和协作图都提供了直接的形式化操作语义。通过基于所定义语义提出的两个关系来定义一致性方面。该方法得益于我们开发的名为C4的工具的可用性，该工具允许在实际环境中实验该理论框架。这里的目标是使所利用的形式化方法对系统设计者透明，从而促进实践者更广泛地采用。
英文摘要：
The BPMN 2.0 standard is a widely used semi-formal notation to model distributed information systems from different perspectives. The standard makes available a set of diagrams to represent such perspectives. Choreography diagrams represent global constraints concerning the interactions among system components without exposing their internal structure. Collaboration diagrams instead permit to depict the internal behaviour of a component, also referred as process, when integrated with others so to represent a possible implementation of the distributed system. This paper proposes a design methodology and a formal framework for checking conformance of choreographies against collaborations. In particular, the paper presents a direct formal operational semantics for both BPMN choreography and collaboration diagrams. Conformance aspects are proposed through two relations defined on top of the defined semantics. The approach benefits from the availability of a tool we have developed, named C4, that permits to experiment the theoretical framework in practical contexts. The objective here is to make the exploited formal methods transparent to system designers, thus fostering a wider adoption by practitioners.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
