相对定时的业务流程建模符号的语义模型及应用

理论计算机科学电子笔记229（2009）59-75www.elsevier.com/locate/entcs一种BPMN彼得·Y H.黄1和杰里米·吉本斯2联合王国牛津大学计算实验室摘要我们描述了一个相对定时的业务流程建模符号（BPMN）的语义模型。我们在通信顺序进程（CSP）语言中定义了语义该模型增强了我们的通过引入相对时间的概念，以从一个范围内非确定性地选择的延迟的形式，建立了非定时模型我们通过一个例子来说明应用我们还展示了一些属性有关的时间语义和BPMN我们的时间语义允许BPMN图的行为属性通过FDR工具提供的自动模型检查进行机械验证关键词：业务流程，CSP，细化，时间语义，验证，工作流1介绍业务流程和工作流程的建模是软件工程中的一个重要领域。业务流程建模符号（BPMN）允许开发人员采用面向流程的方法来建模系统。在我们以前的工作[16]中，我们已经给出了一个使用Z [20]的抽象语法和一个不定时的进程语义[ 14 ]在CSP的语言[14]到BPMN的子集[12]。 但由于缺乏当时间性成为一个因素时，这种语义不能精确地对并发运行的活动建模例如，图1显示了一个简化的乳腺癌临床试验，改编自Neo-tango试验方案[4]。临床试验的BPMN表示基于新的观察工作流模型及其相应的BPMN转换[18]。请注意，本文中使用的临床试验规范绝不是真实试验的准确代表。在临床研究中，安全有效地进行干预非常重要，通常干预必须满足一系列肿瘤安全性原则[7]。在本例中，我们将重点关注1电子邮件：peter. comlab.ox.ac.uk2电子邮件：jeremy. comlab.ox.ac.uk1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.06.02960P.Y.H. Wong，J.Gibbons/Electronic Notes in Theoretical Computer Science 229（2009）59Fig. 1. 简化的临床试验图1中表示为BPMN子流程状态的干预集合A2。A2的扩展版本如图2所示，下面我们展示了图二.一系列临床干预措施对于每种药物的给药，为了简单起见，我们省略了剂量• EC C -环磷酰胺，每14天至20天一次• EC E-肾上腺素，每18天至21天• TG-紫杉醇，每5天至10天一次，随后吉西他滨，最多10天安全原则之一是排序，它确保每次干预“为了良好的效果和最小的伤害，暂时采取（必要的）行动”。在这里，我们感兴趣的是下面这个原则在干预A2中的具体例子吉西他滨（TG G）在环磷酰胺（EC C）给药后、表阿霉素（EC E）给药前最多只能给1次。正是这些类型的属性，我们希望验证BPMN表示，而仔细的计算可以揭示这个试验规范是否确实满足该属性，因此是本文其余部分的结构如下。 第二部分是引言到BPMN; CSP [14]和Z [20]的介绍，这是本文中使用的，在附录中给出。在第3节中给出了我们对BPMN的语法描述的概述。第4节简要描述了我们的相对时间语义。在第5节中，我们展示了一些与定时和非定时模型相关的属性，在CSP改进，并重新访问的例子，以显示如何相对定时模型P.Y.H. Wong，J.Gibbons/Electronic Notes in Theoretical Computer Science 229（2009）5961可用于对照排序规则进行验证。最后，我们与相关工作的比较，本文。时间模型的完整形式定义可以在我们的长篇论文[17]中找到2BPMN如图3所示，我们的BPMN子集中的状态可以是池、任务、子流程、多个实例或控制网关，每个都通过正常序列、异常序列流或消息流链接。一个正常的序列队列流可以是进入一个状态或从一个状态输出，并且具有相关的保护;一个异常序列队列流，由标记为task*、bpmn*、task**和bpmn** 的状态描述，表示在该状态内发生错误。虽然序列流表示单个局部图中的控制流，但消息流表示不同局部图中状态之间的单向通信。因此，全局图是通过消息流连接的局部图的集合图三. BPMN图在图3中，有两种类型的启动状态：start和stime。 开始状态通过启动其传出转换来模拟当前范围内业务流程的开始;它没有传入转换，只有一个传出转换。stime状态是一个可变的开始状态;当指定的持续时间过去时，它启动其传出转换。还有两种类型的中间状态，itime和imessage。itime状态是延迟事件;在它的输入转换被触发之后，延迟事件在启动它的输出转换之前等待指定的持续时间。imessage状态是一个消息事件;在其传入转换被触发之后，消息事件等待直到指定消息到达，然后才开始其传出转换。两种类型的状态最多都有一个传入转换和一个传出转换。有两种类型的结束状态，结束和中止。结束状态通过初始化传入转换来模拟当前范围内业务流程实例的成功终止;它只有一个传入转换，62P.Y.H. Wong，J.Gibbons/Electronic Notes in Theoretical Computer Science 229（2009）59外向过渡中止状态是一种不同的结束状态;它模拟不成功的终止，通常是当前范围内业务流程实例的错误。我们的BPMN子集包含两种类型的决策状态，xgate和agate。 它们中的每一个都有一个或多个传入序列流和一个或多个传出序列流。一个xgate状态是一个独占网关，接受它的一个入站流，并接受它的一个出站流;这种网关类型的语义可以描述为一个独占选择和一个简单的合并。玛瑙状态是一个并行网关，它在初始化所有传出数据流之前等待所有传入数据流。任务状态描述了一个原子活动，并且只有一个传入和一个传出转换。它需要一个唯一的名称来标识活动。在时间语义模型的环境中，每个原子任务必须花费一定的时间才能完成。bpmn状态描述子进程状态。它本身就是一个业务流程，因此它对BPMN状态流进行建模。 本文在分析了现有文献的基础上，我们假设所有的子过程状态都是扩展的[12];这意味着我们对子过程的内部行为进行建模。图3中标记为bpmn的状态描述了一个折叠的子流程状态，其中隐藏了所有内部细节;此状态只有一个传入和一个传出转换。在图3中，还有标记为task*、bpmn*、task**、bpmn**、task*和bpmn* 的图形符号，它们描述了带有异常序列的任务状态和子进程状态。在我们的BPMN状态子集中，有三种类型的异常与任务和子流程状态相关联。状态task* 和bpmn* 都是具有ierror异常流的状态的示例，该异常流对由于任务或子进程状态中的错误而导致的中断进行建模;状态task** 和bpmn** 是具有定时异常流的状态的示例，并且对由于指定持续时间的流逝而导致的中断进行建模;状态task* 和bpmn* 是具有消息异常的状态的示例，并在接收到指定消息时对中断进行建模。每个任务和子流程状态最多可以有一个定时异常流，尽管它可能有多个错误和消息异常流。每个任务和子流程也可以定义为多个实例。BPMN中有两种类型的多实例：miseq状态类型表示串行多实例，其中指定的任务按顺序重复;在mipar状态类型中，指定的任务并行重复。 类型miseqs和mipars是它们的子流程对应物。图3中的图形化符号池形成了每个局部图的最外层容器，表示单个业务流程;只有一个执行实例 在任何时候都是允许的。池中包含的每个本地图也可以是涉及多个业务流程的业务协作（全局图）中的参与者。虽然序列消息流仅限于单个池，但消息消息流表示池之间的通信。P.Y.H. Wong，J.Gibbons/Electronic Notes in Theoretical Computer Science 229（2009）5963^^ ^您的位置^3抽象语法在本节中，我们使用Z符号描述BPMN的抽象语法[20]。 由于篇幅的原因，本节提供了BPMN抽象语法的部分定义我们首先引入一些最大值集来表示构造，例如行，任务和子进程名称，定义为Z基本类型：[PName，Task， Line， Channel， Guard， Msg]其中PName是图的名称集合。在本文中，我们将只考虑描述时间周期（持续时间）的BPMN定时事件的语义，而不是绝对时间戳。我们定义模式类型Time来记录每个持续时间;该模式对XML模式的六维空间的严格正子集进行建模 数据类型持续时间[21，第3.2.6节]。时间=[年、月、日、时、分、秒：N]图3中所示的每种状态类型都是使用自由类型Type定义的，其中每个构造函数都描述了一种特定的状态类型。例如，原子任务状态的类型由任务t定义，其中t是标识该任务状态的唯一名称。下面是部分定义。类型：：= start|stime时间|end N|中止任务|task任务|xgate|bpmnBName|miseq任务任务× N任务根据BPMN规范[12]，每个状态类型都有其他描述其属性的相关属性;我们的语法定义只包括其中一些属性。例如，序列多实例状态类型的循环数由构造函数miseq中的自然数记录。在本文中，我们称之为序列流和异常流的我们通过下面的模式定义给出序列流或异常流以及消息流的类型。Trans=[guard：Guard;line：Line]消息流=[msg：Msg;chn：Channel]每个原子任务状态指定一个延迟范围，min. max，类型为Range，表示在这些范围内选择非确定性延迟。每个任务在执行时在内部范围=[min，max：时间|min≤ Tmax]我们通过模式State记录每个状态的类型、转换和消息流。在这里，我们展示了模式状态的部分定义，省略了64P.Y.H. Wong，J.Gibbons/Electronic Notes in Theoretical Computer Science 229（2009）59^⟨⟩由于空间的原因，用于消息流的架构组件State=[type：Type;in， out， error：PTrans;loop：N;ran：Range]在这里，我们从图2中的示例中提供任务状态EC E的语法定义。⟨|类型~任务EC E，输入~ t 1，输出~ t 2，错误~ t，循环~ 0，跑~跑|min ~ min|年、月、时、分、秒~ 0、天~ 18|你好，最大值|年、月、时、分、秒~ 0、天~ 21 |⟩ |⟩ |⟩池封装的每个BPMN图都是本地图，表示协作中的单个业务参与者，由一组良好构造的状态建立[17]。虽然我们将每个局部图与唯一的名称相关联，但表示业务协作的全局图是由一组有限的名称组成的，每个名称与其局部图相关联;我们还将每个全局图与唯一的名称相关联。4时间语义我们定义了一个时间语义函数，它采用全局图的语法描述，描述协作，并返回CSP过程，该过程对该图的时间行为进行建模。也就是说，该函数采用一个或多个池状态，每个状态封装表示业务协作中的单个参与者的本地图，并返回每个对应于单个参与者之一的定时行为对于每个局部图，相对定时语义是部分交织由制定和协调功能定义的两个过程。en-timed函数返回进程的并行组合，每个进程对应于局部图的状态的非定时方面;这本质上是我们的局部图的非定时语义[16]。coordination函数返回一个用于协调该图的定时行为的进程;它本质上实现了 实时系统和定时协调语言采用的两阶段功能方法的变体[10]。我们的定时模型允许自动翻译，不需要用户交互。现在我们将简要概述协调函数;同样出于篇幅的原因，我们只提供带有非正式描述的函数类型。制定和协调职能的完整正式定义可以在我们的长篇论文中找到[17]。非正式地，协调过程执行以下步骤：分支并制定所有未计时的事件和网关，直到BPMN过程达到时间稳定性，即当所有活动的BPMN状态都被计时时;以某种顺序对所有立即的活动状态进行排序。tn;根据它们的定时信息制定所有时间就绪状态;然后从序列中移除所制定的状态。该过程重复执行这些步骤，直到制定终止。P.Y.H. Wong，J.Gibbons/Electronic Notes in Theoretical Computer Science 229（2009）5965--我们定义了clock函数来实现协调，其中TimeState是一组定时的BPMN状态，函数allstates递归地返回一组包含在局部图中的状态，包括那些包含在图的子流程状态中的状态时钟：PName→ 当地→ 过程这个函数获取PName类型的图的名称及其Local类型的指定环境（图/子进程名称与它们的状态集之间的映射），并返回一个进程，该进程首先触发一个开始状态的传出转换，由制定确定。然后，该过程的行为由函数stable定义。stable：（P状态→›P状态→过程）→P州→›PName流程当地→函数stable是一个高阶函数;它接受某个函数f（例如，从下面的函数timer构造）和一组活动状态，并返回一个过程，该过程递归地制定所有未定时的活动状态，直到局部图是时间稳定的[17]，即当局部图的所有活动状态都被定时时。回到图2中的示例，状态EC C、EC E、TG T和TG G是定时的，并且当函数stable最初应用于图的语法时，它返回的过程将根据序列图来执行所有状态，直到活动状态的集合是EC C、 EC E、 TG T，即图是时间稳定的。 之后，函数的行为由函数f定义;在时钟的定义中，f是应用了前四个参数的函数计时器，其中第三和第四个参数最初为空。计时器：PName→当地→ P状态→P状态→P状态→过程通常，函数timer采用图的名称和指定环境，一组在前一时间稳定性之前活动的定时状态（初始为空），一组非确定性延迟其执行的定时状态（初始为空），以及一组在当前时间稳定性期间活动的定时状态。 它根据其定时信息对当前活动的定时状态的集合进行排序。非正式的订购过程执行以下两个步骤：• 创建具有最短延迟的活动定时状态的子集，我们将这些状态表示为时间就绪[17]，在我们的示例中，在第一次时间稳定之后，唯一的时间就绪状态是状态TG T，其具有5天的最小延迟;• 从所有未时间就绪的定时状态的延迟中减去最短延迟，以表示至少该时间量已经过去。在我们的示例中，由于TG T是时间就绪的，其他活动定时状态EC C和EC E将分别具有9到15天和13到16天的延迟。→66P.Y.H. Wong，J.Gibbons/Electronic Notes in Theoretical Computer Science 229（2009）59→›•→然后，该函数在时间就绪状态集合和活动但时间未就绪状态集合上表现为由函数truntrun ： PName→<$trun J： PName→<$record：PName→Local→›Local→ ›本地→P 态 →›P 态→›P态→P状态进程P状态→过程P状态→过程函数trun返回一个进程，该进程递归地制定给定BPMN进程中时间就绪的当前活动定时状态的子集协调时间就绪状态是通过将函数trunJ返回的执行过程与记录函数record返回的记录过程部分交错来实现的。函数trunJ获取图如果这些进程的相应状态终止、被取消或被延迟，则这些进程终止。对于这些情况中的每一种，进程都将向记录进程传送相应的协调事件。在所有交错进程终止之后，函数trunJ终止，并像进程一样运行run（A）= Qa：A 一运行（A），在同一组协调事件上，以便如果任何后续协调由于循环而包含相同的时间就绪状态，则该过程将不会导致阻塞。下面我们展示了应用于时间就绪状态TG T的trun j，事件在此开始. TG T表示状态TG T（Paclitaxel的管理）的制定，init。TG G表示从状态TG T到TG G的控制流，并且结束。TG T和延迟。TG T是TG T的终止和延迟事件。开始。TG T→初始化。TG G →完成。TG T →跳过H延迟TG T → run（{finish. TG T，延迟。TG T}）函数记录获取图以下规则非正式地描述了函数：(i) 如果所有时间就绪状态都延迟了它们的颁布，并且没有其他当前活动状态，则记录重新计算这些状态，使得延迟范围具有最短上限的状态将被颁布;(ii) 如果所有的时间就绪状态都已经被制定或延迟，那么这就完成了一个定时协调的周期，然后该过程的行为被定义为稳定并继续进行下一个周期;(iii) 如果存在尚未颁布或延迟的时间就绪状态，则记录等待来自执行进程的协调事件在我们的例子中，当时间就绪状态TG T被应用于记录时，它返回的过程要么等待TG T被执行，要么被延迟。如果TG T生效，P.Y.H. Wong，J.Gibbons/Electronic Notes in Theoretical Computer Science 229（2009）5967--N±TF它在一个空的非定时状态集和定时状态集EC上表现为稳定C、欧共体E，TGG，因为TG T的紧接着的状态是TG G，这是定时状态（规则ii）。否则，它也将表现为稳定的，因为当前活动状态的集合不是空的（规则ii）。协调在制定顶层图的结束状态后终止，以完整定义语义功能，可以在我们的较长论文中找到[17]。5分析我们已经实现了本文中描述的语义作为一个原型工具，使用-ING函数式编程语言Haskell。 读者可从我们的网站3找到实施的副本。该工具输入来自JViewsBPMN Modeler [9]的BPMN图的XML序列化表示，并将时序信息作为自定义属性进行了丰富，并将其转换为包含CSP进程的ASCII文件，这些CSP进程表示其以机器可读CSP表示的行为[14]。以下是时间模型的一些结果。 我们说一个图是定时的如果它包含定时信息，否则不定时;每个定时图都是另一个不定时图的定时变体，即用定时信息扩充的不定时图。下面是一个关于时间变化的直观属性命题5.1不定时不变性对于任何非定时局部图，存在一个（无限）定时变体图集合，使得集合中的所有图在非定时语义下都是失败等价的CSP行为模型跟踪（）、稳定故障（）和故障发散（）允许基于反向包容的细化排序[14]。一个行为规范R可以通过构造满足它的“最小”--也就是最不确定的--过程来表达任何满足规范R的过程Q都必须精化PR，记为PRQ。任何进程的一个共同行为属性可能是死锁自由。我们定义进程DF，为事件所在的局部图指定无死锁规范。n和中止。n表示成功执行和中断恢复[17]。DF=（H i：H i）|finn，中止|}·i → DF）H（H n：N·fin. n→跳过）H（H n：N·中止。n→停止）定义5.2局部图是无死锁的，如果对应于该图的行为的进程对定时和非定时模型使用公共语义域的结果之一是，我们可以将某些行为属性从非定时世界转移到定时世界。 我们通过显示任何时间变化来实现这一点在任何本地图中，定时协调过程是对制定过程的响应插件[13]。非正式地说，如果Q是3http://www.comlab.ox.ac.uk/peter.wong/observation/68P.Y.H. Wong，J.Gibbons/Electronic Notes in Theoretical Computer Science 229（2009）59不准备与P为它们的共享接口设定的模式合作。我们现在正式介绍里德等人。使用稳定故障模型定义CSP进程上的二元关系RespondsTo定义5.3对于存在共享事件集合J的任何过程P和Q，Q对所有迹s∈ seq（αP<$αQ）和事件集合X响应于Pi（sTαP，X）∈failures（P）<$（initial（P/ s）<$JJ）\X/=<$<$（sTαQ，（initials（P/s）<$J J）\X）∈/failures（Q）其中，initials（P/ s）是跟踪s之后的P的可能事件的集合，并且AJ是事件A{C}的集合;C表示CSP中的成功终止第5.4章反应对于相对时间模型下的任何局部图p，其中它的制定和协调分别由过程E和T建模，T响应于E。证据（草图。）我们继续考虑定义协调过程的每一个函数，并证明对于任何局部图p，如果存在一组状态，这些状态可以由p我们这样做是为了表明，如果由每个功能定义的过程与pQ命题5.4的一个直接结果是，从非定时到定时设置都保持了死锁自由。5.5Deadlock Freedom的定义对于任何过程P，建模非定时局部图的行为，并且对于任何过程Q，建模该图的定时变体的行为DF±F PDF ±FQ我们说一个行为性质是与时间无关的，如果以下成立。5.6时间独立性一个行为规范过程S相对于某个非定时局部图是时间无关的，该局部图的行为由过程Pi表示，对于任何过程Q，该过程Q对该图的定时变量的行为进行建模，S±F PS ±FQ作为命题5.4和5.5以及以上修正的结果，我们可以通过以下结果来推广与时间无关的规范。命题5.7一个特定过程S相对于某个非定时局部图是时间无关的，该局部图的行为由过程P i i给出S±FP惠迹（S）解迹（P）解死锁（S）解死锁（P）P.Y.H. Wong，J.Gibbons/Electronic Notes in Theoretical Computer Science 229（2009）5969--⟨⟩其中，trace（P）是进程P的可能轨迹的集合，deadlocks（P）是P可以死锁的轨迹的集合。现在我们重新查看图2中给出的示例。由于空间的原因，图中的XML表示及其相应的生成的CSP脚本也可以从我们的网站上找到。 在本节中，我们假设过程A2到是图中图表的相对时间行为。这里我们使用CSP事件开始。其中N是数据类型Node上的值，表示相应药物的给药。节点：：= TG 不|TG G|EC C|EC ECSP事件结束。i其中i的范围大于N是表示子过程和图的错误终止的特殊事件，在我们的示例中，我们使用事件fin。0表示图的成功终止。为了验证第1节中的排序规则的临床干预集，我们利用CSP的稳定故障语义，也就是说，我们将属性验证问题转化为细化问题。下面的过程S是满足排序规则的最不确定的CSP过程S=开始。TG G → S H启动。EC E → SH开始。EC C → T H fin. 0 →跳过T=开始。EC E → S H开始。EC C→ T这里是相应的failure refinement断言。S± FA 2\{fin. 1，finn. 2，finn。3，开始。TGT}我们通过隐藏A2的al-phabet的一部分来抽象图的行为，因为我们感兴趣的属性只覆盖事件开始的集合。TG G，开始。EC E，开始。EC C，finn。0 ，即过程S的字母表。当我们要求FDR检查这个断言时，下面的反例就开始了。EC C，开始。TG G.这告诉我们事件开始了。TG G，表示在给予一定剂量的环磷酰胺之后可以给予一定剂量的吉西他滨，该迹线足以反驳我们的例子对顺序规则的正确性，因为一定剂量的表阿霉素必须在吉西他滨之后。依他滨的句法结构示意更详细的分析显示，虽然环磷酰胺可以在14天后给药，而表阿霉素只能在18天后给药，但紫杉醇在给药前可以延迟长达10天，并且由于吉西他滨允许在10天内给药，所以它可以在5天后给药，即在表阿霉素之前和环磷酰胺之后。一种可能的解决方案是限制环磷酰胺和表柔比星的给药持续时间我们选择了后者，因为它最大限度地减少了整体临床干预的变化我们通过在状态TG T和TG G之间包括延迟事件（itime状态）来实现这一点，延迟时间为16天。70P.Y.H. Wong，J.Gibbons/Electronic Notes in Theoretical Computer Science 229（2009）59FF∀·除了描述单个业务流程外，BPMN还可以用于指定业务协作，其中多个业务流程（参与者）通过消息流进行通信，非正式地说，如果参与者在消息流通信模式上进行合作，则该参与者与协作兼容。类似于在非定时模型上定义的兼容性概念[19]，我们使用CSP的响应性来形式化时间兼容性定义5.8时间兼容性。考虑到CSP流程所描述的一些协作，C=（m）i：{1. n} ·αTi<$Ti）\M其中，n的范围在N上，M是与其参与者之间的消息流相对应的事件集合，参与者的定时行为由过程Ti建模，参与者Ti相对于协作Ci是时间兼容的，j：{1.. n}\{i}·T i响应T j在我们的时间语义下形式化兼容性的一个结果是，由于响应性在[13]中是精化封闭的，时间兼容性也是精化封闭的。命题5.9给定参与者P i，其中i在某个指标集上变化，在某个协作C中是时间相容的，它们在下的精化在C中也是时间相容的。然而，细化闭包并不能捕获协作中所有可能的兼容参与者。具体来说，对于协作中的每个参与者，存在一个时间兼容的参与者类别，其中任何成员都可以替换它并保持时间兼容性。这个类可以通过稳定失效等价形式化这一概念扩大了我们以前在不定时环境中的定义[16]。定义5.10时间兼容类。给定某个局部图名p及其指定l，我们公理化地将其时间兼容的参与者类cfT（p， l）定义为一组对，其中每个对通过其环境和标识它的名称cfT：（PName×Local）→p：PName;l：LocalcfT（p， l）=P（P名称×本地）{pJ：PName; lJ：Local|(((tsem p l）\（αprocessp l\mg p l））±F（（tsem pJlJ）\（αprocesspJlJ\mg pJlj）（tsem pJlJ\（αprocesspJlJ\mg pJlJ））±F（tsem p l\（αprocessp l\mg p l））}P.Y.H. Wong，J.Gibbons/Electronic Notes in Theoretical Computer Science 229（2009）5971其中函数MG获取局部图的描述并返回一组 对应于该图的消息流的CSP事件这自然会导致对协作的特征或最抽象的时间兼容参与者的定义。第5.11章特殊的参与者给定某个参与者p的时间兼容类cp，在某个环境l中指定，对于某个协作c，cp的特征参与者，由一对名称和环境指定，由应用于cp的函数charT给出。charT：P（PName×Local）→（PName×Local）charT=（λps：P（PName×Local）·（μ（pJ，lJ）：（PName×Local）|mg pJlJ=α过程pJlJ（n（p， l）：ps·（tsem pJlJ±F（tsem p l（α过程pJlJ\mg pJlJ））下面的结果是命题5.9、定义5.10和5.11的直接结果。命题5.12如果在某个环境l中指定的时间相容类cp的特征参与者p对于某个协作c是时间相容的，那么cp中的所有参与者对于c也是时间相容6相关工作和结论在本文中，我们介绍了一个相对时间的语义BPMN在CSP中的模型和推理BPMN中描述的合作。 我们采用了在实时系统和定时协调语言中广泛使用的两阶段功能方法的变体[10]。我们展示了属性相关的非定时和定时模型的BPMN的局部和全局图，通过使用CSP的概念的响应性，并提出了一个例子来演示应用程序的语义模型。我们随后在Haskell中实现了语义函数的原型。据我们所知，本文描述了像BPMN这样的协作图形符号的第一个相对时间模型。已经进行了一些尝试为类似的符号提供时间模型，如UML活动图[6，8]和工作流网[11]。Gueli et al. [6]和Eshuis [8]在Clocked Transition System中定义了他们的离散时间语义模型，其中行为规范表示为时态逻辑公式，并通过模型检查进行验证;在Ling et al.的工作，他们定义了一个正式的语义范德阿尔斯特的工作流网的时间扩展尽管如此，它们的语义并没有提供明确建模时间所需的抽象级别，因为它们建模了离散的时间单位，我们相信这些时间单位可能72P.Y.H. Wong，J.Gibbons/Electronic Notes in Theoretical Computer Science 229（2009）59不直接适用于业务流程开发人员，而我们的定义捕获了W3C标准定义的六维空间[21，第3.2.6节]。 与BPMN不同的是，它们的目标图形符号以及它们的语义模型并不是为考虑多个图的协作分析而设计的此外，我们的语义模型已经被定义为与我们早期的无时间模型相对应[16]，因此时间无关的行为属性可以在两个模型中保留在非定时设置中，存在许多方法，其中引入了新的流程演算来捕获协作和编排中的兼容性概念。著名的作品包括Carbone et al。s End-Point and Glocal Calculi forformalising WS-CDL [2] and Bravetti et al.的编舞计算-lus捕获编排一致性的概念[1]。这两部作品都解决了形式不良的舞蹈编排问题，这是一类不可能正确投射的舞蹈编排。 虽然不良编排的概念与与我们对兼容性的定义和Bravetti等人[1]定义的契约细化概念类似，他们仅根据进程演算来定义他们的编排，没有明显的图形化规范符号，这可能更容易被领域专家访问。未来的工作将包括描述适合于BPMN的时间无关行为属性的类别;应用Dwyer等人作者非常感谢Bill Roscoe在这项工作中对响应性提出的有见地的建议。作者还想感谢匿名推荐人提供的有用建议和评论。这项工作由微软研究院资助引用[1] 马里奥·布拉维蒂和吉安路易吉·扎瓦塔罗。舞蹈编排与合同遵守的统一理论。第六届软件组合国际研讨会论文集（SC[2] Marco Carbone、Kohei Honda、Nobuko Yoshida、Robin Milner、Gary Brown和Steve Ross-Talbot。以通信为中心的并发程序设计的理论基础技术报告，W3C，2006年。[3] 马修湾作者：George S. Avrunin和James C.科比特用于有限状态验证的属性规范模式。在ICSEIEEEComputer Society Press，1999.[4] 海伦娜厄尔，卡洛斯卡尔达斯，海伦霍华德，珍妮特邓恩，和克里斯普尔。Neo-tAnGo一项采用分子谱、蛋白质组学和候选基因分析的序贯表阿霉素+环磷酰胺和紫杉醇+/-吉西他滨治疗高危早期乳腺癌的新辅助治疗研究，2004年。[5] 正规系统（欧洲）有限公司故障-分歧修正，FDR 2用户手册，1998年。 www.fsel. com.[6] 尼古拉斯·盖尔菲和阿梅尔·马马尔。时间活动图的形式语义及其PROMELA翻译。APSEC 05，第283-290页，2005年[7] Peter Hammand，Marek J.作者声明：John W.协议和危险法规中安全推理的形式化1995年10月，第19届计算机在医疗保健中的应用年度研讨会[8] 亨德里克·埃舒伊斯工作流程建模的UML活动图的语义和验证。博士论文，特温特大学，2002年。P.Y.H. Wong，J.Gibbons/Electronic Notes in Theoretical Computer Science 229（2009）5973[9] BPMN Modeler.可查阅http://www.ilog.com/products/jviews/diagrammer/bpmnmodeler/。[10] I. 林登，J. -M. Jacquet，K.De Bosschere和A.布罗吉论时间协调模型的表现力Sci. Comput.程序. ，61（2）：152[11] Sea Ling 和 H. 施 密 特 工 作 流 程 建 模 与 分 析 的 时 间 petri 网 2000 年 IEEE International Conference onSystems，Man，and Cybernetics，第3039[12] OMG. Business Process Modeling Notation（BPMN）Specification，2006年2月。www.bpmn.org网站。[13] J. N. Reed，J. E. Sinclair和A. W.罗斯科互操作组件的响应性。Form. ASP. Comput. ，16（4）：394[14] A. W.罗斯科 并发的理论与实践。 Prentice-Hall，1998年。[15] W. M.范德阿尔斯特。工作流程网的验证。在ICATPN[16] 彼得·Y H. 王和杰里米·吉本斯BPMN的进程语义。 在第10届正式工程方法国际会议上，2008年10月。出现。可在www.example.com上获得扩展版本http://web.comlab.ox.ac.uk/oucl/work/peter.wong/pub/bpmnsem.pdf。[17] 彼得·Y H. 王和杰里米·吉本斯ARelative-TimedSemantics for BPMN（extended version），2008.http://web.comlab.ox.ac.uk/oucl/work/peter.wong/pub/bpmntime.pdf。[18] 彼得·Y H.王和杰里米·吉本斯长期运行的实证研究。在Proceedings of 1st International Conference onModel Transformation，Volume 5063 ofLNCS，2008年7月。可在www.example.com上获得扩展版本http://web.comlab.ox.ac.uk/oucl/work/peter。 wong/pub/transext.pdf。[19] 彼得·Y H.王和杰里米·吉本斯业务流程兼容性。第八届国际软件质量会议论文集。IEEE Computer SocietyPress，August 2008.出现。[20] J. C.伍德考克和戴维斯。使用Z：规范，证明和完善。Prentice Hall International Series in ComputerScience，1996年。[21] XML Schema Part 2：Datashees第二版，2004年10月。http://www.w3.org/TR/2004/REC-xmlschema-2-20041028/.附录CSP在CSP [14]中，进程是一种行为模式;行为由事件组成，这些事件在环境和进程之间是原子的和同步的。在这种情况下，环境可以是另一个过程。事件可以是复合的，使用点运算符“.”构造;通常，这些复合事件表现为在进程和环境之间同步通信数据对象的通道。 由于篇幅的原因，我们只描述了该语言语法的一个子集 这是本文中使用的CSPP，Q：：= P| [答]|Q|P| [A|B]|Q|P\A|P Q Q|P H Q|e → P|Skip|停止e：：=x|X. e过程P| [答]|Q表示共享集合A中事件的进程P和Q的部分交织。过程P| [A|B]|Q表示平行合成，其中P和Q可以独立地演化，但必须在集合A和B中的每个事件上同步;74P.Y.H. Wong，J.Gibbons/Electronic Notes in Theoretical Computer Science 229（2009）59\H→HNHFTF∈∈集合A是P的字母表，集合B是Q的字母表，A和B可以分别在没有P和Q的合作的情况下发生进程PA是通过从P的环境中隐藏集合A中事件的所有出现而获得的。过程PQQ表示过程P和Q之间的外部选择;过程准备好表现为P或Q。进程P Q表示进程P或Q之间的内部选择，准备好至少表现为P和Q中的一个，但不一定是它们中的任何一个。对一组索引进程的内部选择写为i：I·P（i）。过程e P表示能够执行事件e的过程，在事件e之后， 它将像进程P一样运行。Stop进程是一个死锁进程，Skip进程是一个成功终止进程。CSP有三种指称语义：跟踪（），稳定故障（）和故障发散（）模型，以增加精度。 在本文中，我们的过程定义是无发散的，因此我们将集中讨论稳定故障模型。痕迹模型对于我们的目的来说是不充分的，因为它没有记录事件的可用性，因此只建模过程可以做什么，而不是它必须做什么[14]。值得