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

摘要

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

说明书

技术领域

本发明涉及一种基于AADL模态时间自动机模型的嵌入式软件测试方法，涉及嵌入式系统软件测试方法。

背景技术

随着嵌入式软件规模的增长，软件开发过程中的各种难题凸显出来，传统的软件开发流程如V模型、W模型已经很难适应当今大规模软件开发的需求。为此，业界提出了模型驱动架构方法(Model Driven Architecture，MDA)，基于该方法构造出来的特定平台的系统模型可以自动化的转换成代码。因此，系统模型成为软件开发过程的关键，如何评估模型的质量自然成为模型驱动架构软件开发的关键。传统的基于代码的软件评估已经不能满足大规模软件的评估需求。基于模型的软件评估正成为一种趋势。在软件模型设计出来以后，对模型的各种功能属性和非功能属性进行评估，能在软件开发的最初阶段发现架构设计中存在的缺陷，及时的修改模型，从而极大地缩短了软件开发的周期和成本。

针对MDA的发展趋势，美国自动化工程师协会(Society of Automotive Engineers，SAE)发布了航空标准AS5506---架构分析与设计语言(Architecture Analysis and Design Language，AADL)，AADL是一种建模语言，它很好地支持了架构模型的设计和复杂实时嵌入式系统的描述。AADL通过构件及构件间的交互对嵌入式系统架构模型进行描述和分析。AADL不关心构件的内部实现，而更注重从软件构件的非功能属性(如安全性、可靠性、实时性等)以及构件间交互去描述一个系统架构。因此，可以通过对AADL模型的分析找出系统设计出现的缺陷，保证嵌入式软件在开发早期发现问题，及时在架构级别对系统进行重构，保证嵌入式系统的可靠性并缩短开发周期和节约开发成本。

AADL对系统操作模态进行了规范，嵌入式系统的执行过程由一系列操作模态组成，每种操作模态下包含多个软件构件或硬件构件以及构件间的交互，当前模态决定被认为是活动的线程集合和可行的传输数据和控制的关联。多模态系统是指包含多种操作模态的应用系统，如巡航控制系统包括初始化模态、正常模态、备份模态以及故障模态等，每一种模态下包含特定功能的系统。系统运行过程中，当检测到某个特定的事件(由外部环境的改变或者控制系统内部的改变引起)时，系统根据模态转换协议初始化一个模态转换，使系统在规定时间内从当前操作模态转换到一个新的操作模态。模态转换导致一些现有任务被删除，一些新的任务被增加以执行新模态相关的一些功能，也有一些任务保持不变。在实时环境中，操作模态转换需要考虑实时性和正确性。实时性指从一个模态转换请求到达到进入一个新模态之间的最大延迟需满足实时嵌入式系统的时间约束。正确性指系统对模态相关的事件的响应符合规格说明。

为了描述多模态构件的分层组合，AADL标准定义了系统操作模态(System Operation Mode，SOM)的概念。一个SOM定义为一个模态容器，容器里的每一个元素都跟一个构件关联。如果一个构件是活动的(active)，它关联的元素赋值为该构件的当前模态。如果一个构件是非活动的(inactive)，它关联的元素值为inactive。一个系统有且只有一个初始SOM。在这个初始SOM中，根构件处于它的初始模态，在根构件处于初始模态时所有那些处于活动状态的构件也处于它们的初始模态，其它构件处于非活动状态。当系统中一个模态转换请求到达时，使能一个SOM转换，通过改变容器内涉及该模态转换的元素的值使系统从旧的SOM转换到新的SOM。在模态转换过程中，新的模态转换请求将会被忽略，直到模态转换完成，系统进入一个新模态后才开始响应新的模态转换请求。

在嵌入式软件开发的过程中，软件测试扮演着重要的角色，伴随着软件开发的始末，以保证嵌入式软件的功能性和非功能性需求。由于AADL是基于构件的嵌入式系统设计语言，对应基于构件的软件测试模型有：马尔科夫链模型、UML模型、状态图模型等。但是这些模型对于基于AADL模型测试的支持较少，同时这些模型在描述系统的时间属性方面比较欠缺，不能满足嵌入式实时系统的测试需求。嵌入式实时系统的实时性和正确性是系统设计首先需要考虑的问题，如果一个嵌入式实时系统的执行不能满足响应实时性和操作正确性，将会导致灾难性的后果。因此，对基于构件的嵌入式实时系统模型的分析和验证成为至关重要的问题，为保证系统模型满足设计需求(实时性和正确性)，需要提出新的基于AADL模型的测试方法。

发明内容

要解决的技术问题

