基于带抑制弧的Petri网表示的嵌入式系统模型的子网化简

张 玮 夏传良

(山东建筑大学计算机科学与技术学院 山东 济南 250101)

0 引 言

嵌入式系统在无人机、物联网和医疗设备等领域都有广泛应用。对可靠性、正确性和实时性的高要求是嵌入式系统的特征[1-2]。为了保证系统的正确性和有效性，需要在嵌入式系统的设计中采用形式化的建模方法。

目前可用于描述嵌入式系统的模型主要有有限状态机、数据流图、Petri网[3]和SysML(Systems Modeling Language)。基于Petri网表示的嵌入式系统PRES+模型是一种用于嵌入式系统建模、验证和分析的比较有效的方法[4-8]。

为了设计嵌入式系统，Cortés等[4]提出了一种基于PRES+的嵌入式系统的形式化计算模型。Karlsson等[5]提出了一种PRES+与基于组件的系统级设计集成的方法。Xia等[7-8]提出了PRES+模型的细化方法和合成方法。

加入抑制弧可以增强Petri网的建模能力[9-10]。为了提高PRES+的建模和验证能力，我们在PRES+模型中加入抑制弧，得到基于带抑制弧的Petri网表示的嵌入式系统(PIRES+)模型。但是，在PIRES+建模和验证复杂的嵌入式系统过程中存在状态空间爆炸问题。

为了解决Petri网的状态空间爆炸问题，国内外学者提出了多种模型转换方法，其中化简操作是一种重要的转换方法。

Boucheneb等[11]提出了一种时间Petri网(TPN)的部分化简技术。Berthomieu等[12]给出了一种减少库所和变迁数量的方法。对于PRES+系统，Xia[6]提出了化简规则，在一定条件下，化简后得到的PRES+与原模型完全等价。

本文的主要动机是给出PIRES+保性化简规则，使得化简前后保持可达性、功能性和实时性等性质不变，不用进行可达空间分析，从而达到缓解状态空间爆炸的目的。

1 相关概念

定义1PRES+模型N=(P,T,FI,FO,M0)，其中：P={p1,p2,…,pm}是库所的有限非空集合；T={t1,t2,…,tm}是变迁的有限非空集合；FI⊆P×T是一组输入弧的有限非空集合，定义了库所到变迁的输入关系流；FO⊆T×P是一组输出弧的有限非空集合，定义了变迁到库所的输出关系流；M0是N的初始标记。托肯携带了时间和数据信息。对于每一个变迁，都存在与之相关的变迁函数、最小变迁时延和最大变迁时延。

将抑制弧加入PRES+模型中，得到PIRES+模型。

定义2PIRES+模型N={P,T,FI,FO,I,M0}，其中：P={p1,p2,…,pm}是库所的有限非空集合；T={t1,t2,…,tm}是变迁的有限非空集合；FI⊆P×T是一组输入弧的有限非空集合，定义了库所到变迁的输入关系流；FO⊆T×P是一组输出弧的有限非空集合，定义了变迁到库所的输出关系流；I⊂P×T(I∩F=∅)是抑制弧的有限非空集合；M0：P→N0是N的初始标记，其托肯携带了时间和数据信息。

k=是托肯，其中:v是托肯的类型标识；r是托肯的时间标识。

只有当抑制库所为空时，被抑制的变迁才会被触发。在图形上，抑制弧将库所连接到变迁，并且弧在变迁处以空圆环结束。其余约束与PRES+模型的约束相同。

以下给出两个PIRES+模型具有相同可达性、功能性和实时性的概念。

定义3两个PIRES+模型N1和N2若有相同的可达性需满足：

(1)N1和N2有相同数量的输入库所和输出库所。

(2) 若把相同数目的托肯数放入N1和N2的输入库所中，那么N1和N2的相应输出库所得到的托肯数相同。

定义4两个PIRES+模型N1和N2若有相同的功能性需满足：

(1)N1和N2有相同的可达性。

(2) 若把具有相同类型标识的托肯放入N1和N2的输入库所中，那么N1和N2的相应输出库所得到的托肯的类型标识也相同。

定义5两个PIRES+模型N1和N2若有相同的实时性需满足：

(1)N1和N2有相同的可达性。

(2) 若把具有相同时间标识的托肯放入N1和N2的输入库所中，那么N1和N2的相应输出库所得到的托肯的时间标识也相同。

2 化简规则

2.1 基于T型子网的化简规则

在PIRES+模型中，基于T型子网化简规则(RST)的前提条件是存在一个T型子网满足定义6。示例见图1，T型子网部分被化简为变迁t。

图1 化简规则RST示例

定义6若PIRES+模型NR={PR,TR,FIR,FOR,IR,MR,0}是模型N={P,T,FI,FO,I,M0}的子网，需满足以下条件：

(1)PR⊆P,TR⊆T,PR≠∅,TR≠∅。

(2)FIR=FI∩{(PR×TR)|(PR×TR)∉I),FOR=FO∩(TR×PR),IR=I∩{(PR×TR)|(PR×TR)∈I}。

(4) {tin,tout}⊆TR,tin是NR的唯一输入变迁，tout是NR的唯一输出变迁。

(5) 对于∀t∈TR,存在变迁函数f:τ(p1)×τ(p2)×…×τ(pn)→(q),·t={p1,p2,…,pn},q∈t。

(6) 对于∀t∈TR,存在最小变迁时延d-和最大变迁时延d+,两者均为非负实数且满足d-≤d+。

(7) 子网中的抑制弧不会造成网的死锁。

(8) 同一组库所和变迁不能同时存在有向弧和抑制弧。

