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

摘要

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

说明书

技术领域

本发明涉及一种验证AADL模型运行状态与需求一致性的方法，

背景技术

近年来，伴随着嵌入式软件的规模和复杂度的不断增加，其开发周期和开发成本也急剧增加，对非功能属性的要求也越来越高。传统的以代码为核心的开发方法已经不能适应这种趋势，开发的重点逐步从代码级提前到模型级。模型驱动结构方法MDA(Model Driven Architecture)就是由OMG提出的一种很有应用前景的基于模型的软件开发方法。使用MDA软件开发方法，系统设计者在设计阶段把需求转化成一种形式化语言描述的模型，再对系统模型进行充分的分析验证，将可能存在的大部分错误解决，使系统模型自动生成的代码中出现问题的几率将大大降低，当系统设计出现变更时，只需要修改系统模型后重新生成代码，目前MDA方法已经成为嵌入式软件开发中的研究热点。成功应用模型驱动开发方法的核心问题就是模型能否完整正确地反映软件需求。本发明就是提出一种基于AADL模型的软件开发过程中所构建的系统模型运行状态与需求一致性的验证方法。

AADL(Architecture Analysis and Design Language，结构分析和设计语言)是在自动化工程师协会SAE(Society of Automotive Engineers)指导下开发的，在目前基于模型驱动的开发方法中应用最为广泛。AADL将构件抽象为软件构件、执行平台(硬件)和系统构件3种类型，按照构件及构件之间的相互作用对应用系统的结构进行描述与分析，并且支持对嵌入式软件非功能属性的描述。AADL模型并不关心具体的功能实现，描述的仅仅是系统框架，从而在体系结构级对系统的非功能属性进行规约，适合具有挑战性资源约束(如尺寸、重量和功率)、严格实时要求和高性能保证等级的嵌入式系统。

目前面向AADL的测试工具主要包括SEI开发的开源工具集OSATE(open source AADL tool environment)，Axlog开发的全局仿真工具ADeS工具等。OSATE提供基于AADL的建模和基本的语义检查和架构分析等，但侧重于模型中构件的输入输出连接等检查和分析。Axlog开发的ADeS工具以模型的全局分析为目标，但是目前还不支持模式和模式迁移，只能在初始模式下，进行任务分析，不能完整的验证系统的运行状态。计算机科学2009年第11期公开的《AADL模型的测试方法研究》利用马尔科夫链模型对AADL模型进行测试，以考察所建模型与需求中期望的模型行为的一致性，但其阈值等依据经验获得，测试结果欠缺准确性，且最后判断结果只能笼统地说所构建的AADL模型模式迁移有错误，并不能明确说明错误发生在哪些事件迁移上。

发明内容

本发明的技术解决问题是：克服现有技术的不足，提供一种验证AADL模型运行状态与需求一致性的方法，提高了AADL模型建立的可靠性。

本发明的技术解决方案是：一种验证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以库所集Sx变迁集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模型运行状态与需求不一致。

本发明与现有技术相比的有益效果是：本发明提出将AADL模型中的“模式”及“模式迁移”映射为Petri网模型中的库所及变迁，并将此Petri网模型作为被测模型，结合Petri网模型性质和AADL模型的特点计算AADL模型可达的状态集合，达到判断建立的AADL模型运行状态是否与需求一致的目的，从而提高了所建AADL模型的正确性，缩短了系统建立时间，节省了系统建立成本。

附图说明

图1为本发明的流程图；

图2为AADL模型与Petri网的映射关系图。

具体实施方式

通过将AADL模型中构件的“模式”及“模式迁移”映射为Petri网模型，并结合Petri网的关联矩阵以及状态方程等理论，形成了判断所构建的AADL模型运行状态与需求一致性的验证方法，其流程如图1所示，具体实施步骤如下：

(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]；

Petri网具有丰富的系统描述手段和行为分析技术，是一种适合于描述分布并发系统行为的模型。Petri网模型定义为六元组∑＝(S，T；F，K，W，M₀)，其中S表示库所(place)集，T表示变迁(transition)集，F为从S和T构造出的流关系(flow relation)。K，W和M₀分别为∑的容量函数，权函数和初始标识。

因为AADL模型不关心具体的功能实现，而是在框架级对系统进行建模。即AADL模型中的模式和模式迁移是在系统层次上对系统状态和变化的描述，因此从这个意义上讲，将AADL模型转化成Petri网模型以后对应的权函数W为1，容量函数K≥1。

(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模型运行状态与需求不一致。

实施例：

以一个飞行控制系统为例，说明本发明的实施步骤：

首先给定一个简单的需求。本发明重点关注需求中的状态和引起状态迁移的事件。系统接收到起飞信号后，从初始状态进入起飞准备状态。然后判断起控条件，若起控条件不合适，系统停飞，舵控置0，返回初始状态。若起控条件满足，则进入起飞状态，起飞的过程中通过计算角度等控制飞行状态，直到运行结束，进入停飞状态，舵控置0，返回初始状态。

(1)根据需求中的状态和状态迁移构建AADL模型，AADL模型中模式和模式迁移分别对应需求中的状态和状态迁移，根据需求所构建的AADL模型如图2的左半部分所示。

(2)根据转换关系将所构建的AADL模型中的模式和模式迁移转换成Petri网模型，结果如图2所示的右半部分，其中，s₀表示初始状态，s₁表示起飞准备状态，s₂表示停飞状态，s₃表示起飞状态；t₁表示起飞信号，t₂表示起控条件不合适，t₃表示舵控置0，t₄表示起控条件合适，t₅表示运行结束。

(3)计算Petri网模型的关联矩阵C，其关联矩阵的矩阵元素C(s_i，t_j)＝W(t_j，s_i)-W(s_i，t_j)，因此，图2右半部分所对应的关联矩阵为：

(4)利用Petri网模型的状态方程判断构建的AADL模型运行状态与需求是否一致；

将需求中的所有状态根据其对应的Petri网模型中库所进行标识，得到：st₀表示初始状态，st₁表示起飞准备状态，st₂表示停飞状态，st₃表示起飞状态；需求中的所有状态迁移根据其对应的Petri网模型中变迁进行标识，得到：tr₁表示起飞信号，tr₂表示起控条件不合适，tr₃表示舵控置0，tr₄表示起控条件合适，tr₅表示运行结束。

根据需求，初始状态标识向量

根据发明中所述的判断方法，取i＝1，2，3，分别进行AADL模型运行状态与需求的一致性判断：

当i＝1时

1)根据需求列出将st₀变为st₁的可行变迁序列，共1个；

