4.4.2 武器装备体系流程扩展模型

为了实现武器装备体系动态演化的形式化，满足作战流程在线迁移切换的要求，基于着色Petri网，从控制流和数据流对武器装备体系流程模型进行描述和分析。

定义4.16（体系流程扩展模型WF_CPN）：

WF_CPN=(∑,P_c,P_d,T,A_c,A_d,K,C,G,E_c,E_d,AT,IN,OUT,I)

（1）∑为数据类型的集合，并且控制托肯类型CONTROL∈∑，即colorCONTROL=with st；

（2）P_c为非空有限控制库所集，存放网构软件服务操作的控制托肯以及控制参数；

（3）P_d为非空有限数据库所集，存放网构软件服务操作的数据托肯以及数据参数；

（4）T为非空有限变迁集，网构软件服务操作的集合；

（5）A_c⊆P_c×T∪T×P_c是一个有限控制弧集，且P_c∩T=P_c∩A_c=T∩A_c=∅；

（6）A_d⊆P_d×T∪T×P_d是一个有限数据弧集，且P_d∩T=P_d∩A_d=T∩A_d=∅；

（7）K是控制库所容量函数，∀p_c∈P_c有K（p_c）=st，表示在模型的一个控制库所中最多只能有一个控制托肯；

（8）C是数据类型函数，表示为C：（P_c∪P_d）→∑，有P_c→CONTROL，P_d→∑\CONTROL，并且模型中如果有指定库所p∈（P_c∪P_d），则它的托肯类型为C（p）；

（9）G是防卫函数，表示为G：T→G（t），要求满足∀t∈T：[Type（G（t））]=B∧Type（Var（G（t）））⊆∑，指定变迁引发须满足的前提条件；

（10）E_c是控制弧A_c上的函数，有E_c（a_c）=st表示控制托肯的输入、输出；

（11）E_d是数据弧A_d上的函数，表示为E_d：A_d→E_d：（a_d），要求满足表达式：，式中p_d是A_d（a_d）中的库所，p_d的数据类型集上的多重集是，E_d是数据托肯的输入、输出；

（12）AT是变迁的属性函数，定义为AT：T→Attributes（tType，opName，portType，inputSet，outputSet），是模型中相关操作需要指定变迁类型、操作名称、端口类型、输入参数和输出参数，对于∀t∈T，（inv₁，inv₂）∈inputSet，outv₁∈inputSet，则接口操作可记为；

（13）IN是变迁T中需要输入的参数变量：IN∈P_d且¬∃t∈T：＜t，IN＞∈A_d，即没有前集；

（14）OUT是变迁T中需要输入的参数变量：OUT∈P_d且¬∃t∈T：＜OUT，t＞∈A_d，即没有后集；

（15）I是一初始化函数，满足。

在WF_CPN模型中没有孤立元素，模型入口为P_i={p_i|p_i∈P_c∧·P_I=∅}，模型出口为，模型入口点能表达过程模型的开始，本文默认模型的入口库所为1，对模型出口的数量不加限制。图4.8给出了WF_CPN模型示意图。WF_CPN的变迁表示的相关操作也称为活动，操作对应的变迁有两类托肯输入，分别为控制托肯和数据托肯。在WF_CPN模型中活动执行的顺序由控制托肯的流向来决定。在WF_CPN模型中数据托肯有两种，分别是活动（操作）数据与业务逻辑控制数据，前者描述了体系流程活动的输入参数和输出参数，后者与控制托肯一起决定流程的具体执行路径。

WF_CPN模型基于着色Petri网，将库所分为数据库所和控制库所，由数据托肯和控制托肯一起决定体系的执行流程，从形式化角度实现了流程的控制流和数据流的分离，为武器装备体系动态演化分析提供了形式化基础。

武器装备体系的动态演化是在流程运行过程中实施的，WF_CPN模型的动态运行规则为武器装备体系的流程切断提供了基础。

