TimeAwareBPMN-js：基于Web的时间感知BPMN流程编辑器和验证工具

≥软件X 17（2022）100939原始软件出版物TimeAwareBPMN-js：用于Time-Aware BPMN流程的编辑器和时态验证工具Mario Ocampo-Pinedaa，Roberto Posenatoa， Francesca Zerbatoba意大利维罗纳大学计算机科学系b瑞士圣加仑大学ar t i cl e i nf o文章历史记录：收到2021年2021年12月3日收到修订版2021年12月3日接受保留字：BPMN时态过程建模时态约束网络动态能控性a b st ra ct本文介绍了TimeAwareBPMN-js，一个基于Web的图形化编辑器，用于时间感知的BPMN（业务流程模型和符号）模型，允许（1）创建和编辑丰富的BPMN流程具有时间约束，例如偶然的持续时间和条件，以及（2）验证这样的约束是良好定义的并且满足某些（时间）属性。时间约束的验证是通过插件实现的，由于应用程序的模块化架构，用户可以很容易地添加插件。不同的插件可以验证不同的时间属性。作为概念证明，TimeAwareBPMN-js包含CSTNU插件，该插件验证动态可控性属性，即，它在设计时检查是否存在满足所有时间约束的过程的运行时调度，而不管在执行期间如何揭示偶然的持续时间和条件。版权所有2021作者。由爱思唯尔公司出版这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）中找到。代码元数据当前代码版本v1.3此代码版本所用代码/存储库的永久链接https://github.com/ElsevierSoftwareX/SOFTX-D-21-00180Code Ocean compute capsule N.A.法律代码许可证MIT使用git的代码版本控制系统使用JavaScript、Java的软件代码语言、工具和服务编译要求，操作环境依赖性JVM 11，Node.js，bpmn-js-properties-panel，camunda-bpmn-moddle，jQuery，min-dash，tiny-svg，xmlbuilder，开发人员文档/手册https://gitlab.com/univr.di/TimeAwareBPMN/-/wikis/home问题支持电子邮件mario. univr.it1. 动机和意义业务流程模型被组织广泛用于设计、分析、实现和控制其业务流程。流程模型通常是在流程建模语言的帮助下指定的，例如业务流程模型和符号（BPMN）标准[1]。根据所使用的流程建模语言，流程模型可以捕获不同的视角。其中，我们发现控制流，即，流程执行的活动及其顺序、数据流透视图和∗通讯作者。电子邮件地址：mario. univr.it（Mario Ocampo-Pineda），roberto. univr.it（Roberto Posenato），francesca. unisg.ch（Francesca Zerbato）。https://doi.org/10.1016/j.softx.2021.100939时间透视[2]。最后一个是指广泛的过程在执行过程中需要满足的时间属性和约束。业务流程中时间约束的建模和验证是业务流程管理（BPM）社区长期研究的主题（最新调查见[3例如，存在将BPMN [4，5]的扩展与时间自动机（例如，[6[5，9，10]），以及基于时间约束网络的方法（例如，[11[16]）。在[17]中，作者引出了一组十种时间模式，与业务流程和活动的建模和控制相关的时间方面。在这些模式中，活动之间的持续时间和时间滞后似乎是实践中最常见的。在2352-7110/©2021作者。 由Elsevier B.V.出版。这是一篇开放获取的文章，使用CC BY许可证（http://creativecommons.org/licenses/by/4.0/）。可在ScienceDirect上获得目录列表SoftwareX期刊主页：www.elsevier.com/locate/softxMario Ocampo-Pineda、Roberto Posenato和Francesca Zerbato软件X 17（2022）1009392特别地，持续时间允许限制执行过程元素所需的时间跨度[17]。近年来，研究人员指出，需要区分两种持续时间限制：可控和偶然。可控制的持续时间是相对于由执行流程的代理管理的流程活动（以下称为可控活动）而言的。相反，或有持续时间是相对于由外部代理人管理的其他活动（以下称为或有活动）而言的，该过程只能在活动执行后观察持续时间[11]。通常，持续时间约束在设计时指定为时间间隔，用于定义持续时间段的最小值和最大值时间滞后，也称为相对约束[11]，限制任何两个过程活动的开始/结束时刻之间的时间距离（参见。[17]中的TP1）或任意事件（参见TP3在[17]中）。给定时间感知过程模型，即，流程模型，如果指定了时间约束，则可以在设计时检查不同的属性，以确保正确执行流程一个有趣的属性是动态可控性，它保证有可能以这样一种方式调度所有可控活动，即在给定应急活动的所有可能持续时间的情况时间约束网络是用于建模和解决时间问题的最精细的模型之一[18，19]，包括动态可控性检查。时间约束网络是动态可控的，如果它是可能的，以确定一个schedule，给定到目前为止执行的活动，递增地确定哪些活动可以开始（和可控的，他们的持续时间），以满足所有的时间约束。在本文中，我们介绍了TimeAwareBPMN-js，这是一个能够对时间感知BPMN模型进行建模和验证的工具[20]。建模是通过GUI编辑器实现的，该编辑器允许对定义良好的时间感知BPMN流程进行建模。时态属性的验证是基于插件的，这些插件可以使用用户定义的技术来检查不同的时态属性。作为概念验证，该工具具有CSTNU插件，该插件能够验证时间感知BPMN过程的动态可控性，将该过程转换为等效的具有不确定性的条件简单时态网络（CSTNU）并利用其检查算法[21]。1.1. 相关工作在文献中，有许多关于在BPMN过程中管理临时方面的建议。然而，只有少数人提供了一个工具，可以直接用来检查的consis-tency/可控性的时间属性。下面，我们按时间顺序概述这些建议。在[22，23]中，作者提出了从BPMN 2.0的扩展版本到定时通信顺序流程模型（CSP+T）的转换。BPMN扩展允许定义任务的持续时间约束和活动之间的相对约束。这种方法的主要贡献是在CSP术语方面为定时BPMN元素定义了形式语义。这两个提案都没有提供一个现成的工具来转换到CSP及其检查。在[7，20]中，作者提出表示绝对和相对时间约束，并分析这种扩展的BPMN模型的行为，对于建模，他们建议扩展ActivitiEclipse设计器（http://www.activiti.org/），而对于验证，他们只提供了一种方法来支持转换到时间自动机，而没有提供工具。一旦确定了一个时间自动机，它就可以被UPPAAL Tiga工具[24]分析，以检查可能的死锁或最后期限违规。在[25]中，作者提出了一种工具ATAPIS，它允许管理具有[12]中描述的许多时间属性/约束的业务流程。该工具以扩展的ADEPT2表示法[26]表示业务流程，其中时间属性的指定是直接和直观的。在ATAPIS中，通过将模型转换为CSTNU实例[21]并使用 CSTNU 的 检 查 算 法 来 检 查 业 务 流 程 的 动 态 可 控 性 使 用ATAPIS，可以以集成的方式设计，检查和管理可能的不一致性，而不需要任何外部工具或时间约束网络知识。在[27]中，作者提出了将BPMN元素的子集编码到Maude中，Maude是一个重写逻辑系统，他们还提出了如何表示编码任务和流的持续时间约束。这种时间约束被定义为随机表达式，而概率被用来表示网关中的各种形式的分支行为在论文中，作者还提出了一些案例研究检查定时进程，但没有提供一个现成的工具来设计和检查模型。在[28]中，作者提出了BPMN的时间相关元素的形式语义，支持事件、时间信息类别（日期-时间、持续时间、周期）和BPMN标准规定的相应ISO-8601描述的不同组合。然后，直接根据一阶逻辑定义所提出的语义，然后在Alloy [29]中进行翻译，以支持过程的形式化验证。作为同一作者指出，所提出的工具仅允许对研究案例模型的子集进行语义验证，但是在表1中，我们提供了用于管理时间方面的上述方法的比较。对于每种方法，我们报告它是否支持BPMN流程的建模，一些常用的时间模式[12]，动态可控性属性的检查，最重要的是，它们是否提供了一个集成的现成工具。这样的工具应该允许用户设计具有时间约束的过程模型并验证时间属性，而不需要用户进行其他外部操作，例如将模型转换为其他格式和/或使用外部应用程序。据我们所知，只有ATAPIS [25]和TimeAwareBPMN-js提供这样的工具，ATAPIS基于ADEPT 2，TimeAwareBPMN-js基于BPMN。2. 软件描述TimeAwareBPMN-js是一个Web应用程序，它扩展了Bpmn-js工具包-Camunda开发的BPMN编辑器[31]-来建模和验证时间感知的BPMN模型。2.1. 软件构架TimeAwareBPMN-js是一个Web以这种方式，可以利用以不同语言编写的桌面应用程序/库，否则它们不能在浏览器（客户端）内执行具体来说，客户端是BPMN Web编辑器bpmn-js [31]，扩展为（1）对时间感知的BPMN流程进行建模，（2）提供以插件形式实现的不同验证工具，以及（3）通过HTTP协议与服务器应用程序交互。服务器是一个Node.js应用程序，在第一次交互时，返回BPMN编辑器，然后处理Mario Ocampo-Pineda、Roberto Posenato和Francesca Zerbato软件X 17（2022）1009393一CFGH我J表1总结了文献中支持业务流程中时间约束建模和验证的不同方法。标签“计划"表示该功能目前正在开发中随时间变化循环元素计划动态可控性？✓×✓××✓集成工具？×部分×部分Fig. 1. 客 户 端和服务器插件之间交互的框图。客户端通过运行服务器端插件来执行验证，边缘图标是一个新的按钮，用于添加边表示-根据所请求的任何两个BPMN元素之间的相对约束来确定时间约束[13]。时间属性图1显示了TimeAwareBPMN-js的框图中与客户端插件和相应的服务器端插件之间的交互相关的部分，以强调插件如何工作。应用程序的界面由两部分组成：1. 一个图形编辑器，使建模/编辑的过程丰富的时间约束，如下所述;2. 一个工具栏，可以选择要激活的插件，并根据所选插件选择可用的操作。图2描绘了TimeAwareBPMN-js界面的屏幕截图，显示了图形编辑器（区域1）和包含可能操作按钮的工具栏（区域2）。调色板包含可用于设计模型的BPMN元素。用蓝色框起来的范围，比如b，代表BPMN元素（比如Tasks和catching Events）的偶然持续时间约束。当范围有误差时，例如，最小持续时间大于最大持续时间，则帧变红（例如，d）。绿色边框的范围表示网关等元素的持续时间约束。绿色是为了强调这种框架范围可以通过时间验证算法来限制，以保证某些属性（如果需要）。相反，蓝框范围，即，连续的值不能被修改，并且验证算法必须保证在运行时可以使用这种范围的任何值。长虚线双短虚线边缘是任务T1和T4之间的相对约束的示例。该面板显示了元素属性面板的新选项卡，用于编辑所考虑元素的时间约束（例如，在图中，选项卡显示了用户任务的最小持续时间和最 大 持 续 时 间 T4 ） 。 下 拉 列 表 Temporalconstraintverification允许选择要使用的验证插件。可能的操作（线上的按钮）会根据所选插件自动更新。 图 2、所选插件为CSTNU，具有动作验证条件、节奏验证、下载CSTNU、重置颜色等功能。Browse按钮允许从文件加载时间感知的BPMN模型，而Save按钮允许将表示的模型作为XML文档下载。2.2. 软件功能TimeAwareBPMN-js的主要和新颖功能是：对BPMN元素的相关子集进行建模，每个元素通过时间约束或用于表示时间约束的属性进行扩充;任何一对BPMN元素之间的相对约束的建模，以表示不同类型的时间滞后[13，17];通过在应用程序中集成为插件的外部工具对BPMN过程中定义的时间约束和属性进行验证。e··Reference Capel，Men-Doza[23]，Moraleset al. [22日]Cheikhrouhou等人 [20、30]ATAPIS[25]Durán等人[27日]Houhou等人 [28日] 我们的工具2011年20132016201820212021时态推理的形式化CSP+T时间自动机CSTNUMaudeFOLCSTNU o.BPMN支持？✓✓×✓✓✓时滞✓✓✓✓✓活动持续时间✓✓✓✓✓·Mario Ocampo-Pineda、Roberto Posenato和Francesca Zerbato软件X 17（2022）1009394F¬¬图二. TimeAwareBPMN-js界面截图。TimeAwareBPMN-js编辑器允许管理基本BPMN元素的一个子集，并通过时间约束和属性进行增强。与文献[6，13]一致，我们考虑使用时间约束元素进行增强，这些元素允许对基本控制流模式进行建模，并专注于现实场景中常用的流对象此外，我们允许用户对基本数据、泳道和工件元素进行建模，尽管我们没有用时间约束来增强它们表2总结了我们的工具所支持的BPMN的完整集合，报告，对于每个BPMN 元素，可以在其上定义哪些时间约束和属性。列Minduration和Max duration表示限制执行元素的时间范围的两个约束。色谱柱条件？指定持续时间约束是否假定为偶然的。一个命题标签是一串布尔文字（例如，p，p），其表示用于应用元素的时间约束的条件。例如，命题标签p q表示，当条件p为真而条件q为假时，必须遵守与元素相关的时间约束。一个空的命题标签表明， 当执行元素时，必须始终遵守元素的时间约束。 模型的可能布尔条件在异或（XOR）网关中定义并设置在执行网关时的运行时间。我们的时间感知BPMN流程模型[13]只允许二进制XOR网关用于表示执行1的替代流程。 在运行时，当执行XOR网关时，系统评估与XOR网关相关联的条件，然后执行与条件的真值相关联的分支。在XOR网关中观察到的条件的真值存储在布尔变量中，其名称可以由用户在独占网关的属性面板的时间约束选项卡或由程序直接分配。 这样一个变量的名称存储在属性Observed命题中（参见表2）。例如图2、不同的任务必须1如果有两个以上的可选执行流程，则可以将它们表示为级联两个或更多个二进制XOR网关根据选择的付款方式执行。从控制流的角度来看，不同的任务必须放在两个可选的流上。XOR Split网关观察条件并将真值存储在变量中p.通过这种方式，关于任务“授权信用卡”的时间约束一般来说，隐式命题标签由程序自动为所有元素确定这样的隐式命题标签可以由用户定制以扩展或限制相关联的约束的适用性。在此版本的TimeAwareBPMN-js编辑器中，时间被视为离散的，并且时间约束值被表示为整数，而没有显式的时间粒度。因此，用户必须固定适当的时间粒度（例如，分钟、秒），允许将所有时间约束表示为整数值。2.2.1. 相对限制条件TimeAwareBPMN-js编辑器允许指定流对象对之间的相对约束（即，活动、事件和网关），如[13]中所述。相对约束限制执行的两个给定时刻之间的时间距离。它指定给定时间间隔、两个相对时刻和命题标签（用于可能定制其适用性）。 给定一对流对象，第一个时刻可以是第一个元素的开始或结束，而第二个时刻可以是第二个元素的开始或结束 只有对于BPMNStart（none）和End（none）元素，开始和结束时刻是相同的，因为这些流元素被定义为瞬时事件。例如，在图2中，任务T1和T4之间的边是使用按钮e绘制的相对约束。约束的详细信息如下所示在其时间约束选项卡（如图3所示）中：它将T1的开始时刻和T4的结束时刻之间的时间距离限制为区间[2， 18]中的值。Mario Ocampo-Pineda、Roberto Posenato和Francesca Zerbato软件X 17（2022）1009395表2该工具支持的BPMNProcess元素的完整列表，包括通过时间约束增强的流对象✓ ：可配置约束;×：不适用约束BPMN元素最小持续时间最大持续时间命题标号任务应急？观察到命题相对约束的源/目标？用户任务服务任务脚本任务发送任务接收任务✓✓✓✓✓✓✓✓✓✓✓✓✓✓✓是的是的不是的×××××✓✓✓✓✓事件开始（无）结束（无）××××××不不××✓✓中级捕捞计时器中级投掷✓连接对象序列流关联✓×✓×××不不××××泳道泳池（单人）车道××××××不不××××数据数据对象数据存储××××××不不××××伪影文本注释×××没有××2.2.2. 时间属性时间感知BPMN流程中的临时约束意味着检查这些约束的定义至少是一致的。例如，如果两个活动必须至少持续5分钟（由两个时间约束指定），则不可能有将两个活动的总执行时间限制为9分钟的约束然而，这使得验证任务更具挑战性，因为时间约束可以具有不同的属性（可控的，偶然的，有条件的）。如在第1节中已经介绍的，验证任务可以是验证模型是否是动态可控的，即，可以调度所有可控制的任务，使得对于偶发任务的任何持续时间都满足所有时间约束。另一个验证任务可以是验证哪些任务可以在给定的最后期限内完成而没有任何约束违反。换句话说，这样的时间验证任务应该是灵活的，用于检查模型的不同时间属性。因此，我们选择将验证任务的执行委托给插件，即，可添加的软件模块到TimeAwareBPMN-js来验证当前BPMN模型是否满足时间属性。每个插件都可以运行外部软件/库，以通过API实现检查由TimeAwareBPMN-js提供。作为概念验证，TimeAwareBPMN-js随插件CSTNU插件一起分发，该插件可以检查模型的动态可控性。具体来说，CSTNU插件将当前BPMN模型转换为CSTNU的相应实例模型采用[13]中提出的方法。然后，它使用一个外部库，CSTNU工具[32]，用于检查这样的网络的动态可控性。在[13]中，作者考虑了一个更丰富的时间感知BPMN模型，其中选择可以是观察（如果其值由环境决定）或决策（如果其值由流程的执行者决定）。 然后，他们证明了这种时间感知BPMN模型的进程的动态可控性等价于相应CSTNUD实例的动态可控性。CSTNUD实例是一个CSTNU实例，其中也有表示决策的布尔变量，与观测值相比，必须以不同的方式进行管理[33]。由于在TimeAwareBPMN-js中我们不表示决策，因此所提出的实例转换总是确定具有零决策的CSTNUD，即，CSTNU。因此，我们的时间感知BPMN模型的动态可扩展性等同于相应CSTNU实例的可控性CSTNU插件中的动态可控性检查还最小化了非偶然的持续时间范围，删除了所有不能使用的持续时间值。然后，如果模型是动态可控的，插件将更新所有的时态约束（但不包括偶然的约束，因为它们不能被修改），并将结果显示给用户。如果模型不是动态可控的，插件会向用户显示一条消息，提供在流程模型中发现的不一致的详细信息。一般来说，CSTNU插件验证时间对于具有多达20个活动的BPMN模型来说大约是时间在很大程度上取决于XOR网关的数量和配置。[21]作者认为，消息信号✓ ✓ ✓✓ ✓ ✓不不××✓✓网关并行（AND）异或（XOR）✓ ✓ ✓✓ ✓ ✓不不×✓✓Mario Ocampo-Pineda、Roberto Posenato和Francesca Zerbato软件X 17（2022）1009396图3.第三章。T 1 和 T 4 之 间 相 对 约 束 的 “ 时间约束”选项卡。一些随机实例具有10个活动和多达5个XOR网关，需要多达103秒来验证（最坏情况分析）。这些实例的特征在于XOR网关是按顺序的，并且存在依赖于所有XOR选择的全局相对约束2.2.3. 实现细节在本节中，我们将给出一些关于插件如何工作的实现细节。让我们假设一个用户想要使用一个外部库，它提供了一些方法，这些方法对于在时间感知的BPMN流程中检查一些时间属性非常有用。 通过添加两个插件，一个用于客户端，一个用于服务器，可以在TimeAwareBPMN-js中使用这样的库。客户端插件的目标是：（1）提供与特定动作相关的按钮，用户可以通过这些按钮请求验证某些时间属性，（2）将带有所有必要数据的请求发送到服务器，以及（3）接收并显示结果。服务器端插件的目标是：（1）接受验证请求，（2）调用关联库的方法实现验证，（3）返回结果。为了方便地集成这样的插件对，TimeAwareBPMN-js提供了一个JavaScript API，允许插件与应用程序.使用TimeAwareBPMN-jsAPI将这两个插件实现为JavaScript模块并将它们保存在特定目录中以使插件立即可用就足够了。3. 说明性实例在本节中，我们将给出一个示例，说明如何使用该工具来验证时间感知的BPMN模型。操作的一般流程可以按以下步骤组织1. 用户可以通过从选项板中添加所需的元素和连接器，并使用Web编辑器中提供的时间约束面板设置时间约束，来创建新的BPMN模型。或者，用户可以使用工具栏中的Load按钮加载BPMN模型。例如图在图2中，用户创建了一个简单的流程模型，其中包含一个开始事件、四个用户任务（T1、T2、T3和T4）、两个独占网关（G1和G2）、一个消息事件（IE1）和一个结束事件（e）。最小和最大持续时间约束已指定为所有任务，中间事件，网关使用其时间约束面板，（图。2有T4面板的例子）。此外，该过程还包含任务T1和任务T4之间的相对约束。2. 一旦指定了所有的时间约束，用户可以选择插件，使用工具栏中的时间约束验证下拉列表来验证模型的时间约束。在图2中，用户选择了CSTNU插件。3. 然后，用户可以选择插件中可用的操作之一例如，时间验证检查所有时间约束是否定义良好。 如果时间约束没有明确定义，例如，分钟持续时间>最大持续时间，该工具报告错误，显示描述错误和相关约束的窗口。一个例子显示在子面板a的图。 四、如果所有约束都定义良好，该工具将验证模型的动态可控性，将过程转换为等效的CSTNU实例并验证其动态可控性。4. 在运行时间验证之后，结果将以消息的形式呈现，并更新流程模型。图1中的子面板b-d图4描绘了验证的三种可能结果：过程是动态可控的，并且不需要更新它（b），过程是动态可控的，并且一些约束需要更新（c），以及过程不是动态可控的（d）。如果模型更新后，更新后的元素的边框颜色会发生变化。如果模型不是动态可控制标记的，该工具将更新确定“不可控制”状态的元素的框架颜色4. 影响和结论在这项工作中，我们描述了TimeAwareBPMN-js，一个用于建模和验证时间感知BPMN模型的Web应用程序。至于应用程序的影响，我们设想它可以用于不同的目的，并支持各种应用环境中的研究人员：时间感知BPMN模型简介 该应用程序可以帮助研究人员研究如何在BPMN模型中建模时间约束。实际上，研究人员可以加载表示流程模型的任何BPMNv2XML文件，并使用不同的时间约束来丰富它，以表示运行时需求。由于该应用程序允许以简单的方式验证时间约束，因此将促进这种研究结果。此外，该应用程序允许将所有时间约束保存为BPMN文件中的扩展元素，以简化其分布。事实上，在BPMN模型中研究时间约束并不像看起来那么容易。例如，具有不同命题标签的相对约束和偶然约束的相互作用可以容易地导致运行时·Mario Ocampo-Pineda、Roberto Posenato和Francesca Zerbato软件X 17（2022）1009397见图4。时间验证操作显示的消息示例。（a）时间限制定义中的错误。（b）成功的时间验证结果，而无需修改模型。（c）具有更新元素的成功时间验证结果，以黄色框表示。 （d）时间验证结果不成功导致不可控制执行的元素用粉红色框住无法在没有错误的情况下执行的配置。TimeAwareBPMN-js有助于理解这种相互作用，显示可能的不一致性。一种新的时态验证算法框架。在时间感知的过程模型领域，不同的命题处理的表示和检查的时间约束和属性的BPMN模型。许多提案要求将BPMN模型转换为其他格式，并使用LoLA [34]或UPPAAL [24]等外部工具进行检查。TimeAwareBPMN-js架构旨在将此类转换和外部工具执行集成为应用程序的插件。这样的插件可以很容易地构建和集成，这要归功于应用程序API。使用插件，用户可以专注于模型的逻辑方面，而不必担心将BPMN转换为其他形式主义或与外部工具的连接所产生的问题。应用. 在BPM领域，人们对考虑工作流系统中的时间方面非常感兴趣[2，3，12这些建议的一个关键方面是缺乏一个实际的应用程序，允许使用这种时间感知（BPMN）模型。这个应用程序将有助于时间感知BPMN模型的传播，提供一个坚实的和可扩展的框架来验证时间感知BPMN流程。在未来的工作中，我们计划扩展TimeAwareBPMN-js，以简化时间约束的编辑，表示固定日期约束，其他BPMN元素中的时间约束-例如循环，边界事件和子流程-并提供有关流程中可能出现的不一致性的竞合利益作者声明，他们没有已知的竞争性财务利益或个人关系，可能会影响本文报告的工作致谢我们要感谢匿名审稿人以及维罗纳大学计算机科学系的CarloCombi教授和Barbara Oliboni教授对手稿的评论。资金这项工作得到了INdAM-GNCS项目2020的部分支持医疗和商业引用[1]对象管理组。业务流程模型和符号版本2.0.2. 2014年，[2021年7月7日访问]。https://www.omg.org/spec/BPMN/2.0的网站。2/PDF。[2]放大图片作者：Eder J，Panagos E，Rabinovich M.工作流时间管理重新审视。 在：对信息系统工程的种子贡献：25年的CAiSE。Springer; 2013，p.207-213. http://dx.doi.org/10.1007/978-3-642-36926-1_16.[3]Cheikhrouhou S，Kandas S，Guermouche N，Jmaiel M.业务流程建模中的时 间 视 角： 调 查 和 研 究 挑战 。 面 向 服 务 的计 算 应 用 2015;9 （ 1 ） ： 75-85.http://dx.doi.org/10.1007/s11761-014-0170-x.[4]放大图片作者：Gagne D，Trudel A. Time-BPMN。2009年IEEE商业和企业计算会议。2009，第361-367页。http://dx.doi.org/10.1109/CEC.2009.71。[5]Combi C，Oliboni B，Zerbato F. BPMN中持续时间约束的规范和管理的模块化方法84.第八十四章：一个人111-144.http://dx.doi.org/10.1016/j.is.2019.04.010网站。[6] 放大图片作者：Lanz A，Weber B，Reichert M.流程感知信息系统的时间模式。RequirEng2014;19（2）.113-141.http://dx.doi.org/10.1007/s00766-012-0162-3，orgname = Springer.[7]Cheikhrouhou S，Kandas S，Guermouche N，Jmaiel M.增强业务流程中时间 约 束 的 形 式 化 规 范 和 验 证 。 2014 年 IEEE International Conference onServicesComputing。2014年，第701-708页。http://dx.doi.org/10.1109/SCC.2014.97网站。··Mario Ocampo-Pineda、Roberto Posenato和Francesca Zerbato软件X 17（2022）1009398[8] 作者：Jiang Jiang，Jiang Jiang，Jiang Jiang具有时间和资源约束的业务过程的形式化验证。2011 IEEE International Conference on Systems，Man，andCybernetics（IEEE系统、人与控制论国际会议）2011年，第1173-118. 网址：//dx.doi.org/10.1109/ICSMC.2011.6083857网站。[9] Huai W，Liu X，Sun H.通过业务流程模型验证实现可信的组合服务。2010年第七届泛在智能计算国际会议和第七届自主可信计算国际会议。2010，第422-427页。http://dx.doi.org/10.1109/UIC-ATC.2010.114.[10]Combi C，Oliboni B，Zerbato F.在BPMN 2.0中建模和处理持续时间约束。在：应用计算研讨会的会议记录，SAC '17。ACM; 2017，第727-734页。http://dx.doi.org/10.1145/3019612的网站。3019618.[11]波塞纳托河，孔比C时态概念工作流模式的可控性。在：业务流程管理，第七届 国 际 会 议 ， BPM 2009 。 LNCS ， vol. 5701 ， Springer; 2009 ， p. 64-79.http://dx.doi.org/10的网站。1007/978-3-642-03848-8_6。[12]杨伟华，王伟华，王伟华.在模块化流程中控制时间意识。在：企业，业务流程和信息系统建模。BPMDS 2016，EMMSAD 2016.商业信息处理讲义，Springer; 2016年，第157-172页。http://dx.doi.org/10的网站。1007/978-3-319-39429-9_11。[13] Posenato R，Zerbato F，Combi C.管理决策任务和事件时间感知业务流程 模 型 。 在 ： 业 务 流 程 管 理 员 。 BPM 2018.. 2018 年 ， 第 102-118 页 。http://dx.doi.org/10.1007/978-3-319-98648-7_7 ， orgname = Springer ，series=LNCS，volume=11080，isbn=978-3-319-98648-7.[14]张文龙，王文龙，王文龙.在模块化流程中管理时间意识。软件系统建模2019;18（2）. 1135-1154. 网址：//dx.doi.org/10.1007/s10270-017-0643-4网站。[15] Franceschetti M，Eder J.半偶然任务持续时间：表征和可控性。高级信息系 统 工 程 国 际 会 议 （ CAISE ） 。 Springer; 2021 ， p.246-261 。http://dx.doi.org/10.1007/978-3-030-79382-1_15。[16]Maggi FM，Montali M，Peñaloza R，Alman A.扩展具有不确定性的时态业务约束。在：业务流程管理。BPM 2020。12168，Springer; 2020，p. 35-54.http://dx.doi.org/10.1007/978-3-030-58666-9_3.[17]杨伟杰，李伟杰，李伟杰.流程时间模式：正式基础。Inf Syst 2016;57：38-68.http://dx.doi.org/10.1016/j.is.2015.10.002网站。[18] Dechter R ， Meiri I ， Pearl J. Temporal constraint networks. 人 工 智 能1991;49（1）：61-95.http：//dx.doi.org/10.1016/0004-3702（91）90006-6.[19]Schwalb E ， Vila L. 时 间 限 制 ： 调 查 。 限 制 1998;3 （ 2 ） . 129-149.http://dx.doi.org/10.1023/A:1009717525330网站。[20]Cheikhrouhou S，Kandas S，Guermouche N，Jmaiel M. BPMN 2.0中以时间为中心的业务流程建模在：信息集成和基于Web的应用服务国际会议。ACM; 2013 年 ， 第 154-163 页 。 http://dx.doi.org/10.1145/2539150.2539182 网站。[21]Hunsberger L，Posenato R.不确定条件简单时态网络动态可控性检验的健全完备算法。在： 第25届国际研讨会上的时间表示 和推理（时间2018 ）。LIPICS，vol.120，2018，p.14：1-14：17。网址：//dx.doi.org/10.4230/LIPIcs.TIME.2018.14网站。[22]Morales LEM，Tuñón MIC，Pérez MA.一种用于业务流程组合验证的时间BPMN 形 式 化 方 案。 在： 企 业 信 息 系 统 。 商 业 信 息处 理 讲 义 ， Springer;2011，第388-403页。 http://dx.doi.org/10.1007/978-3-642-19802-1_27.[23]Capel MI，Mendoza LE.自动化从BPMN模型到CSP+t规范的转换。2012年第35 届 IEEE 软 件 工 程 研 讨 会 。 2012 年 ， 第 100-109 页 。http://dx.doi.org/10.1109/SEW.2012.17网站。[24]杨文，杨文. UPPAAL-实时系统自动验证的工具套件。在：混合动力系统III.Springer; 1996，p. 232-243. http://dx.doi.org/10.1007/BFb0020949网站。[25]ATAPIS-自适应时间和过程感知信息系统。2019年，URLhttps://www.uni-ulm.de/en/atapis。[26]Goser K，Jurisch M，Acker H，Kreher U，Lauer M，Rinderle-Ma S，et al.Next- generation process management with ADEPT 2.收录于：第五届业务流程管理国际会议上的BPM演示程序会议录。2007年，p. 四、[27]Durán F，Rocha C，Salaün G.重写逻辑中BPMN随时间的随机分析。2018年科 学 计 算 计 划 ;168 ： 1-17 。 http://dx.doi.org/10 的 网 站 。1016/j.scico.2018.08.007。[28] Houhou S，Baarir S，Poizat P，Quéinnec P. A direct formal semantics对于BPMN时间相关的构造。第16届软件工程新方法评估国际会议论文集。SCITEPRESS;2021，第138-149页。http://dx.doi.org/10.5220/0010462901380149.[29]杰克逊·D软件抽象：逻辑、语言与分析。MIT Press;2012.[30]Cheikhrouhou S，Kaghos S，Jmaiel M. 以时间为中心的业务流程模型的验证 。 2014 年 IEEE 第 23 届 国 际 WETICE 会 议 。 2014 ， 第 326-331 页 。ht