一种基于AADL模态时间自动机模型的嵌入式软件测试方法

摘要

本发明涉及一种基于AADL模态时间自动机模型的嵌入式软件测试方法，技术特征在于：根据AADL架构模型文件，生成带有模态信息的AADL系统构件树，通过广度优先遍历构件树，构造AADL模型的时间自动机模型。利用现有的时间自动机的验证工具，对AADL模型模态转换的正确性及时间属性进行验证。本发明方法能够在嵌入式软件设计早期阶段对模型实施测试，尽早发现软件模型的正确性和实时性是否满足设计需求，及时修订设计方案，从而缩短了嵌入式实时系统开发的周期并节约了开发成本。

主权项

1.一种基于AADL模态时间自动机模型的嵌入式软件测试方法，其特征在于步骤如下：步骤1：构建AADL架构模型描述文件的构件树，以系统构件作为树的根节点，下一层为子系统构件，依次向下为进程构件、线程构件；以构件的名称作为构件树中的每个节点的标识，每个节点包含该构件的模态信息；所述的模态信息包括模态名称、引起模态转移的事件、模态转移的目标模态和系统的初始模态；步骤2：对步骤1得到的构件树进行广度优先遍历，提取每个节点的当前模态，并存储至时间自动机六元组<∑，S，S₀，C，I，E>的S集合中，提取到的系统初始模态信息存储在S₀集合中。其中：S是一个有限的状态集合，S＝{SOM₁，SOM₂，…，SOM_i}为模态的状态空间，SOM_i为任一模态；S₀是一个起始状态集合；∑＝{ep₁，ep₂，…，ep_k}是一个有限事件集合，ep_k是集合中某事件；C是一个有限时钟集合；I是一个映射，它为S中的每一个状态SOM_i指定Φ(C)中的某一个时钟约束；E是一个转移集合，E＝{e₁，e₂，…，e_k}，e_i表示每条转移，每条转移(s，a，δ，λ，s′)表示输入字符a时，从位置s到s′的一个转移，δ是定义在时钟集C上的一个时钟约束，在位置转移发生时必须被满足，λ表示发生位置转移时被重置的所有时钟变量的集合，且满足步骤3：根据步骤2得到的模态的状态集合S，将S中父节点的模态向量与它的孩子节点的模态向量作笛卡尔乘积，将得到的模态向量继续添加到S中，构造完成时间自动机<∑，S，S₀，C，I，E>的状态集合S；步骤4：根据步骤1得到的构件树，再一次对构件树进行广度优先遍历，提取每个节点中引起模态转移的事件，以向量ep_k(k≥1)表示，并存储至<∑，S，S₀，C，I，E>中的∑中，∑＝{ep₁，ep₂，…，ep_k}，构造完成时间自动机<∑，S，S₀，C，I，E>的事件集合∑；步骤5：根据步骤3和步骤4得到的状态集合S和事件集合∑，按照如下的方法构造时间自动机中的转移集合E：广度优先遍历步骤1得到的构件树，提取事件集合中每个事件ep_i(1≤i≤k)的源模态集合M_is＝{SOM_si，…，SOM_sj}和目标模态集合M_it＝{SOM_ti，…，SOM_sj}，得到表示在事件集合ep_i触发下，模态从M_is转移到模态M_it的每条转移e_i＝(M_is，e_pi，_，_，M_it)，转移集合为E＝{e₁，e₂，…，e_k}其中：对∑中的每个ep_i其转移函数为e_i＝(M_is，ep_i，_，_，M_it)，$M_{\mathrm{is}}\subseteq S,$$M_{\mathrm{it}}\subseteq S;$步骤6：为步骤5得到的转移集合E增加表示模态转移的时钟约束c₁，C＝{c₁}；所述的c₁包括模态转移发生时离开源模态的时间c11和到达目标模态的时间c₁₂，将c₁作为每条转移函数的时钟约束，得到转移函数e_j＝(M_is，ep_i，c₁，{c₁}，M_it)，所述c₁获取步骤如下：步骤a：当源模态下线程间的同步属性Synchronized_Component为true，c₁₁＝{T₁中线程周期的最小公倍数}，否则c₁₁＝0；步骤b：当目标模态下线程间的同步属性Synchronized_Component为true，c₁₂＝{T₂中线程周期的最小公倍数}，否则c₁₂＝0；步骤c：得到转移时间记为c₁＝c₁₁+c₁₂；步骤7：重复步骤6，直到E中的所有模态转移中都增加了时钟约束，E＝{e₁，e₂，…，e_k}，得到各个元素都构造完成的时间自动机<∑，S，S₀，C，I，E>，AADL模型到时间自动机模型转换完毕；步骤8：根据步骤7得到的时间自动机模型，使用时间自动机模型的实时系统验证工具UPPAAL验证AADL模型的模态转移是否满足实时性和可达性。