在WF_CPN模型中，对所有的变迁t∈T及所有的（x₁，x₂）∈（P_c∪P_d）×T∪T×（P_c∪P_d）有：

（1）A（t）={a∈（A_c∪A_d）|a∈（P_c∪P_d）×{t}∪{t}×（P_c∪P_d）}：与t关联的弧集；

（2）Var（t）={v|v∈Var（G（t））∨∃a∈A（t）：v∈Var（E（a））}：t的变量集；

（3）A（x₁，x₂）={a∈（A_c∪A_d）|a∈（x₁，x₂）}：两端为x₁、x₂的弧集；

（4）当a∈（A_c（x₁，x₂）∪A_d（x₁，x₂））时，E（x₁，x₂）=∑E（a）：两端点为x₁、x₂的弧函数集合。

在WF_CPN中，它的动态行为由引发规则来定义，当变迁发生时库所中的托肯数量都会产生动态变化，这样推进流程运行。在WF_CPN模型中引入了数据类型和变量，在变迁发生之前，必须对变迁进行绑定（赋值）。

定义4.17（变迁绑定）：是定义在Var（t）之上的函数b，满足：①∀v∈Var（t）：b＜v＞∈Type（v）；②G（t）＜b＞为“真”。

变迁绑定是将变迁t中的每个变量赋值，并且要求满足防卫表达式，变迁才能引发。绑定记为＜v_l=c_l，v₂=c₂，…，v_n=c_n＞，Var（t）={v_l，v₂，…，v_n}。绑定的集合记为B（t）。

定义4.18（绑定元素）：定义为一个（t，b）对，t∈T，b∈B（t），它的集合表示为BE。

定义4.19（托肯元素）：定义为一个（p，c）对，p∈（P_c∪P_d），c∈C（p），它的集合表示为TE。

定义4.20（绑定元素）：定义为一个（t，b）对，t∈T，b∈B（t），它的集合用BE表示。

定义4.21（标识）：定义为所有托肯元素集合TE之上的一个多重集，用M来表示。

定义4.22（步）：定义为所有绑定元素集合BE之上的非空有限多重集，用Y表示。

在上述定义中，标识用来描述WF_CPN的状态，步表示引起WF_CPN状态发生改变的事件的发生步骤。

定义4.23（步的使能）：当WF_CPN处于标识M时，当且仅当：

（1）∀p_d∈P_d:∑E_d(p_d,t)＜b＞≤M(p_d);

（2）∀p_c∈P_c∧p_c∈·t:∑E_c(p_c,t)≤M(p_c);

（3）∀p_c∈P_c∧p_c∈·t-t·:M(p_c)+E_c(t,p_c)≤K(p_c);

（4）∀p_c∈P_c∧p_c∈·t∩t·:M(p_c)+E_c(t,p_c)-E_c(p_c,t)≤K(p_c);

则步Y是使能的，此时称绑定（t，b）有效，并且变迁t可引发。

定义4.24（步的发生）：步Y的发生，它能够使WF_CPN的状态从标识M₁改变为M₂，此时从标识M₁可直达标识M₂。

定义4.25（步发生后的标识）：当在标识M₁时步Y使能，则其发生后标识变为M₂：

步Y的发生引起模型标识变化的过程，记为M₁[t＞M₂。

WF_CPN模型定义了变迁之间的数据依赖关系，在WF_CPN模型中，变迁可以接收的全部参数，是以该变迁为目标的所有数据弧的弧函数所决定的。变迁必须提供的全部参数，是该由变迁出发的所有数据弧的弧函数所决定的，弧函数同时指定了变迁之间交互数据的数据类型。

从上面分析来看，WF_CPN模型不仅描述了变迁之间的控制关系，而且显式描述变迁之间的数据依赖关系，为了深入研究作战运行流程的迁移切换，需要对WF_CPN模型的数据依赖关系及特性进行分析。