一种基于MSVL的Petri网模型检测方法

摘要

本发明公开了一种基于MSVL的Petri网模型检测方法，首先利用现有的建模工具Workcraft建立Petri网系统模型，然后将该模型转换成等价的MSVL程序，为此本发明给出了分别由Petri网系统的顺序语意、并行语意和最大并行语意指导的三种转换方法；最后使用现有的MSVL支持工具MSV对生成的MSVL程序进行仿真、建模和验证。针对上述转换方法，本发明开发了转换工具PN3MSVL和PN4MSVL，使得工具MSV能够对Petri网系统的各种语意进行分析和验证。本发明解决了现有的Petri网模型检测方法难以充分验证各种语意的完全正则性质的问题。

说明书

技术领域

本发明属于Petri网的模型检测技术领域，尤其涉及一种基于MSVL的Petri 网模型检测方法。

背景技术

作为图形化和形式化的工具，Petri网被广泛的应用于建模和分析离散事件 系统。Petri网的图形能够将复杂的需求直观地表达出来，而模糊的文本描述或 者晦涩的数学符号则不能。除此之外，利用Petri网的数学理论能够对系统模型 的一些性质(例如可达性、安全性和活性)进行形式化分析。现有的Petri网分 析方法包括覆盖树方法、网化简方法和网展开方法等。除此之外，针对Petri 网现已提出多种模型检测方法，例如偏序模型检测、符号模型检测和限界模型 检测。这些方法可以验证用线性时序逻辑(LTL)和计算树逻辑(CTL)描述 的性质。虽然这两个逻辑能描述很广泛的性质，但是仍然难以满足实际应用的 需要。这是因为它们的描述能力都不是完全正则的。Petri网有顺序语意、并行 语意和最大并行语意等多种语意，然而现有的模型检测方法通常只验证顺序语 意的性质。因此，目前难以充分验证Petri网各种语意的完全正则性质。

投影时序逻辑(PTL)是区间时序逻辑(ITL)的扩展，可以用于描述和验 证并发系统。命题投影时序逻辑(PPTL)不仅具有完全正则表达能力，而且擅 长描述顺序和迭代行为。建模、仿真和验证语言(MSVL)是PTL的可执行子 集，不仅包含顺序语句、条件语句和循环语句，还具备并行语句和等待语句。 作为形式化程序设计语言，MSVL不但可以像一般的命令式程序设计语言一样 执行，而且可以像Promela语言一样建模并行系统，还可以利用统一模型检测 方法对PPTL描述的系统性质进行验证。除此之外，目前MSVL的支持工具 MSV已经实现，可以对MSVL程序进行仿真、建模和验证。

发明内容

本发明的目的在于提供一种基于MSVL的Petri网模型检测方法，旨在解 决现有的Petri网模型检测方法难以充分验证各种语意的完全正则性质的问题。

本发明的目的在于提供一种基于MSVL的Petri网模型检测方法，该基于 MSVL的Petri网模型检测方法首先利用现有的建模工具Workcraft建立Petri 网系统模型，然后使用转换工具PN3MSVL和PN4MSVL将Petri网系统转换成 顺序等价、并行等价或最大并行等价的MSVL程序；最后利用现有的MSVL 支持工具MSV对生成的MSVL程序进行仿真、建模和验证。

进一步，该基于MSVL的Petri网模型检测方法包括以下步骤：

步骤一：利用建模工具Workcraft建立Petri网系统模型；

步骤二：利用转换工具PN3MSVL和PN4MSVL将Petri网系统转换成顺序 等价、并行等价或最大并行等价的MSVL程序；

步骤三：利用MSVL支持工具MSV对生成的MSVL程序进行仿真、建模 和验证。

进一步，Workcraft、PN3MSVL、PN4MSVL和MSV已经集成到工具集 MSVToolkit中。

进一步，步骤二中PN3MSVL实现了顺序语意指导的转换；首先通过解析 g文件来构造Petri网系统Z＝(P,T,W,M₀)，g文件由Workcraft建模生成；然后 将Z转换为顺序等价的MSVL程序并将显示在MSVToolkit的文本框内：

其中对每个变迁t∈T，g_t≡∧_q∈Pv_q≥w_qt和对每个库 所q∈P，m_q＝M₀(q)是自然数；对每个库所w_qt＝W(q,t)和w_tq＝W(t,q)都是 自然数；另外，g_T≡∨_t∈Tg_t。