为了避免现有技术的不足之处，本发明提出一种基于AADL模态时间自动机模型的嵌入式软件测试方法，对AADL模型进行测试，保证AADL模型满足设计需求。

本发明的思想在于：根据AADL架构模型文件，生成带有模态信息的AADL系统构件树，通过广度优先遍历构件树，构造AADL模型的时间自动机模型。利用现有的时间自动机的验证工具，对AADL模型模态转换的正确性及时间属性进行验证。

技术方案

一种基于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_tj}，得到表示在事件集合ep_i触发下，模态从M_is转移到模态M_it的每条转移ei＝(M_is，ep_i，_，_，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₁包括模态转移发生时离开源模态的时间c₁₁和到达目标模态的时间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模型的模态转移是否满足实时性和可达性。

有益效果

本发明提出的一种基于AADL模态时间自动机模型的嵌入式软件测试方法，能够在嵌入式软件设计早期阶段对模型实施测试，尽早发现软件模型的正确性和实时性是否满足设计需求，及时修订设计方案，从而缩短了嵌入式实时系统开发的周期并节约了开发成本。

附图说明

图1为本发明方法流程图；

图2为实施实例中AADL模型构件树；

图3为系统模态迁移图；

图4为UPPAAL自动机验证工具；

具体实施方式

现结合实施例、附图对本发明作进一步描述：

该实例描述了控制系统，系统由两个进程构件构成，每个进程构件下包含三个线程构件，每个线程都是周期线程。系统包括5种模态os1、os2、01、02、03、04。系统初始化后进入模态os1，模态os1下包含两种模态01和02。当线程t1和t2的事件端口t1s.e1和t2s.e2接收事件后，触发线程模态从01切换到模态02。在线程t3的数据端口t3s.e3接收到事件后，线程模态由02切换到01。系统模态os2下包含两个模态03和04，进程p1在事件端口p1s.event1接收到事件后触发系统模态从os1转换到模态os2，在模态os2下，线程t4和t5的端口t4s.e4，t5s.e5接收到事件时，从03模态切换到04模态，线程t6的端口t6s.e6在接收到事件后从04模态切换到模态03。下面为该系统的AADL架构模型代码：

thread t1

features

    e1:out event port；

properties

    Dispatch_Protocol＝＞Periodic；

    Period＝＞50ms；

end t1；

thread implementation t1.imp

end t1.imp；

thread t2

features

    e2:out event port；

properties

    Dispatch_Protocol＝＞Periodic；

    Period＝＞50ms；

end t2；

thread implementation t2.imp

end t2.imp；

thread t3

features

    e3:out event port；

properties

    Dispatch_Protocol＝＞Periodic；

    Period＝＞50ms；

end t3；

thread implementation t3.imp

end t3.imp；

thread t4

features

    e4:out event port；

properties

    Dispatch_Protocol＝＞Periodic；

    Period＝＞50ms；

end t4；

thread implementation t4.imp

end t4.imp；

thread t5

features

    e5:out event port；

properties

    Dispatch_Protocol＝＞Periodic；

    Period＝＞50ms；

end t5；

thread implementation t5.imp

end t5.imp；

thread t6

features

    e6:out event port；

properties

    Dispatch_Protocol＝＞Periodic；

    Period＝＞50ms；

end t6；

thread implementation t6.imp

end t6.imp；

process p1

features

    event2:in event port；

end p1；

process implementation p1.imp

subcomponents

    t1s:thread t1 in modes(01)；

    t2s:thread t2 in modes(01)；

    t3s:thread t3 in modes(02)；

modes

    01:initial mode；

    02:mode；

    M12:01-[t1s.e1，t2s.e2]-＞02；

    M21:02-[t3s.e3]-＞01；

end p1.imp；

process p2

features

    event2:out event port；

end p2；

process implementation p2.imp

subcomponents

    t4s:thread t4 in modes(03)；

    t5s:thread t5 in modes(03)；

    t6s:thread t6 in modes(04)；

modes

    03:initial mode；

    04:mode；

    M34:03-[t4s.e4，t5s.e5]-＞04；

    M43:04-[t6s.e6]-＞03；

end p2.imp；

system s1

end s1；

system implementation s1.imp

subcomponents

    p1s:process p1 in modes(os1)；

    p2s:process p2 in modes(os2)；

modes

    os1:initial mode；

    os2:mode；

    os12:os1-[p1s.event1]-＞os2；

    os21:os2-[p2s.event2]-＞os1；

    end s1.imp；

根据步骤1构件AADL架构模型描述文件的构件树，以系统构件作为树的根节点，下一层为子系统构件，依次向下为进程构件、线程构件。每个构件包含该节点的模态信息。如图2所示；

根据步骤2对步骤1得到的构件树进行广度优先遍历，提取每个节点的当前模态存储至时间自动机的S集合中，由于根节点是系统构件，则它的模态向量初始化为空。得到相应的模态向量为SOM₁＝{os1}，SOM₂＝{os2}，SOM₃＝{01}，SOM₄＝{01}，SOM₅＝{02}，SOM₆＝{03}，SOM₇＝{03}，SOM₈＝{04}得到S＝{SOM₁，SOM₂，…，SOM₈}；提取系统的初始模态信息存储在S₀集合中：S₀＝{os1}；

根据步骤3由步骤2得到的模态状态集合S，将S中父节点的模态向量与它的孩子节点的模态向量作笛卡尔乘积，将得到的模态向量继续添加到S中：SOM₉＝{os1，01}，SOM₁₀＝{os1，01}，SOM₁₁＝{os1，02}，SOM₁₂＝{os2，03}，SOM₁₃＝{os2，03}，SOM₁₄＝{os2，04}。则S集合：S＝{SOM₁，SOM₂，…，SOM₁₄}；

根据步骤4由步骤1得到的构件树，再一次对构件树进行广度优先遍历，提取每个节点中引起模态转移的事件，用向量ep_k(k≥1)表示：ep₁＝{p1s.event1}，ep₂＝{p2s.event2}，ep₃＝{t1s.e1，t2s.e2}，ep₄＝{t3s.e3}，ep₅＝{t4s.e4，t5s.e5}，ep₆＝{t6s.e6}，并存储至<∑，S，S₀，C，I，E>中的∑中，得到∑＝{ep₁，ep₂，…，ep₆}；

根据步骤5根据步骤3和步骤4得到的状态集合S和事件集合∑，按照如下的方法构造时间自动机中的转移集合E：

∑＝{(p1s.event1)，(p2s.event2)，(t1s.e1，t2s.e2)，(t3s.e3)，(t4s.e4，t5s.e5)，(t6s.e6)}，

根据得到的事件集合，对于集合中的每个元素找出模态转换的源模态向量和目标模态向量。对于事件集合中的元素ep₁，由于ep₁是引起系统级的模态转换事件，对应的源模态向量为SOM₁，目标模态向量为SOM₂。于是得到一个转移e₁＝(SOM₁，ep₁，_，_，SOM₂)。(“_”为转移函数中还未被定义的元素)

对事件元素ep₂，对应的源模态向量为：SOM₂，目标模态向量为SOM₁，则转移为e₂＝(SOM₂，ep₂，_，_，SOM₁)，依次构造的转移函数为：

e₃＝({SOM₃，SOM₄}，ep₃，_，_，SOM₅)；

e₄＝(SOM₅，ep₄，_，_，{SOM₃，SOM₄})；

e₅＝({SOM₁₂，SOM₁₃}，ep₅，_，_，SOM₁₄)；

e₆＝(SOM₁₄，ep₆，_，_，{SOM₁₂，SOM₁₃})；

根据步骤6为时间自动机增加时间约束的要求，由于线程t1，t2，t3，t4，t5，t6全为周期线程且周期都为50ms，并且t1，t2处于同一个模态和t4，t5处于同一个模态。根据AADL规范，线程t1，t2由模态01转移到模态02的转移时间为t1，t2周期的最小公倍数50ms，线程t4，t5由模态03转移到模态04的转移时间为50ms，其它情况为0ms。所以c₁＝0ms，c₂＝0ms，c₃＝50ms，c₄＝50ms，c₅＝50ms，c₆＝50ms；

根据步骤7重复步骤6，直到E中的所有模态转移中都增加了时钟约束时间：

e₁＝(SOM₁，ep₁，c₁，{c₁}，SOM₂)；

e₂＝(SOM₂，ep₂，c₂，{c₂}，SOM₁)；

e₃＝({SOM₃，SOM₄}，ep₃，c₃，{c₃}，SOM₅)；

e₄＝(SOM₅，ep₄，c₄，{c₄}，{SOM₃，SOM₄})；

e₅＝({SOM₁₂，SOM₁₃}，ep₅，c₅，{c₅}，SOM₁₄)；

e₆＝(SOM₁₄，ep₆，c₆，{c₆}，{SOM₁₂，SOM₁₃})。

最后，E＝{e₁，e₂，…，e₆}。自动机<∑，S，S₀，C，I，E>各个元素都构造完成，AADL模型到时间自动机模型转换完毕；

步骤8：根据步骤7得到的时间自动机模型，使用时间自动机模型的实时系统验证工具UPPAAL验证AADL模型模态转移满足实时性和可达性，如图4所示。