飞行程序发布订阅服务Petri网建模分析

王洁宁，姜高扬

（中国民航大学空中交通管理研究基地，天津 300300）

长期以来，航行情报数据还是以纸质航图、AIP手册、NOTAM电报的形式通过邮局和AFTN网进行传递，各个航行情报系统彼此孤立而不能互相调用，所提供的航行情报服务在时效性和信息量方面逐渐不能满足实际需求。为此国际民航组织提出要将传统的航行情报服务（AIS）逐步过渡到航行情报管理（AIM）。AIM就是在全球范围内以交互方式提供满足当前及未来ATM系统和所有飞行阶段需要的航空数据。它明确了航空信息的提供将以数据为中心而不是以产品为中心，其最终目标是逐渐向SWIM——全系统信息管理过渡。

飞行程序作为航行情报的主要内容之一，其发布也将由现在的纸质产品、邮局传送的方式转变为数字信息、网络传输的方式，机场、空管和航空公司的航行情报室获取情报的方式也将由被动等待邮局传送转变为主动订阅感兴趣的信息，因此建立合理的通信服务将是本次过渡所面临的主要问题之一。

发布订阅通信范型作为一种异步通信机制，在时间和空间上具有完全的解耦性，近年来得到了工业界和学术界的普遍关注，已经成为研究的热点。范洪亮[1]、张煜[2]等人研究了发布订阅系统中的路由算法和匹配技术，但是如何将发布订阅服务应用在飞行程序数据共享方面尚未有人研究，因此本文在前人研究的基础上，利用UML建立飞行程序发布订阅服务概念模型，之后给出相应的Petri网模型，利用可达树和P不变量方法分析和验证模型的有效性，为搭建飞行程序发布订阅服务系统奠定理论基础。

1 发布订阅服务概念模型

飞行程序发布订阅服务可以抽象为一个六元组{P，S，B，P_operation，S_operation，B_operation}，其中P表示飞行程序的发布者，即中国民航局航行情报服务中心；S={S1，S2，…，Sn}表示飞行程序的订阅者，即机场、航空公司和空管的航行情报室；B={B1，B2，…，Bk}表示k个中间代理；P_operation定义了航行情报服务中心具有的操作，如向外发布航行情报publish（）；S_operation定义了机场、航空公司和空管的航行情报室具有的操作，典型的有订阅subscribe（）和取消订阅unsubscribe（）；B_operation定义了中间代理具有的操作，比如匹配用户订阅条件操作match（）和通知操作notify（）。

飞行程序发布订阅服务概念模型可用UML中的用例图和顺序图描述，用例图体现了系统的行为，即系统提供的外部可见的服务，可为系统的上下文及系统的需求建模；顺序图强调了消息的时间顺序，可为发布和订阅的具体过程建模[3]。

1.1 发布订阅服务用例图

飞行程序发布订阅服务的用例图如图1所示，用户发布或者订阅信息之前必须登录系统，通过身份验证以后方可进行相应的操作，这样就保证了系统的安全性。登录系统之后机场航行情报室向中间代理提交自己的订阅条件，说明需要哪种飞行程序；航行情报服务中心连续地向中间代理发布最新的飞行程序数据；中间代理将所有发布的飞行程序数据与订阅者的订阅条件相匹配，筛选出符合用户需求的数据通知给用户。当订阅者对某些数据不再感兴趣时可以取消之前的订阅。

1.2 订阅服务顺序图

订阅服务顺序图描述了机场、航空公司和空管的航行情报室订阅飞行程序的流程，如图2所示。航行情报室首先调用entry（）函数登录系统，之后系统通过validate（）函数验证用户身份，如果是授权用户则可以执行subscribe（）操作。代理收到信息以后将信息解析为内部数据结构，根据用户的订阅和取消订阅的条件，过滤出用户想要取消的信息，更新用户订阅列表，最后调用add（）函数将最新的订阅列表加入到匹配模块中去。

1.3 发布服务顺序图

与订阅服务相同，发布服务顺序图描述了发布服务消息传递的先后顺序，如图3所示。其中entry（）和validate（）函数与订阅服务中的函数相同，parse（）函数是按照用户的订阅条件进行发布内容的解析，通过Match模块将飞行程序数据从航行情报中剥离出来，生成订阅用户列表，之后中间代理依据用户列表将不同的飞行程序数据通知给相应的用户。