定义7对于PIRES+模型NR={PR,TR,FIR,FOR,IR,MR,0}的变迁集TR-{tin,tout}存在变迁函数fR。对于TR-{tin,tout}，∃fR：τ(p1)×(p2)×…×τ(pn)→τ(q)，其中:(TR-{tin,tout})={p1,p2,…,pn};q∈(TR-{tin,tout})。

以图1为例，因为变迁t1和变迁t3是串联关系，变迁t2和变迁t4是串联关系，t1与t2、t3与t4又分别是并联关系，所以fs=(f1∘f3)‖(f2∘f4)(符号∘ 表示复合操作，符号‖表示并列操作)。

假设1假设PIRES+模型的T型子网NR={PR,TR,FIR,FOR,IR,MR,0}满足：

(1) 在一个执行过程中(托肯从tin流入通过NR再从tout流出)，如果tin被触发则tout也会被触发。

(2) 对于PR，如果在初始状态下无托肯，则在执行过程后也不含托肯。

(3) 在tin被触发前和tout被触发后，∀t∈TR-{tin,tout}，t不处于使能状态。

(1)P′=P-PR。

(2)T′=T-TR+{t}。

(6)fR=fout∘fs∘fin。

(8)I′=I-IR。

因为N′-N1=N-N2,所以N′和N有相同的可达性、功能性和实时性。

2.2 基于P型子网的化简规则

在PIRES+模型中，基于P型子网化简规则(RSP)的前提条件是存在一个P型子网满足定义10。示例见图2，P型子网部分被化简为库所p。

图2 化简规则RSP示例

定义10若PIRES+模型NR={PR,TR,FIR,FOR,IR,MR,0}是PIRES+模型N={P,T,FI,FO,I,M0}的P型子网，需满足：

(1)PR⊆P,TR⊆T,PR≠∅,TR≠∅。

(2)FIR=FI∩{(PR×TR)|(PR×TR)∉I),FOR=FO∩(TR×PR),IR=I∩{(PR×TR)|(PR×TR)∈I)。

(4) {pin,pout}⊆PR,pin是NR的唯一输入库所，pout是NR的唯一输出库所。

(5) 对于∀t∈TR,存在变迁函数f:τ(p1)×τ(p2)×…×τ(pn)→τ(q),·t={p1,p2,…,pn},q∈t·。

(6) 对于∀t∈TR,存在最小变迁时延d-和最大变迁时延d+，两者均为非负实数且满足d-≤d+。

(7) 子网中的抑制弧不会造成网的死锁。

(8) 同一组库所和变迁不能同时存在有向弧和抑制弧。

定义11对于PIRES+模型NR={PR,TR,FIR,FOR,IR,MR,0}的变迁集TR存在变迁函数fR。对于TR，∃fR：τ(p1)×τ(p2)×…×τ(pn)→τ(q)，其中:·TR={p1,p2,…,pn};q∈TR·。

以图2为例，因为变迁t1和变迁t3、t2是串联关系，变迁t4和变迁t3、t2是串联关系，t3与t2又分别是并联关系，所以fs=f1∘ (f3‖f2)∘f4。

假设2假设PIRES+模型的P型子网NR={PR,TR,FIR,FOR,IR,MR,0}满足：

(2)PR如果在初始状态下无托肯，则在执行过程后也不含托肯。

(1)P′=P-PR+{p}。

(2)T′=T-TR。

(8)I′=I-IR。

因为N-N1=N′-N2,所以N′和N有相同的可达性、功能性和实时性。

3 应用实例

本节以一个基于手机通信模型的简化实例来说明PIRES+模型化简规则的有效性。

系统初始化后，首先进行终端和键盘的初始化，然后打印无线通信菜单，通过创建键盘控制子程序完成手机号的拨入与拨出。该系统的PIRES+模型如图3所示。

图3 基于嵌入式的手机通信模型

在该模型中，各变迁的含义为：t1表示系统初始化；t2表示终端初始化；t3表示键盘初始化；t4表示打印无信通信菜单；t51表示接受键盘输入；t52表示控制命令判断；t53表示无效信息输入；t54表示拨入号码；t55表示拨出号码；t56表示系统循环等待；t61表示检测是否停止；t62表示停止；t63表示未停止；t7表示返回。

该PIRES+模型中虚线所标注部分为T型子网N1，使用基于T型子网的化简规则RST进行化简得到初步化简模型N′，结果如图4所示。

图4 使用RST规则后的化简结果

图4中，f5=f51∘ ((f52∘ (f54‖f55))‖f53)∘f56,a5=a51+max(a52+max(a54,a55),a53)+a56,b5=b51+max(b52+max(b54,b55),b53)+b56。根据定理1得，所得的初步简化模型N′与原模型有相同的可达性、功能性和实时性。

对于模型N′，虚线所标注部分为P型子网N2。使用基于P型子网的化简规则RSP进行化简，得到模型N″(如图5所示)。

图5 使用RSP规则后的化简结果

对于模型N″，虚线所标注部分可用基于T型子网的化简，得到最终的简化模型Nr(如图6所示)。

图6 最终化简结果

综上所述，最终得到的模型Nr与原模型N有相同的可达性、功能性和实时性。

4 结 语

本文在PRES+的基础上加入抑制弧，得到PIRES+模型。PIRES+模型增强了建模能力，但是在建模和分析过程中存在状态空间爆炸问题。为了缓解此问题。本文提出PIRES+的两种化简规则，并且证明了化简后所得模型与原模型有相同的可达性、功能性和实时性。本文的实例说明了该化简规则的有效性。