一种验证AADL模型运行状态与需求一致性的方法

摘要

一种验证AADL模型运行状态与需求一致性的方法，步骤包括：(1)根据需求中的状态和状态迁移构建AADL模型，AADL模型中模式和模式迁移分别对应需求中的状态和状态迁移；(2)将AADL模型中模式和模式迁移转化为Petri网模型；(3)计算Petri网模型的关联矩阵C；(4)利用Petri网模型的状态方程判断构建的AADL模型运行状态与需求是否一致。本发明提出将AADL模型中的“模式”及“模式迁移”映射为Petri网模型中的库所及变迁，并将此Petri网模型作为被测模型，结合Petri网模型性质和AADL模型的特点计算AADL模型可达的状态集合，从而达到判断建立的AADL模型运行状态是否与需求一致的目的，提高了所建AADL模型的正确性，缩短了系统建立时间，节省了系统建立成本。

主权项

1.一种验证AADL模型运行状态与需求一致性的方法，其特征在于步骤如下：(1)根据需求中的状态和状态迁移构建AADL模型，AADL模型中模式和模式迁移分别对应需求中的状态和状态迁移；(2)将AADL模型中模式和模式迁移转化为Petri网模型，AADL模型与Petri网模型的转换关系为：AADL模型中的模式映射为Petri网模型中的库所s_i，库所s_i的集合形成库所集S，i∈[0，n]，初始库所s₀的token为1，AADL模型中的模式迁移映射为Petri网模型中的变迁t_j，变迁t_j的集合形成变迁集T，j∈[1，m]；(3)计算Petri网模型的关联矩阵C，关联矩阵C以库所集S_x变迁集T为序标集，其关联矩阵C的元素C(s_i，t_j)＝W(t_j，s_i)-W(s_i，t_j)，W(s，t)为(s，t)上的权，W(t，s)为(t，s)上的权；(4)利用Petri网模型的状态方程判断构建的AADL模型运行状态与需求是否一致，具体判断过程如下：1)将需求中的所有状态根据其对应的Petri网模型中库所进行标识，需求中的状态st_i对应于Petri网模型中库所s_i，需求中的所有状态迁移根据其对应的Petri网模型中变迁进行标识，需求中的状态迁移tr_j对应于Petri网模型中变迁t_j，根据需求列出将st₀变为st_i的q个变迁序列T，q≥1；2)对于每一个变迁序列，通过Petri网模型的状态方程M₀+CU＝M计算得到目标状态标识M，根据M中M(st_i)的值判断AADL模型运行状态与需求是否一致；所述Petri网模型的状态方程为M₀+CU＝M，M₀为根据需求中的状态确定的初始状态标识向量，向量元素M₀(st_i)为该标识下st_i处的token值；C为关联矩阵；U为根据需求中的状态迁移确定的变迁标识向量，其状态元素U(tr_j)为具体变迁序列中变迁tr_j对应的标识，当变迁tr_j发生时U(tr_j)为1，变迁tr_j不发生时U(tr_j)为0；M为Petri网模型的目标状态标识向量，向量元素M(st_i)为该标识下st_i处的token值；根据M中M(st_i)的值判断AADL模型运行状态与需求是否一致的过程为：设f_p为第p个变迁序列T_p转化后的AADL模型运行状态与需求是否一致的标识，p∈[1，q]，若第p个变迁序列T_p中含有导致状态st_i出现的直接变迁个数与M(st_i)的值相同，则在第p个变迁序列T_p下所构建的AADL模型运行状态与需求相一致，置f_p＝1；若第p个变迁序列T_p中含有导致状态st_i出现的直接变迁个数与M(st_i)的值不相同，则在第p个变迁序列T_p下所构建的AADL模型运行状态与需求不一致，置f_p＝0；设F_i＝f₁×f₂×…×f_p×…×f_q，若F_i＝1，则从st₀变为st_i的q个可行变迁序列T下所构建的AADL模型运行状态与需求相一致；若F_i＝0，则从st₀变为st_i的q个可行变迁序列T下所构建的AADL模型运行状态与需求不一致。