2 发布订阅服务Petri网建模

发布订阅服务概念模型刻画了系统需求和工作流程，但是模型的正确性和有效性尚不明确，因此需要采用合理的方法对概念模型的性质进行评估。Petri网是分布式系统的建模和分析工具，其特别适合于描述系统中进程或部件的顺序、并发、冲突以及同步等关系[4]，通过Petri网建模，可以对系统模型的性能和结构进行分析与评估，进而可以反映出模型的正确性和有效性。

Petri网和P不变量的定义和性质[5]：

定义1（Petri网）PN={P，T，I，O，m}，其中：

P={p1，…，pn}是库所的有限集合，n>0 为库所的个数；

T={t1，…，tm}是变迁的有限集合，m>0 为变迁的个数；

P∩T=Ø，且P∪T≠Ø，即库所和变迁不相交且网中至少有一个元素；

I：P×T→N是输入矩阵，其定义了从P到T的有向弧的权的集合，这里N={0，1，…}为非负整数集；

O：T×P→N是输出矩阵，其定义了从T到P的有向弧的权的集合；

m：P→N是标识，其为一列向量，其第i个元素表示第i个库所里的Token数。

定义2（P不变量） 一个P不变量为一（n×1）非负整数向量x，并满足xTC=0，其中C=O-I称为关联矩阵。

性质1（P不变量） 若只要存在一个（n×1）正实数向量x，使得xTC≤0，则PN是结构上有界的。

性质2（P不变量） 若只要存在一个（n×1）正实数向量x，使得xTC=0，则PN是结构上守衡的。

2.1 订阅服务的Petri网模型

假设订阅者有两个订阅条件和一个取消订阅的条件，因此系统的初始条件为库所p1中有2个托肯，代表用户需要订阅的两条信息，p3中1个托肯，代表用户取消某一条信息的请求，在变迁t3激发前，来自p3的取消订阅条件和来自p4的订阅条件一一比较，如果该信息是用户指定要取消的，则放入库所p5中，表示信息已经取消，否则放入p6中，作为更新过的用户订阅列表，然后加入到匹配模块p7中去。匹配模块会接收发布者发来的各种信息，并与其中的用户订阅列表匹配。订阅系统的Petri网模型如图4所示。

库所变迁的含义如表1所示。

表1 订阅服务库所变迁的含义Tab.1 Place and transition meaning of Sub-service

2.2 发布服务的Petri网模型

发布服务的Petri网模型如图5所示，系统的初始条件为p1和p3中存在托肯，只有这样变迁t2才能激发，其实际意义为只有当系统中有发布信息且有用户订阅时，匹配模块才开始工作。一旦发布的信息与用户需求匹配成功，则生成订阅用户列表，中间代理根据订阅用户列表将信息通知给用户。

库所和变迁的含义如表2所示。

表2 发布服务库所和变迁的含义Tab.2 Place and transition meaning of Pub-service

3 模型的分析和验证

Petri网的分析方法可分为基于可达树与基于不变量两种方法，前者为图形分析方法，后者为数学分析方法。下面分别用可达树和不变量分析方法对飞行程序发布订阅服务Petri网模型进行分析和验证。

3.1 订阅服务Petri网模型的可达树分析

从初始标识m0开始，通过变迁将PN所有可能的标识关联起来，组成的树状结构图称为可达树。树中的节点为标识，节点之间用表示变迁的箭头连接，箭头起端所连接的标识通过该箭头所代表的变迁的激发，产生该箭头末端所连接的标识。

可达树的构造算法如下[6]：

步骤1：以初始标识m0为树根，并作上“new”的记号；

步骤2：若“new”标识存在，则做以下事情，否则终止；

步骤3：选择某一“new”标识m；

1）若m与树中间已有的其他标识相同，则将其记为“old”，然后转向其他“new”标识；

2）若在m下无变迁使能，则将m记为“dead end”（死点）；

步骤4：对于m下使能的所有变迁t，做以下事情：

1）激发 t，产生标识 m′；

2）若在从树根至m′的路径上存在一标识m″，使得m′＞m″，则对于那些m′（p）＞m″（p）成立的p，用w取代m′（p）；