进一步，步骤二中PN4MSVL实现了并行语意指导的转换和最大并行语意 指导的转换；首先通过解析g文件来构造安全的Petri网系统Z＝(P,T,W,M₀)，g 文件由Workcraft建模生成；然后将Z转换为并行等价的MSVL程序或最大 并行等价的MSVL程序并将程序显示在MSVToolkit的文本框内：

其中g_T的定义与MSVL程序中的相同，

进一步，步骤三中利用工具MSV分别对和进行仿真、建模和验 证。

进一步，利用MSV分别仿真执行和从而得到Z的一个最小步 字、步字和最大步字。

进一步，利用MSV分别构造和的范式图，从而得到Z在顺序语 意、并行语意和最大并行语意下的状态空间。

进一步，利用MSV分别验证和是否满足PPTL公式描述的完全 正则性质，从而判断Z的顺序语意、并行语意和最大并行语意是否满足该性质。

本发明实现了转换工具PN3MSVL和PN4MSVL，并将它们集成到工具集 MSVToolkit。PN3MSVL包含三个模块：Petri网系统获取模块、顺序语意指导 的转换模块和MSVL程序输出模块；PN4MSVL包含四个模块：Petri网系统获 取模块、并行语意指导的转换模块、最大并行语意指导的转换模块和MSVL程 序输出模块。利用PN3MSVL和PN4MSVL可以将Petri网系统转换为顺序等价 的MSVL程序、并行等价的MSVL程序和最大并行等价的MSVL程序。通过 MSV对生成的MSVL程序进行仿真、建模和验证，从而实现对Petri网各种语 意的分析和验证。因此，本发明解决了现有的Petri网模型检测方法难以充分验 证各种语意的完全正则性质的问题。

附图说明

图1是本发明实施例提供的基于MSVL的Petri网模型检测方法流程图；

图2是本发明实施例提供的工具集MSVLToolkit的用户界面。MSVLToolkit 不但集成了转换工具PN3MSVL和PN4MSVL，还包含Petri网系统的现有建模 工具Workcraft和MSVL的现有支持工具MSV。该图下部是利用PN3MSVL转 换实施例中的Petri网系统Z生成的MSVL程序

图3是本发明实施例提供的安全的Petri网系统Z；

图4是本发明实施例提供的利用工具PN4MSVL转换网系统Z生成的MSVL 程序

图5是本发明实施例提供的利用工具PN4MSVL转换网系统Z生成的MSVL 程序

图6是本发明实施例提供的利用工具MSV对程序的仿真结果；

图7是本发明实施例提供的利用工具MSV对程序和的仿真结果；

图8是本发明实施例提供的利用工具MSV对程序的建模结果；

图9是本发明实施例提供的利用工具MSV对程序的建模结果；

图10是本发明实施例提供的利用工具MSV对程序的建模结果；

图11是本发明实施例提供的利用工具MSV对程序验证性质时输出的反 例路径；

图12是本发明实施例提供的利用工具MSV对程序验证性质时输出的反 例路径。

具体实施方式

下面结合附图及具体实施例对本发明的应用原理作进一步描述。

现有工具MSV中的MSVL统一模型检测方法可以验证MSVL程序是否满 足PPTL公式描述的完全正则性质。基于MSVL的Petri网模型检测方法为了利 用工具MSV来验证Petri网的完全正则性质，需要将Petri网转换成等价的 MSVL程序。

Petri网是三元组N＝(P,T,W)，其中P和T是两个有限非空且不相交的集合， 分别称作库所集合和变迁集合；W:(P×T)∪(T×P)→N₀是库所和变迁之间有权值 的流关系，N₀表示自然数集合；Petri网的图形表示中库所和变迁分别使用正方 形节点和圆形节点表示，流关系则用节点之间的有向边表示；由节点x指向y的 边上标注的数字是边的权值W(x,y)；边的权值为1，则省略标注；对x∈P∪T， 是x的前置集，表示x的后置集，是 x的因果集；

