本发明涉及一种工作网系统数据流错误检测的技术领域，特别是涉及一种业务流程设计缺陷的检测方法、可读存储介质及终端。
背景技术：
近年来，信息技术的不断发展使得系统的业务流程或工作流设计成为各个组织与企业间的重要应用技术。设计良好的系统，不仅需要具备完善的业务功能(无业务死角等)及流畅的用户体验(无崩溃或卡死等)，而且还要避免由不正确的业务数据(不一致数据、缺失数据等)而引发的有损用户利益的安全问题。因此，系统的正确性不仅需要考虑业务逻辑，还需关注业务数据的功能需求，这些需求往往体现在用户数据值的变化上。数据在业务交互过程中也享有一定的约束条件，使得符合规范的数据才能被运行，而当数据值异常时可以及时得到反馈。我们建立了可以捕捉数据的值及其动态变化的形式化网模型(wft网)，利用这个模型模拟数据在业务流程运行过程中的变化，不仅可以更加详细的描述数据的相关性质，还扩展了广泛用于验证系统业务流程正确性的合理性这一性质，使得新的合理性可以从业务逻辑的正确和数据需求的满足这两个方面来进行系统正确性的判断，同时也是业务流程设计缺陷的检测。
以往也有针对系统业务流程设计错误检测的方法研究，包括基于petri网的方法、基于图论的方法、基于逻辑验证的方法以及基于本体论的方法。其中一类特殊的petri网也就是工作流网(wf网)，其合理性分析作为一种全面的分析方法得到广泛应用。但是这些研究大部分都是基于业务逻辑层次的，所检测的也是系统运行有无死锁、活锁或死变迁，并没有考虑业务流程中数据所扮演的角色，进而忽视了流程运行时因数据参与而引发的问题。而事实上，数据是业务流程运行必不可少的部分，首先业务实例需要数据才能启动，并且业务活动的执行往往受到一定的数据约束，同时活动的执行也促使数据的演化(生成与消耗等)。介于上述这些形式化方法模型并不能将数据融入到业务流程的分析中，因此一些基于原网的扩展模型相继被提出，例如带有数据的工作流网(wfd网)和颜色工作流网(cwf网)，这些网模型考虑了流程运行过程中数据的变化及其对活动的路由控制。但是在这些网模型中，数据被高度抽象成定义或未定义，无法捕捉其具体赋值，对于数据值的变化及其本身需要满足的约束条件等情况无法描述，因此基于这些网模型的正确性验证、合理性分析依然只是针对业务逻辑层面的。总之，不论是工作流网还是其现有的扩展模型，虽然它们能够用来验证系统业务逻辑设计是否正确，但它们对于由数据值变化而引起的业务异常却不可分析，已经无法完全概述系统对于业务数据的功能需求。
技术实现要素：
鉴于以上所述现有技术的缺点，本发明的目的在于提供本发明的一种业务流程设计缺陷的检测方法、可读存储介质及终端，用于解决现有技术中业务流程数据的值被篡改或不当操作而引起的系统数据需求不被满足的异常情况。
为实现上述目的及其他相关目的，本发明提供一种业务流程设计缺陷的检测方法，包括以下步骤：根据待测系统的业务流程，以及业务逻辑、流程数据及所述流程数据对业务活动的控制约束，构建成所述待测系统的wfd网；根据所述流程数据与数据库间的交互，在所述wfd网基础上构建所述待测系统的wft网；根据所述wft网的结构特征，以及所述数据库对所述流程数据的数据约束，利用数据精炼方法对所述待测系统的流程数据赋以具体值；根据数据精炼技术，将所述业务活动的使能条件和发生规则转换为所述wft网的执行语义，生成可达配置图；根据所述wft网，采用线性时序逻辑方法构建所述wft网的合理性分析方法，判定所述wft网的合理性，获得所述待测系统的合理性判定结果。
于本发明的一实施例中，所述采用线性时序逻辑方法构建所述wft网的合理性分析方法包括采用一阶线性时序逻辑的方法分别从控制流和数据流构建所述wft网的合理性分析方法。
于本发明的一实施例中，所述构建待测系统的wft网的方法包括：构建8元组的工作流网
于本发明的一实施例中，所述流程数据的赋值精炼，包括：对所述wft网n中的流程数据d，其值域为bd，d在状态c下的赋值集合为vd，计算所述数据库中与d相关的数据表的集合
于本发明的一实施例中，所述可达配置图的生成，包括：对所述wft网n，给定起始配置c0，将c0作为可达配置图的根节点，并标记为新；对除所述根节点以外是否存在标记为“新”的其他节点进行检测，根据检测结果执行第一生成操作；其中，所述第一生成操作包括：若其他节点中均不包含标记为“新”的节点，则所述可达配置图生成结束，输出n的可达配置图rg(n)；若存在标记为“新”的节点，任意选择一个“新”的节点，记为配置c，并在所述配置c下根据变迁的状态执行第二生成操作；其中，所述第二生成操作包括：若在配置c下，不存在任何变迁有发生权，则将c标记为“终止”节点，并继续对除所述根节点以外的其他节点进行检测，以及根据检测结果执行所述第一生成操作；若在配置c下，变迁t1,…,tn(n≥1)有发生权，对每个变迁ti(1≤i≤n)进行第三生成操作；其中，所述第三生成操作包括：根据发生规则计算发生ti后生成的新配置c1,…,cm(m≥1)，对每个新配置ci(1≤i≤m)，判断ti未发生前的配置图中是否已经存在该ci；若存在，那么将原本指向ci的箭头指向这个与ci相同的配置；若不存在，那么将ci记录到配置图中，且生成一个箭头从c指向ci，在箭头上添加标签t，并将ci标记为“新”；去掉配置c的“新”标记，并继续对除所述根节点以外的其他节点进行检测，以及根据检测结果执行所述第一生成操作。
于本发明的一实施例中，所述控制流正确性的判断方法，包括：在所述wft网n的可达配置图rg(n)中，将连接所述根节点c0到单个所述终止节点cf的一条配置序列为n的一条执行路径，记为ρ:c0c1…cf，且将路径ρ中所有触发变迁构成的集合记为tρ，令t为n的变迁集合；在默认循环只执行一次的情况下，基于rg(n)计算n所有可能的执行路径，依次记为ρ1,…,ρn，其中ρi:ci0ci1…cif(1≤i≤n)，对每个ρi中的终止节点cif进行判断，包括：若配置cif中的标识为含有n中的非终止库所含有托肯，也就是cif不是n的终止配置，则设定n的控制流为不合理；若配置cif中的标识为有且仅有n中的终止库所含有托肯，也就是cif为n的终止配置，则记录
于本发明的一实施例中，所述数据流正确性的判定方法，包括：所述wft网n需要满足的数据需求为集合λ＝(λ1,…,λm)，其中λj为一阶线性时序逻辑公式；所述wft网n的执行路径包括ρ1,…,ρn，对每个ρi:
另外，本发明还提供一种终端，包括处理器及存储器，所述存储器用于存储程序指令，所述处理器用于执行所述存储器存储的程序，以使所述终端执行如上所述业务流程设计缺陷的检测方法中的步骤。
以及，本发明还提供一种可读存储介质，所述可读存储介质存储有计算机程序，其特征在于，所述计算机程序被处理器执行时实现如上所述业务流程设计缺陷的检测方法中的步骤。
如上所述，本发明的一种业务流程设计缺陷的检测方法、可读存储介质及终端，具有以下有益效果：
通过对待测系统构建带数据表操作的工作流网模型，即wft网，可实现系统业务流程中的流程数据与底层数据库进行交互操作，以及基于数据库延伸定义业务活动受到的数据约束；并且，基于利用精炼技术构建所述系统新的发生规则并生成新的带有数据状态的配置图，实现了用工作流网标识和相关的数据及数据表的状态来刻画不同精炼值下的数据在所述工作流网中运行时的状态；同时，将系统需要满足的数据需求表达成一阶线性时序逻辑公式，构建了系统的合理性判定方法，实现了从业务流程的控制流和数据流两方面对系统流程合理性的判定，能够较详细地对系统业务流程的设计错误类别进行归类和检测，将本发明实施例应用在复杂的系统中，减少错误检查的人工成本和时间成本。
附图说明
图1显示为本发明提供的业务流程设计缺陷的检测方法于一实施例中的主要思想示意图。
图2显示为本发明提供的业务流程设计缺陷的检测方法于一实施例中的流程示意图。
图3显示为本发明实施例车辆出入证申请工作流系统图。
图4显示为本发明实施例车辆出入证申请系统的wft网模型图。
图5显示为本发明实施例车辆出入证申请系统的wft网可达配置图。
元件标号说明
s201～s205步骤
具体实施方式
以下通过特定的具体实例说明本发明的实施方式，本领域技术人员可由本说明书所揭露的内容轻易地了解本发明的其他优点与功效。本发明还可以通过另外不同的具体实施方式加以实施或应用，本说明书中的各项细节也可以基于不同观点与应用，在没有背离本发明的精神下进行各种修饰或改变。需说明的是，在不冲突的情况下，以下实施例及实施例中的特征可以相互组合。
需要说明的是，以下实施例中所提供的图示仅以示意方式说明本发明的基本构想，遂图式中仅显示与本发明中有关的组件而非按照实际实施时的组件数目、形状及尺寸绘制，其实际实施时各组件的型态、数量及比例可为一种随意的改变，且其组件布局型态也可能更为复杂。
本发明提供的所述业务流程设计缺陷的检测方法，通过对待测系统进行工作流网建模及对所述工作流网合理性分析，并且基于系统的流程数据和持久层数据将业务流程运行过程中业务活动执行受到的数据约束条件考虑到系统模型中以及对所述系统模型的合理性定义中，从而对系统中业务活动的运行和数据的特征属性进行刻画和分析，以此来判断所述待测系统的业务流程是否存在设计错误。
参阅图1，为所述业务流程设计缺陷的检测方法主要思想，包括：将所述待测系统和所述待测系统的业务数据的功能需求采用形式化方法作构建为wfd网模型，在所述待测系统的wfd网模型基础上增加了流程数据与数据库的交互访问操作，并基于数据库延伸定义所述wfd网模型中的业务活动受到的数据约束；将得到的业务逻辑层、流程数据层、持久数据层以及数据约束进行融合后得到wft网模型；基于所述wft网模型生成可达配置图，将所述待测系统需要满足的业务数据的功能需求转化成对应的一阶线性时序逻辑公式，分别从控制层和数据层构建合理性分析方法，基于所述合理性分析方法对所述待测系统级进行合理性判定，得到系统是否正确的判断结果。
本发明提供的所述业务流程设计缺陷的检测方法，通过在设计阶段检测系统是否存在控制层和/或数据层的漏洞，从而保证检测后的系统能同时满足逻辑正确和数据正确性的要求。例如，在设计阶段检测系统的输入数据是否缺少数据数值的验证环节，如是则会导致系统数据无法满足要求。
请参阅图2，本发明提供一种检测业务流程设计缺陷的方法的流程示意图，包括如下步骤：
s201，根据所述待测系统的业务流程，获取业务逻辑、流程数据及所述业务逻辑与流程数据分别对业务活动的控制约束，构建与所述待测系统对应的wfd网模型。
需要说明的是，所述待测系统为需要进行检测的系统；所述待测系统中的流程数据包含了数据约束。以待检测的报销系统为例，对于报销流程中的审批环节，只有部分员工才具有审批权限，因此，在此流程中具有审批权的人员总数就是一种数据约束。
根据现有的系统模型构建方法，建立所述待测系统的数据工作流网，即wfd网，用于反映所述待测系统中业务流程的流向。
具体的，所述系统模型构建方法包括petri网。需要说明的是，一个petri网o＝(p,t,f)由三种元素构成：一个有限的库所集合p，一个有限的变迁集合t(
如果对一个变迁t∈t，在标识m下t的每个前集库所都至少含有一个托肯，即m≥·t，则称t在标识m可以使能，表示为m[t＞。变迁t发生之后将生成了一个新的标识m′，则有m′＝m-·t t·，这一过程可以被表示为m[t>m′。若标识m在经过一个变迁序列发生后生成了新的标识m″，则这一过程可以被表示为m[*>m″，我们称m″由m可达，表示为m″∈r(m)。
在数学中，一个集合a的幂集2a由a的所有子集构成。例如，如果a＝{a,b}，那么集合
令π是一个谓词集合，其中的每一个谓词都代表一个表示数据约束的命题，取值是布尔类型，即true或者false。π中的谓词与关系联接词(即∧(“与”)、∨(“或”)、
于本实施中，基于所述petri网技术构建所述数据工作流网，即wfd网。所述wfd网为一个8元组的数据工作流网
s202，根据所述待测系统中的流程数据与数据库间的数据交互，在已有的所述wfd网的基础上构建所述待测系统的wft网模型。
其中，所述数据库为关系数据库，即采用关系数据库对所述流程数据进行存储，形成所述待测系统的数据库。
所述关系数据库采用数据模式和数据表进行表达，以方便所述关系数据库的形式化表达。所述数据模式采用一3元组表示，即：
r＝(u,v,dom)
其中，r表示一个数据模式，u是一个有限的属性集合，且存在一个唯一的特殊属性i∈u称为标识属性；v表示u中属性的值域集合；dom:u→v为属性到值域的映射。
令r′＝(u′,v′,dom′)是所述数据模式的一个实例，其中u′＝{u1,…,ul}，v′＝{v1,…,vn}，u1表示所述属性集合中的的单个标识属性，所述v1表示所述值域中的单个属性值。属性u1，…，ul的值域构成的笛卡尔积的一个元素为一个元组，表示为r。r[ui]表示元组r中属性ui的值。
因此，数据模式这样的一个实例可以视为一个行和列分别对应元组和属性的二维表，可以表示为r′(u1,…,ul)，其中u1为标识属性，表r′中的任意两个元组的标识属性u1对应的值都不能相等。所述关系数据库通过形式化方法可以转化成有限的数据表。对所述数据表的数据操作类型有四种，分别为：检索、插入、更新和删除。
基于所述wfd网构建与所述数据库交互的工作流网模型，即构建所述wft网，为一个8元组的带数据表操作的工作流网
其中，(p,t,f)是一个petri网；
s203，根据生成的所述wft网的结构特征，以及所述数据库对所述流程数据的数据约束，利用数据精炼技术对流程数据赋值。
其中，所述数据精炼技术为一种形式化方法，可以将处于被定义状态但不赋予具体值的抽象数据用与之行为对应的具体数据值来替代。
具体的，采用所述数据精炼技术对所述流程数据赋值包括：
(21)对所述wft网n中流程数据d，其值域为bd，d在状态e下的赋值集合为vd(初始化为空)，计算所述数据库中与d相关的数据表的集合
(22)若
(23)若
(231)若
(232)若πd不为空，对πd中的每个谓词πi，继续以下(2321～2322)步骤；
(2321)若vd中的所有元素都不能使得πi为真，则从bd中选择一个能使得πi为真的元素di，然后将di添加到vd；
(2322)若vd中的所有元素都不能使得πi为假，则从bd中选择一个能使得πi为假的元素di′，然后将di′添加到vd；
(24)输出vd。
由于wft网为概念模型，与wfd网模型类似，其流程数据元素依然是高度抽象的，所述流程数据元素只分为定义的和未定义的两种，无法捕捉数据元素的具体值；但是wft网的运行路径是根据数据元素的值而决定的，因此，本发明采用数据精炼技术对所述流程数据元素进行赋值，从而实现对所述流程数据元素的数值的进一步细化。
进一步的，为适配所述待测系统业务流程所有的运行的情况，根据当前数据库的实时状态以及与该数据元素相关的谓词来对所述流程数据元素进行赋值。
在具体实现时，所述流程数据元素的赋值必须基于所述数据库在当前状态下是否存储有数据，以及要保证每个与之相关的谓词都可以赋值为真或假。
s204，利用所述数据精炼技术，将所述活动的使能条件和发生规则转换为所述wft网的执行语义，生成可达配置图；所述可达配置图覆盖wft网所有可能的运行状态。
具体的，所述可达配置图的生成方法，包括：
(31)对所述工作流网n，将给定起始配置c0，将c0作为可达配置图的根节点，并标记为新；
(32)对除所述根节点以外是否存在标记为“新”的其他节点进行检测，根据检测结果执行第一生成操作，即步骤(321～322)；
所述第一生成操作包括：
(321)若存在其他标记为“新”的节点，任意选择一个“新”的节点，记为配置c，并在所述配置c下根据变迁的状态执行第二生成操作，即步骤(3211～3212)；
(322)若不存在，则生成结束，输出所述工作流网n的可达配置图rg(n)；
所述第二操作包括：
(3211)若在配置c下，不存在任何变迁有发生权，则将c标记为“终止”节点，并返回步骤(32)；
(3212)若在配置c下，变迁t1,…,tn(n≥1)有发生权，对每个变迁ti(1≤i≤n)进行第三生成操作，即步骤(3212a～3212b)；
所述第三生成操作包括：
(3212a)根据发生规则计算发生ti后生成的新配置c1,…,cs(s≥1)，对每个新配置ci(1≤i≤s)，判断ti未发生前的配置图中是否已经存在该ci；
若存在，那么将原本指向ci的箭头指向这个与ci相同的配置；
若不存在，那么将ci记录到配置图中，且生成一个箭头从c指向ci，在箭头上添加标签t，并将ci标记为“新”；
(3212b)去掉配置c的“新”标记，返回步骤(32)。
于本实施例中，对于所述工作流网n，令c＝(m,θ,ω,σ)为所述工作流网n的一个配置，即所述工作流网n的一个状态。其中，m是所述工作流网n的一个标识，代表所述工作流网n的库所中托肯的分布；θ:
构建所述工作流网n的变迁使能条件和发生规则。其中，所述变迁使能条件，即：
对于一个配置c和当前的变迁t∈t，t在c下有发生权当且仅当以下条件：
(1)c中的标识m满足m[t＞；
(2)每个被t读的数据元素、每个与t相关的数据表都必须被定义；
(3)t上的守卫函数的值为真。变迁t被触发后将产生新的配置。
其中，所述新配置的产生规则，即：对于配置c＝(m,θ,ω,σ)和当前的变迁t∈t，如果t被触发且产生了一个配置集合c′，那么新的c′依据以下产生规则生成：
(1)m的变化：m[t＞m′，即配置中的标识由m转变为新的标识m′；
(2)流程数据元素d的值的变化，即由θ(d)转变为θ′(d)，包括：
(2a)如果d被t删除，则θ′(d)＝⊥；
(2b)如果d被t写，则d将被赋予一个精炼值，即
(2c)如果d最多只被t读，则θ′(d)＝θ(d)。
(3)数据表的状态ω(r′)的变化，包括：
(3a)如果t仅在r′中检索数据，则ω′(r′)＝ω(r′)；
(3b)如果t往r′中插入元组，那么令这些元组构成的集合表示为ins(r′)，则ω′(r′)＝ω(r′)∪ins(r′)；；
(3c)如果t将r′中部分元组删除，那么令被删除的元组构成的集合表示为del(r′)，则ω′(r′)＝ω(r′)\del(r′)；
(3d)如果t对r′中的部分元组进行了更改，且将更改前与更改后的这些元组构成的集合分别表示为upd(r′)和upd(r′)′，则ω′(r′)＝ω(r′)\upd(r′)∪upd(r′)′。
(4)谓词的值σ′(π)的变化，包括：
(4a)如果与π相关的某个数据元素被t删除后并未再写，则σ′(π)＝⊥；
(4b)如果与π相关的每个数据元素和数据表在t发生后都被定义，则σ′(π)＝true或者fasle；
(4c)如果每个与π相关的数据元素最多只被t读，且每个与π相关的数据表最多只被t检索，则σ′(π)＝σ(π)。
令c和c′是所述工作流网n的两个配置，c和c′是所述工作流网n的两个配置集合，设置所述工作流网n的可达性如下：
如果当且仅当存在一个t∈t，使得c[t>c，则称从c到c存在一个“必然-步”，用c→mustc表示；
如果c→mustc且c′∈c，则称从c到c′存在一个“可能-步”，用c→mayc′表示；
如果存在一个配置序列为c0,c1,…,cn使得ci→mayci 1，其中0≤i<n，c0＝c，cn＝c′，则称从c到c′存在一条“可能-路径”，即从c到c′是可能可达的，用
如果c0＝{c}，cn＝c，且
因此，利用所述数据精炼方法，通过设定变迁使能条件和发生规则，生成wft网的可达配置图，可以描述不同的流程数据的值在工作流网运行时的状态。
s205，根据生成的所述wft网，采用线性时序逻辑方法构建所述wft网的合理性分析方法，并对所述wft网进行合理性判定，获取合理性判定结果。
其中，所述合理性分析包括对所述wft网的控制流和数据流的合理性分析；所诉合理性判定结果包括控制流和数据流的合理性判定结果，从而检测系统在业务流程中的设计缺陷。
进一步的，所述业务流程设计缺陷包括针对系统业务流程规定需要满足的数据需求，在基于数据精炼考虑所生成的wft网模型所有可能运行路径的情况下，如果存在某些路径，到达不了最终状态或者不满足所有的数据需求，则说明系统业务流程的设计存在缺陷。
进一步的，将所述系统业务数据的功能需求转换为一阶线性时序逻辑公式，并从控制流和数据流两个方面定义所述wft网的合理性。
需要说明的是，一阶线性时序逻辑公式，即ltl-fo公式，是基于线性时序逻辑公式(即ltl公式)的扩展，通过将基于数据库表上的无量词一阶语句添加到ltl公式得到ltl-fo公式。对于所述工作流网n，一个基于数据库
于本实施例中，对于所述工作流网n，rg(n)为可达配置图，其中c0是给定的初始配置，cf是n的所有终止配置的一个集合，
(1)n在控制层是合理的，当且仅当：
(a)
(b)
(c)
(2)n在数据层是合理的，当且仅当n满足的数据需求，即
于本实施例中，所述控制流合理性的判定方法，包括：
(41)在一个wft网n的可达配置图rg(n)中，称连接根节点c0到某个终止节点cf的一条配置序列为n的一条执行路径，记为ρ:c0c1…cf，且将路径ρ中所有触发变迁构成的集合记为tρ，令t为n的变迁集合；
(42)在默认循环只执行一次的情况下，基于rg(n)计算n所有可能的执行路径，依次记为ρ1,…,ρn，其中ρi:ci0ci1…cif(1≤i≤n)，对每个ρi中的终止节点cif进行判断；
(421)若配置cif中的标识为有且仅有n中的终止库所含有托肯，也就是cif为n的终止配置，则记录
(422)若配置cif中的标识为含有n中的非终止库所含有托肯，也就是cif不是n的终止配置，跳到步骤(44)；
(43)计算所有
(431)若两者相等，则执行步骤(45)；
(432)若两者不等，则执行步骤(44)；
(44)判定n的控制流是不合理的；
(45)判定n的控制流是合理的。
于本实施例中，所述数据流合理性的判定方法包括：
(51)wft网n需要满足的数据需求为集合λ＝(λ1,…,λm)，其中λj为一阶时序逻辑公式，wft网n的执行路径包括ρ1,…,ρn，对每个ρi:
(52)初始化与λj关联的流程数据元素构成的集合
其中，所述第一判定操作包括步骤(521～523)，即：
(521)λj:
(522)若k≥1，按照步骤(5221～5224)验证n在
(5221)若
(5222)若
(5223)若
(5224)若
(523)令k＝k-1，继续执行所述第一判定操作直至k<1；
(53)输出结果：n满足数据需求λ＝(λ1,…,λm)；即n的数据流合理；
(54)输出结果：n不满足数据需求λ＝(λ1,…,λm)，即n的数据流不合理。
根据以上的判定算法，若wft网n的控制流和数据流都是合理的，那么这个网对应的系统是完全合理的，系统业务流程的设计没有流程和数据上的错误。
示例性的，请参阅图3，为本发明中采用形式化方法描述了一个企业单位车辆出入证的申请流程。用户必须先在系统成功注册，才能申请办理车辆出入证。另外，用户登录系统后根据当前是否已经注册过车辆出入证与否的信息被引导进行注册或者修改相关信息。在初步注册信息审核通过后需要用户进一步提交文件资料，若提交的文件正确，则最终申请成功，否则需要重新提交。
请参阅图4，为根据本发明提供的所述业务流程设计缺陷的检测方法，以出入证申请系统作为待测系统，构建所述出入证申请系统的wft网。如图4所示，图中包括所述wft网模型的基本业务逻辑、数据元素操作、数据表操作以及活动上的守卫函数，包括：初始库所“开始”，终止库所“结束”，库所p1～p9；变迁t1～t17；数据元素集
请参阅图5，为基于本发明生成的所述出入证申请系统wft网对应的可达配置图，可达配置图中的每一个配置节点表示系统运行到某一时刻的状态。箭头表示状态间通过某个变迁t进行转换。例如，给定初始配置c0＝([start],{θ(id)＝⊥,θ(lpn)＝⊥,θ(pht)＝⊥},{user＝{(id1,lpn1),(id2,null)}},{σ(π1)＝⊥,σ(π2)＝⊥,σ(π3)＝⊥,σ(π4)＝⊥})。为了便于表达，简化为c0＝([start],{⊥,⊥,⊥},{(id1,lpn1),(id2,null)},{⊥,⊥,⊥,⊥})，表示初始时，任何数据都未被写入，数据表含有两个元组(id1,lpn1)和(id2,null)，谓词也处于未定义状态。运行到某一时刻，例如c8＝([p5],{id3,⊥,⊥},{(id1,lpn1),(id2,null),(id3,null)},{false,true,⊥,⊥})，表示此刻，数据元素id的精炼值id3作为标识属性的值被写入系统数据库表<用户>，且由于谓词π1和π2与数据元素id相关，因此谓词π1和π2的值是可判断真与假的。c7，c10，c12，c33，c35，c36，c38，c48，c50为所述出入证申请系统wft网的终止配置，即在这些配置状态下没有活动可以发生，对应路径的流程运行结束。
该系统规定，每个车牌号最多只能被一个用户注册并使用，用一阶线性时序逻辑公式可表达成：
于本实施例中，基于所述出入证申请系统wft网生成的可达配置图上，对于从初始配置到每个终止配置的每条可达路径，根据终止配置中库所托肯的当前分布，由此判断控制流是否合理，即如果存在某一路径，基于系统的业务流程无法到达该路径对应的终止配置状态时，则所述控制流不合理；并且，检测所述每条可达路径中的每个配置节点是否满足如上所述一阶线性时序逻辑公式，由此判断数据流是否合理。
根据所述合理性分析方法对所述出入证申请系统wft的控制流合理性和数据合理性进行分析，得到如下结论：
首先，根据控制流能否完全终止的判定，我们可以得到
1)
2)所有终止配置的库所有且仅有终止库所含有标识；
3)可达图中除终止配置外的节点最终都能到达终止状态。
因此，可以判定该系统的控制流是合理的。
其次，对数据流进行判断，在给定的初始配置下，如果用户可以执行到变迁t9并输入一个已经存在于当前数据库中的车牌号信息并完成资料提交审核，那么一定会出现违背数据需求的运行结果发生。例如，在所述出入证申请系统wft网的可达图中，从初始配置c0到终止配置c48的可达路径用c0c1c4c8c13c19c26c31c37c40c43c46c48表示；当用户id3(图中未标识)先尝试注册车牌号lpn2，由于当前数据库中并没有其他用户注册使用lpn2，所以用户id3可以成功注册lpn2，此时数据库的状态为user＝{(id1,lpn1),(id2,null),(id3,lpn2)}，在通过资料审核以后，用户id3并没有退出该系统，而是选择继续修改车牌号信息，并将原来的车牌号信息lpn2更改为lpn1，此时数据库的状态为user＝{(id1,lpn1),(id2,null),(id3,lpn1)}，过后用户id3成功完成资料审核并退出该系统。这种运行情况出现了车牌号lpn1被两个不同的用户同时注册并使用，显然不满足系统规定的数据需求。因此，由判定结果可知，所述系统的数据流设计是不合理的。
综上所述，该系统是不合理的，其业务流程设计存在缺陷，活动“修改车牌号”缺少对输入的车牌号到数据库中进行唯一性核查的环节。
应用本发明实施例产生的有益效果如下：
(1)可以判定该系统的业务流程设计并不满足规定的数据需求，即在运行过程中某些数据出现异常时系统没有进行识别和处理，该系统是存在数据错误的。
(2)提出了系统业务流程正确性的分析模型，即带数据表操作的工作流网(wft网)，能够捕捉流程数据的具体值，以实现更加详细的描述数据问题。
(3)采用数据精炼技术，构建了相应的可达配置图，为正确性的分析提供了方法基础。
(4)提出了从控制流和数据流两个角度综合定义的合理性作为分析系统业务流程正确性的判定性质依据。能够较详细的对系统业务流程的设计错误类别进行归类和检测，将本发明实施例应用在复杂的系统中，减少错误检查的人工成本和时间成本。
上述实施例仅例示性说明本发明的原理及其功效，而非用于限制本发明。任何熟悉此技术的人士皆可在不违背本发明的精神及范畴下，对上述实施例进行修饰或改变。因此，举凡所属技术领域中具有通常知识者在未脱离本发明所揭示的精神与技术思想下所完成的一切等效修饰或改变，仍应由本发明的权利要求所涵盖。
1.一种业务流程设计缺陷的检测方法，其特征在于，所述业务流程设计缺陷的检验方法包括以下步骤：
根据待测系统的业务流程，以及业务逻辑、流程数据及所述流程数据对业务活动的控制约束，构建成所述待测系统的wfd网；
根据所述流程数据与数据库间的交互，在所述wfd网基础上构建所述待测系统的wft网；
根据所述wft网的结构特征，以及所述数据库对所述流程数据的数据约束，利用数据精炼方法对所述待测系统的流程数据赋以具体值；
根据数据精炼技术，将所述业务活动的使能条件和发生规则转换为所述wft网的执行语义，生成可达配置图；
根据所述wft网，采用线性时序逻辑方法构建所述wft网的合理性分析方法，判定所述wft网的合理性，获得所述待测系统的合理性判定结果。
2.根据权利要求1所述的业务流程设计缺陷的检测方法，其特征在于，所述采用线性时序逻辑方法构建所述wft网的合理性分析方法包括采用一阶线性时序逻辑的方法分别从控制流和数据流构建所述wft网的合理性分析方法。
3.根据权利要求2所述的业务流程设计缺陷的检测方法，其特征在于，所述构建待测系统的wft网的方法包括：
构建8元组的工作流网
其中，(p,t,f)为petri网；
g:
4.根据权利要求3所述的业务流程设计缺陷的检测方法，其特征在于，所述流程数据的赋值精炼，包括：
对所述wft网n中的流程数据d，其值域为bd，d在状态c下的赋值集合为vd，计算所述数据库中与d相关的数据表的集合
若
若
若πd不为空且
若vd中的所有元素都不能使得πi为真，则从bd中选择一个能使得πi为真的元素di，然后将di添加到vd；
若vd中的所有元素都不能使得πi为假，则从bd中选择一个能使得πi为假的元素d′i，然后将d′i添加到vd；
否则输出vd。
5.根据权利要求3所述的业务流程设计缺陷的检测方法，其特征在于，所述wft网的所述可达配置图的生成，包括：
对所述wft网n，给定起始配置c0，将c0作为可达配置图的根节点，并标记为新；
对除所述根节点以外是否存在标记为“新”的其他节点进行检测，根据检测结果执行第一生成操作；
其中，所述第一生成操作包括：
若其他节点中均不包含标记为“新”的节点，则所述可达配置图生成结束，输出n的可达配置图rg(n)；
若存在标记为“新”的节点，任意选择一个“新”的节点，记为配置c，并在所述配置c下根据变迁的状态执行第二生成操作；
其中，所述第二生成操作包括：
若在配置c下，不存在任何变迁有发生权，则将c标记为“终止”节点，并继续对除所述根节点以外的其他节点进行检测，以及根据检测结果执行所述第一生成操作；
若在配置c下，变迁t1,…,tn(n≥1)有发生权，对每个变迁ti(1≤i≤n)进行第三生成操作；
其中，所述第三生成操作包括：
根据发生规则计算发生ti后生成的新配置c1,…,cm(m≥1)，对每个新配置ci(1≤i≤m)，判断ti未发生前的配置图中是否已经存在该ci；
若存在，那么将原本指向ci的箭头指向这个与ci相同的配置；
若不存在，那么将ci记录到配置图中，且生成一个箭头从c指向ci，在箭头上添加标签t，并将ci标记为“新”；
去掉配置c的“新”标记，并继续对除所述根节点以外的其他节点进行检测，以及根据检测结果执行所述第一生成操作。
6.根据权利要求5所述的业务流程设计缺陷的检测方法，其特征在于，所述控制流合理性分析方法，包括：
在所述wft网n的可达配置图rg(n)中，将连接所述根节点c0到单个所述终止节点cf的一条配置序列为n的一条执行路径，记为ρ:c0c1…cf，且将路径ρ中所有触发变迁构成的集合记为tρ，令t为n的变迁集合；
在默认循环只执行一次的情况下，基于rg(n)计算n所有可能的执行路径，依次记为ρ1,…,ρn，其中ρi:ci0ci1…cif(1≤i≤n)，对每个ρi中的终止节点cif进行判断，包括：
若配置cif中的标识为含有n中的非终止库所含有托肯，也就是cif不是n的终止配置，则设定n的控制流为不合理；
若配置cif中的标识为有且仅有n中的终止库所含有托肯，也就是cif为n的终止配置，则记录
若两者相等，则设定n的控制流为合理；
若两者不等，则设定n的控制流为不合理。
7.根据权利要求5所述的业务流程设计缺陷的检测方法，其特征在于，所述数据流的合理性分析方法，包括：
所述wft网n需要满足的数据需求为集合λ＝(λ1,…,λm)，其中λj为一阶线性时序逻辑公式；所述wft网n的执行路径包括ρ1,…,ρn，对每个ρi:
初始化与λj关联的流程数据元素构成的集合
其中，所述第一判定操作包括：
λj:
若k≥1，则根据
若
若
若
若
令k＝k-1，继续执行所述第一判定操作，直至k<1。
8.一种终端，包括处理器及存储器，所述存储器用于存储程序指令，所述处理器用于执行所述存储器存储的程序，以使所述终端执行如权利要求1至7中任一项所述业务流程设计缺陷的检测方法中的步骤。
9.一种可读存储介质，所述可读存储介质存储有计算机程序，其特征在于，所述计算机程序被处理器执行时实现如权利要求1至7中任一项所述业务流程设计缺陷的检测方法中的步骤。
技术总结