3）以m′为一节点，从m至m′画一有向线，将其记为 t，并将 m′记为“new”；

步骤5：除去m的“new”标志，回到步骤2。

订阅服务的可达树如图6所示。

图6 订阅服务Petri网模型的可达树Fig.6 Reachability tree of Sub-service Petri net model

基于可达树可作如下分析：

1）当且仅当树中所有节点上均不出现w时，PN是有界的；

2）当且仅当树中所有的节点上仅包含0或1时，PN是安全的；

3）若没有任何死点包含w，则树中死点的个数就是PN死标识的数目；

4）若某变迁在树中不出现，则该变迁是死变迁，死变迁从反面描述Petri网的活性。

根据上述分析，由图6所示的可达树可知，所建Petri网模型是有界的，除了 p1、p2、p4，其他库所是安全的，PN死标识的数目为1，即最后一个标识为死标识，对应系统的结束状态。由于所有变迁都在树中出现，因此不包含死变迁。

3.2 订阅服务Petri网模型的不变量分析

不变量分析方法是基于矩阵线性代数，其优点是依据简单的线性代数方程就能正确地确定Petri网的性能，进而确定系统的结构特性[4]。订阅Petri网的不变量分析如下：

设输入矩阵为I、输出矩阵为O、关联矩阵为C，则

求解xTC=0得

满足该方程的一个解为

得到一个 P 不变量（2 2 2 2 1 1 1）T。

据性质 1 和性质 2，存在 x=（2 2 2 2 1 1 1）T＞0，满足xTC=0，因此该Petri网模型是结构上有界且守衡的。有界性说明系统中的托肯数没有超过每个库所的容量限制，在用程序实现订阅服务时计算机运行的结果不会出现溢出；守衡性说明系统中包含的资源的数量是固定的，尽管系统的标识在变化，但其所包含的托肯数维持不变，这遵循资源既不能产生又不能消失的法则，其实际意义在于一旦订阅事件发生后，订阅的信息不会无缘无故地产生和消失，因此可认为系统的运行是安全和稳定的。

3.3 发布服务Petri网的可达树分析

根据可达树的构造算法所构造出的发布服务Petri网可达树如图7所示。

图7 发布服务Petri网的可达树Fig.7 Reachability tree of Pub-service Petri net model

由于所有节点上均不出现w，PN是有界的；树中所有的节点上仅包含0或1时，PN是安全的；树中最后一个标识是死标识，对应系统的结束状态；所有变迁都在树中出现，因此不包含死变迁。

3.4 发布服务Petri网的不变量分析

输入矩阵I、输出矩阵O、关联矩阵C分别为

求解xTC=0得

满足该方程的一个解为

得到一个P 不变量（1 1 1 1 1）T。

根据性质1和性质2，存在一个P不变量x=（1 1 1 1 1）T＞0，满足 xTC=0，因此该 Petri网模型是结构上有界且守衡的，对应的实际系统是安全和稳定的。

4 结语

本文利用UML建立了飞行程序发布订阅服务概念模型，根据概念模型中信息处理的流程设计了相应的Petri网模型，通过可达树分析和P不变量分析，得出所建的Petri网模型是结构上有界且守衡的，不包含死变迁。由于Petri网模型是依据概念模型而建，因此可以证明本文所建立的概念模型是正确的、有效的，从而为飞行程序发布订阅服务系统的构建奠定了理论基础。下一步的工作是引入赋时的概念，探讨系统处理大量飞行程序发布订阅信息时的工作效率问题，进一步完善和优化发布订阅服务系统。

[1]苑洪亮.基于内容的“发布/订阅”若干关键技术研究[D].长沙：国防科技大学，2006.

[2]张 煜.发布/订阅系统中信息订阅匹配技术研究与实现[D].南京：南京理工大学，2009.

[3]冀振燕.UML系统分析与设计教程[M].北京：人民邮电出版社，2009：85-86.

[4]吴哲辉.Petri网导论[M].北京：机械工业出版社，2006：1-23.

[5]袁志娟.基于PSO的多跑道运行优化方法及仿真建模[D].天津：中国民航大学，2010.

[6]江志斌.Petri网及其在制造系统建模与控制中的应用[M].北京：机械工业出版社，2004：50-55.