Petri网N＝(P,T,W)的标识M为P的多重集；M(p)＞0，则称在标识M下库 所p是标识的，或p有M(p)个托肯，图形表示中库所p包含M(p)个黑点；M(p)≥W(p,t)，则称在标识M下变迁t是使能的，记为M[t＞；M[t＞，则变迁t 可以执行并产生标识M'，记为M[t＞M'，其中M'(p)＝M(p)+W(t,p)-W(p,t)；在标识M下没有使能的变迁，则称M是死的；步 U是T的多重集；则称在标识M下步U是使能的， 记为M[U＞；M[U＞，则步U可以执行并产生标识M'，记为M[U＞M'，其中 $\forall p\in P,M^{\prime }\left(p\right)=M\left(p\right)+\underset{t\stackrel{·}{\in }\stackrel{·}{p}}{\Sigma }U\left(t\right)·(W(t,p)-W(p,t));$M[U＞且|U|＝1，则称在标识M下 步U是最小步；M[U＞并且不存在步U'满足和M[U′＞，则称在标识M下 步U是最大步；

Petri网系统是四元组Z＝(P,T,F,M₀)，其中(P,T,F)是Petri网，M₀是Petri 网系统的初始标识；存在标识M₁,M₂,...,M_n满足M₀[U₁＞M₁[U₂＞...M_n-1[U_n＞M_n，则 称λ＝U₁U₂...U_n是步序列；最小步序列或最大步序列是只含最小步或最大步的步 序列；M₀[λ＞M表示从标识M₀开始执行步序列λ并最终到达标识M；存在步序 列λ满足M₀[λ＞M，则称标识M是可达的；每个可达标识在每个库所中放置最 多k个托肯，则称网系统是k有界的(k-bounded)；若k＝1，则称网系统是安 全的。

若存在步序列λ＝U₁U₂...U_n满足M₀[U₁＞M₁[U₂＞...[U_n＞M_n，而且M是死标识， 则称有限序列α＝M₀M₁...M_n是Σ的有限步字；若存在步序列λ＝U₁U₂...满足 M₀[U₁＞M₁[U₂＞...，则称无限序列α＝M₀M₁...是Σ的无限步字；以上两种情况中， 称α由λ导出；若步字α可以由最小步序列(最大步序列)导出，则称α是最小 步字(最大步字)；网系统的并行语意由所有的步字构成，顺序语意(最大并 行语意)由所有的最小步字(最大步字)构成；

建模、仿真和验证语言MSVL是投影时序逻辑PTL的可执行子集；Prop是 可数的命题集合；V是可数的变量集合；B＝{true,false}代表布尔域；D表示所 有数据，包括整数、链表和集合。

MSVL的部分算数表达式和布尔表达式：

其中n是整数，x∈V是变量，f是函数。

MSVL的部分语句：

这里x,x₁,...,x_m是变量，e是算数表达式，b,b₁,...,b_n是布尔表达式，p,q,p₁,...,p_n代表MSVL程序；

表示在当前状态变量x的值等于表达式e的值，同时与x对应的命题 p_x置为真；x:＝e表示在下一状态变量x的值等于表达式e的当前值，同时与x对 应的命题p_x置为真；顺序语句、条件语句以及循环语句和传统的命令式程序设 计语言相同；(b₁→p₁)[]...[](b_n→p_n)表示如果条件b₁,...,b_n都为假，那么程序中止， 否则任选b_i为真的p_i执行；p∧q表示程序p和q同时开始，并行执行，而且同时 结束；frame(x₁,...,x_m)表示如果没有碰到变量x_i的赋值语句，那么x_i的值保持不 变；skip表示区间上的单位时间，empty表示空操作；

集合V∪Prop上的状态s是二元组对每个变量x∈V，对其赋D中 的值，或者未定义；对每个命题p∈Prop赋真假值；区间σ＝<s₀,...,s_n>是状态序 列，该序列可以是有限的，也可以是无限的；MSVL程序的最小模型由区间表 示；对每个MSVL程序，都可以构造一个图形，即范式图(NFG)；它可以显 式地刻画MSVL程序的所有状态空间，并包含MSVL程序的所有最小模型；

命题投影时序逻辑(PPTL)具有完全正则表达能力，它的语法定义如下： 其中p∈Prop，Prop是可数原子命题集合； O、+和prj是基本时序操作符。PPTL的部分衍生公式：$O^{n}P\stackrel{\mathrm{def}}{=}O\left(O^{n-1}P\right),\mathrm{len}\left(n\right)\stackrel{\mathrm{def}}{=}{O}^nϵ$和

Petri网系统的顺序语意(并行语意、最大并行语意)满足PPTL公式，当 且仅当顺序语意(并行语意、最大并行语意)中的每个步字都满足该公式；MSVL 程序满足PPTL公式，当且仅当该程序的每个最小模型都满足该公式；Petri网 系统Z＝(P,T,W,M₀)与包含变量{v_q|q∈P}的MSVL程序是顺序等价的(并行等价 的、最大并行等价的)，当且仅当对Z的每个最小步字(步字、最大步字)M₀M₁...， 该程序有最小模型<s₀,s₁,...>，满足对于h≥0，反之亦然；

本发明一种基于MSVL的Petri网模型检测方法是这样实现的，该基于 MSVL的Petri网模型检测方法首先利用建模工具Workcraft建立Petri网系统模 型，然后将该模型转换成等价的MSVL程序，为此本发明给出了分别由Petri 网系统的顺序语意、并行语意和最大并行语意指导的三种转换方法，并将它们 实现为转换工具PN3MSVL和PN4MSVL；本发明利用MSVL现有的支持工具 MSV对所述转换工具生成的MSVL程序进行仿真、建模和验证，从而实现对 Petri网系统各种语意的分析和验证；本发明解决了现有的Petri网模型检测方法 难以充分验证各种语意的完全正则性质的问题。

如图1所示，本发明一种基于MSVL的Petri网模型检测方法包括以下步 骤：

步骤一(S101)：用建模工具Workcraft建立Petri网系统模型；

步骤二(S102)：利用转换工具PN3MSVL和PN4MSVL将给定的Petri 网系统转换成顺序等价、并行等价或最大并行等价的MSVL程序；

步骤三(S103)：利用MSVL的支持工具MSV对生成的MSVL程序进行 仿真、建模和验证；

进一步，Workcraft、PN3MSVL、PN4MSVL和MSV已经集成到工具集 MSVToolkit中；

进一步，步骤二中的PN3MSVL包含三个模块，Petri网系统获取模块、顺 序语意指导的转换模块和MSVL程序输出模块。

Petri网系统获取模块通过解析g文件来构造Petri网系统Z＝(P,T,W,M₀)。 其中，g文件由Workcraft建模生成。

顺序语意指导的转换模块将Z转换为如下所示的顺序等价的MSVL程序 并由MSVL程序输出模块将显示在MSVToolkit的文本框内：

其中对每个变迁t∈T，g_t≡∧_q∈Pv_q≥w_qt和对每个库 所q∈P，m_q＝M₀(q)是自然数；对每个库所w_qt＝W(q,t)和w_tq＝W(t,q)都是 自然数；另外，g_T≡∨_t∈Tg_t；MSVL程序中对每个库所q∈P有变量v_q，该变量 用于记录库所q中的托肯数量；变量v_q按照M₀(q)进行初始化，并置于区间框架 语句中；v_q的值在没有碰到v_q的赋值语句的时候不断地继承到下一状态；针对 每个变迁t∈T，根据其使能规则和执行规则分别构造MSVL布尔表达式g_t和 MSVL语句除此之外，引入布尔表达式g_T，在当前标识下有使能变迁，则 g_T成立，否则不成立；模拟Z的顺序语意，即每次随机选择一个使能变迁执 行，直到Z到达死标识；

进一步，步骤二中的PN4MSVL包含四个模块，安全的Petri网系统获取模 块、并行语意指导的转换模块、最大并行语意指导的转换模块和MSVL程序输 出模块。

安全的Petri网系统获取模块通过解析g文件来构造安全的Petri网系统 Z＝(P,T,W,M₀)。其中，g文件由Workcraft建模生成。

并行语意指导的转换模块将Z转换为如下所示的并行等价的MSVL程序 并由MSVL程序输出模块将显示在MSVToolkit的文本框内。

其中和另外， g_T的定义和中的一样；MSVL程序中对每个库所q∈P有变量v_q，该变量用 于记录库所q中的托肯数量；对每个变迁t∈T有变量v_t，该变量用于标记变迁t 是否在当前标识下执行；因为原模型限定为安全的网系统，所以每个变迁同时 最多执行一次；v_t的值为1则表示t在当前标识下执行，v_t的值为0则表示不执 行；所有值为1的变量v_t对应的变迁t组成当前标识下执行的使能步；布尔表达 式g₁和g₂分别确保每次随机选择的步是非空的和使能的；语句τ_P描述的是执行 一步对每个库所的影响；模拟Z的并行语意，即每次随机地选择一个使能步 执行，直到Z到达死标识；

最大并行语意指导的转换模块将Z转换为如下所示的最大并行等价的 MSVL程序并由MSVL程序输出模块将显示在MSVToolkit的文本框内。

其中g₁与g₂的定义和中的一样；模拟Z 的最大并行语意，即每次随机地选择一个最大使能步执行，直到Z到达死标识； if条件语句中增加的布尔表达式g₃确保每次随机选择的步都是当前标识下的最 大步；

进一步，步骤三利用MSV的仿真模块分别执行和从而得到Z的 一个最小步字、步字和最大步字；

利用MSV的建模模块分别生成和的范式图，从而得到Z在顺序 语意、并行语意和最大并行语意下的状态空间；

利用MSV的验证模块分别验证和是否满足PPTL公式描述的完 全正则性质，从而判断Z的顺序语意、并行语意和最大并行语意是否满足该性 质。

实施例1：

本发明实现了转换工具PN3MSVL和PN4MSVL，并将它们集成到了工具 集MSVToolkit中，如图2所示；除此之外，该MSVToolkit还包含Petri网系 统的现有建模工具Workcraft和MSVL的现有支持工具MSV；方便起见，在 PN3MSVL和PN4MSVL的实际转换中对每个库所q(变迁t)引入同名变量q(t) 而非变量v_q(v_t)；

如图3所示，其为该实施例中的Petri网系统Z；该实施例展示如何利用工 具MSV对Petri网系统的各种语意进行仿真、建模和完全正则性质的验证；

具体步骤：

步骤一：

点击MSVToolkit的按钮Workcraft调用Petri网系统的建模工具Workcraft 建立Z的模型，并将它保存到1.g文件中；

步骤二：

点击按钮Input选择1.g文件，点击按钮Output选择MSVL程序的输出路 径；

点击按钮PN3MSVL，调用转换工具PN3MSVL：首先Petri网系统获取模 块解析1.g文件构造Petri网系统Z，然后顺序语意指导的转换模块将Z转换成 顺序等价的MSVL程序最后MSVL程序输出模块将显示到MSVToolkit 的文本框，如图2下部所示；

勾选选项Safe Petri Net，点击按钮PN4MSVL调用转换工具PN4MSVL： 首先Petri网系统获取模块解析1.g文件构造安全的Petri网系统Z，然后并行语 意指导的转换模块将Z转换成并行等价的MSVL程序最后MSVL程序输 出模块将显示到MSVToolkit的文本框，如图4所示；

勾选选项Safe Petri Net和Max-step，点击按钮PN4MSVL调用转换工具 PN4MSVL：首先Petri网系统获取模块解析1.g文件构造安全的Petri网系统Z， 然后最大并行语意指导的转换模块将Z转换成最大并行等价的MSVL程序最后MSVL程序输出模块将显示到MSVToolkit的文本框，如图5所示；

步骤三：

点击按钮MSV调用MSVL的仿真、建模和验证工具MSV，将生成的MSVL 程序和分别输入到MSV中；

点击MSV的按钮Simulation调用仿真模块对MSVL程序和分别 进行仿真执行，得到Z的一个最小步字、步字和最大步字；如图6所示，程序的仿真执行得到Z的最小步字M₀M₁M₂M₃M₄，其中M₀＝{p₀}，M₁＝{p₁,p₂}， M₂＝{p₁,p₄}，M₃＝{p₃,p₄}，M₄＝{p₅}；如图7所示，程序和的仿真执行得 到Z的同一个步字(也是最大步字)M₀M₁M₃M₄；

点击MSV的按钮Modeling调用建模模块对MSVL程序和分别 进行建模生成其范式图，如图8-10所示；这些范式图分别展示Z在顺序语意、 并行语意和最大并行语意中的状态空间，分别包含Z在这些语意中所有步字；

点击MSV的按钮Verification调用验证模块验证MSVL程序和是 否满足性质(len2∧◇Q)⁺；true，其中Q定义为p₄＝1；该PPTL公式表示：存在n∈N₀使得对每个0≤m≤n，性质Q在第2*m个到第2*(m+2)中的某个状态上成立；针 对程序和工具MSV分别输出了不满足该性质的执行路径(称反例路径)， 如图11和12所示，因此和都不满足该性质；进而可知，Z的顺序语意和 并行语意都不满足该性质；工具MSV对MSVL程序验证该性质的结果是满 足，进而可知Z的最大并行语意满足该性质。

与现有技术相比，本发明具有如下优点以及显著效果：

可以利用MSVL的支持工具MSV分析Petri网系统的顺序语意、并行语 意和最大并行语意；

可以利用工具MSV验证Petri网系统顺序语意、并行语意和最大并行语 意的完全正则性质，而现有的Petri网模型检测技术难以充分验证各种语意的完 全正则性质。

以上所述仅为本发明的较佳实施例而已，并不用以限制本发明，凡在本发 明的精神和原则之内所作的任何修改、等同替换和改进等，均应包含在本发明 的保护范围之内。