变迁序列1：接收起飞信号，对应于需求中的tr₁发生。

2)对于该变迁序列，通过Petri网模型的状态方程M₀+CU＝M计算得到目标状态标识M，根据M中M(st₁)的值判断AADL模型运行状态与需求是否一致；

对于该变迁序列T₁，根据∑的状态方程M₀+CU＝M，计算出在该变迁序列下，系统的目标状态集M。

$M=\left(\begin{array}{c}1\\ 0\\ 0\\ 0\end{array}\right)+\left(\begin{array}{ccccc}-1& 0& 1& 0& 0\\ 1& -1& 0& -1& 0\\ 0& 1& -1& 0& 1\\ 0& 0& 0& 1& -1\end{array}\right)\left(\begin{array}{c}1\\ 0\\ 0\\ 0\\ 0\end{array}\right)=\begin{array}{}\left(\begin{array}{c}0\\ 1\\ 0\\ 0\end{array}\right)\end{array}$

此时M(st₁)＝1。

因为T₁中含有1个导致状态st₁出现的直接变迁tr₁，即T₁中含有导致状态st₁出现的直接变迁个数与M(st₁)的值相同，所以f₁＝1。

F₁＝f₁＝1，说明从st₀变为st₁的变迁序列下所构建的AADL模型运行状态与需求是一致的；

当i＝2时

1)根据需求列出将st₀变为st₂的可行变迁序列，共两个；

变迁序列1：接收起飞信号，起控条件不满足，对应于需求中的tr₁，tr₂发生；

变迁序列2：接收起飞信号，起控条件满足，运行结束，对应于需求中的tr₁，tr₄，tr₅发生。

2)对于每一个变迁序列，通过Petri网模型的状态方程M₀+CU＝M计算得到目标状态标识M，根据M中M(st_i)的值判断AADL模型运行状态与需求是否一致；

对于第1个变迁序列T₁，根据∑的状态方程M₀+CU＝M，计算出在该变迁序列下，系统的目标状态集M。

$M=\left(\begin{array}{c}1\\ 0\\ 0\\ 0\end{array}\right)+\left(\begin{array}{ccccc}-1& 0& 1& 0& 0\\ 1& -1& 0& -1& 0\\ 0& 1& -1& 0& 1\\ 0& 0& 0& 1& -1\end{array}\right)\left(\begin{array}{c}1\\ 1\\ 0\\ 0\\ 0\end{array}\right)=\begin{array}{c}\left(\begin{array}{c}0\\ 0\\ 1\\ 0\end{array}\right)\end{array}$

此时M(st₂)＝1。

在该变迁序列T₁下只包含1个引起st₂出现的直接变迁tr₂。所以f₁＝1。

对于第2个变迁T₂，根据∑的状态方程M₀+CU＝M，计算出在该变迁序列下，系统的目标标识

此时M(st₂)＝1。

在该变迁序列T₂下含有1个引起st₂出现的直接变迁tr₅。因此在该变迁序列下所构建的AADL符合需求，f₂＝1。

综上，F₂＝f₁×f₂＝1，说明从st₀变为st₂的变迁序列下所构建的AADL模型运行状态与需求是一致的；

当i＝3时

1)根据需求列出将st₀变为st₃的可行变迁序列，共1个；

变迁序列1：接收起飞信号，起控条件合适，对应于需求中的tr₁，tr₄发生。

2)对于该变迁序列，通过Petri网模型的状态方程M₀+CU＝M计算得到目标状态标识M，根据M中M(st₁)的值判断AADL模型运行状态与需求是否一致；

对于该变迁序列T₁，根据∑的状态方程M₀+CU＝M，计算出在该变迁序列下，系统的目标状态集M。

$M=\left(\begin{array}{c}1\\ 0\\ 0\\ 0\end{array}\right)+\left(\begin{array}{ccccc}-1& 0& 1& 0& 0\\ 1& -1& 0& -1& 0\\ 0& 1& -1& 0& 1\\ 0& 0& 0& 1& -1\end{array}\right)\left(\begin{array}{c}1\\ 0\\ 0\\ 1\\ 0\end{array}\right)=\begin{array}{c}\left(\begin{array}{c}0\\ 0\\ 0\\ 1\end{array}\right)\end{array}$

此时M(st₃)＝1。

因为T₁中含有1个导致状态st₃出现的直接变迁tr₄，即T₁中含有导致状态st₃出现的直接变迁个数与M(st₃)的值相同，所以f₁＝1。

F₃＝f₁＝1，说明从st₀变为st₃的变迁序列下所构建的AADL模型运行状态与需求是一致的；

因为F₁，F₂，F₃的值均为1，所以所构建的AADL模型与需求一致。

说明：如果F_i＝0，说明从初始状态st₀到目标状态st_i的变迁序列有问题，需要返回去修改模型设计。

本发明未详细描述内容为本领域技术人员公知技术。