基于使用场景的时间扩展EFSM建模与完整性验证①

刘卓媛, 尤 枫, 赵瑞莲, 尚 颖

(北京化工大学 信息科学与技术学院, 北京 100029)

1 引言

当前, 随着嵌入式实时软件在高科技领域(尤其是在航空, 航天和现代武器制造等许多关键领域)的日益增长的应用, 人们更加关注嵌入式实时操作系统的可靠性[1]. 软件测试是保证软件质量和可靠性的主要手段, 针对实时嵌入式软件有着不同的测试方法, 其中基于模型的软件测试技术由于测试效率高, 并且能够发现其他测试技术难以发现的故障[2], 常被应用于该类软件的测试.

实时嵌入式软件不仅具有实时性特征, 而且往往全部或部分表现出基于状态的行为[3], 因此针对该类软件的建模需支持事件驱动、状态转移描述、复杂动态交互行为和严格的时间限制等领域特征[4]. 近年来, 在实时嵌入式软件的测试中最常用的模型有FSM、UML、EFSM等. 其中, EFSM模型由于能同时描述被测软件的控制流和数据流信息, 更精确地描述软件系统的动态行为[5], 常被用于软件测试中. 然而, 目前针对该类软件的基于模型的软件测试方法仍然存在以下问题:(1)不能完全满足该类软件在建模及测试中对实时性的要求； (2)软件通常非常复杂, 而目前大多数研究都是通过分析需求或功能类的文档去构建模型, 通常需要丰富的专业领域知识, 才能构建相对准确和完整的模型, 从而导致建模工作的成本和难度都比较高.

为了解决以上两大问题, 在基于模型的软件测试的研究中, 时间自动机[6,7]在FSM模型上为迁移添加了时钟约束, 为状态添加了不变式约束, 以此来描述实时嵌入式软件的时间特征. 但是, 该模型缺乏对嵌入式软件行为信息的描述. Yin等人基于EFSM模型提出了RT-EFSM (Real-Time Extended Finite State Machine model)[8,9]模型扩展了EFSM模型中状态转换过程中对时间特征的描述, 能够有效表征嵌入式软件的实时特性, 但是在建模时需要对功能和需求文档深入分析,建模成本较高.

而文献[10]从用户的角度描述软件的系统行为,通过记录用户使用软件过程中与软件交互的场景实例,来描述软件的主要功能、使用方式以及边界条件等主要信息[11], 因此基于使用场景构建模型既可以相对细致的描述软件的行为特征, 又不需要考虑软件内部的逻辑结构和特性, 很大程度降低了建模的难度. 在 Wang等人的工作中[12]利用动态分析获取用户与Web应用程序之间的交互信息, 将其表征为用户行为轨迹(trace)并映射到EFSM模型中, 有效实现了面向Web应用程序的EFSM模型的构建. 因此本文将基于使用场景构建实时嵌入式软件的RT-EFSM模型.

但是, 场景难以覆盖系统部件实例之间的所有交互[13],特别是需要复杂的交互才能探究的软件系统行为. 因此,基于使用场景构建的模型大多是不完整的. 为了验证模型的完整性, 严亚伟等人[14]主要针对系统的数据完整性进行分析和验证. 针对数据完整性的定量评估问题,提出使用概率计算树逻辑(PCTL)和马尔可夫决策过程(MDP)分别对完整性进行形式化的定义和评估, 实现了对完整性的定量验证, 为系统开发中的完整性需求提供支持. 文献[15]提出事件及其执行条件可以代表Web应用程序的行为, 依据事件和JS分支覆盖为Web应用程序EFSM模型定义了完整性准则, 对模型的完整性进行评估, 并提出了面向Web应用的EFSM模型自动补全方法, 提高了模型的完整性.

综上, 本文将场景表征为形式化的Scene, 并从中识别出构建RT-EFSM模型的状态和迁移, 利用状态和迁移的等价性有效合并状态和迁移并确定迁移中变量条件的上下界, 从而构建RT-EFSM模型. 而对于实时嵌入式软件, 在同一触发事件的不同条件下, 会导致系统的状态、参数以及后续操作发生不同的变化. 因此该类软件的动态行为涉及用户使用该软件时触发的事件、触发事件时的条件、触发事件后发生改变的系统状态、参数及后续操作. 由于事件和相应的执行条件共同决定了系统到达的状态和后续操作, 因此它们代表了该类软件的系统行为, 从而事件及条件的完整性决定了系统行为模型的完整性. 由于RT-EFSM模型中的迁移条件包括时钟条件和非时钟条件, 因此, 本文主要根据时钟变量条件及非时钟变量条件来设计模型完整性准则来验证模型的完整性, 并利用时钟变量条件在时间轴[9]上的连续性以及非时钟变量条件的对立分支条件生成待补全迁移, 然后在模型上搜索可行的迁移序列以遍历它们, 通过执行生成的迁移序列, 将待补全迁移添加到模型中, 从而提高模型的完整性.

本文的主要贡献概括如下:

(1)本文基于使用场景Scene自动化构建RT-EFSM模型；

(2)本文定义了时钟变量和非时钟变量完整性准则来评估嵌入式软件的RT-EFSM模型的完整性；

(3)针对RT-EFSM模型, 提出了模型的待补全迁移生成策略生成待补全迁移, 并利用模型补全方法将其添加到模型中；

(4)本文以4个实时嵌入式系统为实验对象进行一系列实验来验证所提方法的有效性.

2 基于使用场景的时间扩展EFSM构建与完整性验证方法

2.1 方法整体框架

本文基于实时嵌入式软件的使用场景对软件的动态行为进行建模, 并对模型进行完整性评估及补全, 以保证模型的完整性及后续测试的有效性. 基于使用场景的时间扩展EFSM构建与完整性验证的方法框架如图1所示, 主要包括: (1)基于使用场景构建RT-EFSM模型； (2)设计完整性评估准则并对RT-EFSM模型进行完整性验证； (3)模型补全. 对于不完整的模型, 设计待补全迁移生成策略生成待补全迁移, 并使用模型补全方法将待补全的迁移添加到模型中, 从而提高模型的完整性.

图1 基于使用场景的RT-EFSM构建与完整性验证方法框架

2.2 基于使用场景的RT-EFSM模型构建

(1)使用场景的规范化表示

使用场景主要记录了用户与系统进行交互时所执行的一系列行为活动, 是用例的一个实例, 反映了系统的性能和运行方式[10]. 使用场景一般用自然语言进行描述, 为了自动化地构建RT-EFSM模型, 需要对使用场景进行规范化表示, 本文将其定义为Scene.

定义1. 使用场景(Scene): 一条Scene可以表示为Scene=＜IA0,…,IAj,…,IAn-1＞, 代表用户与实时嵌入式系统软件进行的一系列交互.

EScene中的任一交互IAj表示为＜Source,Event,Cond[Vcond,Ccond],Action,Target＞, 其中Source和Target分别表示系统软件在事件触发前后所处的状态,用一个二元组＜Label,StateName＞表示,Label表示状态标号,StateName表示状态名称；Event表示用户执行的操作, 即触发事件；Cond表示触发事件时系统软件所满足的条件,Vcond和Ccond分别表示事件发生时所满足的变量约束条件和时间约束条件,Action表示系统软件在事件触发后执行的响应及引起参数更改的后续操作.

(2)Scene中的RT-EFSM状态与迁移识别

为了构建RT-EFSM模型, 需从规范化的Scene集合中识别模型的状态和迁移. 根据RT-EFSM模型的定义[9], 模型的状态集合可表示为S={s0, …,sj, …,sn}, 其中的每一个状态sj=＜Label,StateName＞,Label和StateName分别表示状态的标号和名称； 迁移集合T={t0,…,tj,…,tn}表示允许模型从一个状态迁移到另一个状态的交互信息集合, 集合中的任一迁移表示为tj=＜Head(tj),Event(tj),Cond(tj),Action(tj),Tail(tj)＞. 因此,Scene中的任一交互IAj可视为模型中的迁移tj,IAj中的Source与Target可分别对应tj的Head(tj)与Tail(tj), ＜Event,Cond[Vcond,Ccond],Action＞对应于tj中的＜Event(tj),Cond(tj),Action(tj)＞. 从而当遍历完Scene集合中的每一条Scene时, 可获得RT-EFSM模型的状态列表S和迁移列表T.

(3)基于使用场景的RT-EFSM模型构建

根据上节分析, 根据Scene集合可获取RT-EFSM模型的状态列表S和迁移列表T. 但是由于用户与系统可能存在多次重复的交互, 所以收集的Scene集合中的Scene之间可能存在相同的交互信息, 从而导致获取的状态列表和迁移列表中可能会包含相同的状态或迁移.因此, 合并状态和迁移是构建RT-EFSM模型的关键.

根据对Scene集合的进一步分析, 由于嵌入式软件的实时性, 用户的某些操作必须在特定的时间内完成, 但是每一条Scene记录的只是在某一时间点用户与系统软件的交互信息. 因此, 在一定的时间范围内,用户触发相同的事件后系统软件的状态变化和相应的响应是相同的； 而超过了某一时间点时, 即使触发相同的事件, 却会导致系统软件的状态和响应不同. 而这种实时性表征为迁移tj中的时钟变量等式的不同取值.因此迁移的合并过程中需要根据时钟变量的值集确定时间约束, 即迁移的合并可能涉及时钟约束的派生.

同样, 对于系统软件有次数限制的操作, 用户与系统软件进行交互的次数最终表征为模型迁移tj中计数器变量[16]等式的不同取值, 因此迁移的合并过程中需要根据计数器变量的值集确定计数器变量约束, 即迁移的合并可能涉及非时钟变量约束的派生.

为了有效合并迁移列表T并确定迁移的时钟约束和非时钟约束, 本文提出了等价迁移和弱等价迁移概念, 其定义如下:

定义2. 等价迁移: 给定迁移t1=＜Head(t1),lbl(t1),Tail(t1)＞和t2=＜Head(t2),lbl(t2),Tail(t2)＞, 其中标签lbl(t)=＜Event(t),Cond(t),Action(t)＞,Cond(t)=[VC,TC], 当且仅当Head(t1)=Head(t2),lb(t1)=lb(t2), 且Tail(t1)=Tail(t2)时,t1与t2等价.

定义3. 弱等价迁移: 给定迁移t1=＜Head(t1),lbl(t1),Tail(t1)＞和t2=＜Head(t2),lbl(t2),Tail(t2)＞, 其中标签lbl(t)=＜Event(t),Cond(t),Action(t)＞,Cond(t)=[VC,TC],当且仅当Head(t1)=Head(t2),lbl(t1)～lbl(t2),且Tail(t1)=Tail(t2)时,t1与t2弱等价. 其中lbl(t1)～lbl(t2)表示标签信息中除Cond(t1)中的时钟变量和计数器变量与Cond(t2)中对应的同一变量的取值不同外, 其余各个组成部分均相等.

根据等价迁移和弱等价迁移的定义, 遍历迁移列表T, 识别出其中的等价迁移及弱等价迁移, 并对这两种迁移进行合并. 在弱等价迁移的合并过程中, 能够派生出迁移的时间约束及计数器变量约束. 其派生过程如下: 遍历由多个互为弱等价迁移组成的弱等价迁移列表, 抽取其中的时钟变量和计数器变量及其取值, 获得＜var,valueSet＞对, 其中var代表某一变量,valueSet代表该变量的值集. 对于变量var确定其值集valueSet的最小边界值MIN和最大边界值MAX, 从而派生出变量var满足的约束为: MIN≤var≤MAX. 当确定时间约束及计数器变量约束后, 将弱等价迁移列表中的每一条迁移tj上的时钟变量及计数器变量等式修改为派生的时间约束和计数器变量约束, 从而将弱等价迁移列表变为等价迁移列表, 实现了弱等价迁移的合并.

为了实现基于使用场景构建RT-EFSM模型, 设计了算法1, 从使用场景中识别模型的状态和迁移, 并合并等价状态和迁移, 最终得到RT-EFSM模型.

算法1. RT-EFSM模型构建算法1) 将使用场景表示为规范化的Scene, 获得场景的Scene集合；2) 识别Scene集合中RT-EFSM的状态及迁移, 获得其状态列表S及迁移列表T；3) 采用距离公式(本文采用编辑距离)对状态列表S中的任意两个状态的状态名称进行字符串比较, 判断两个状态节点是否为同一状态. 若相同, 则删除状态标号较大的状态, 获得无相同状态的状态集合S′, 并修订迁移列表中的相应状态, 获得新的迁移列表T′；

4) 遍历迁移列表T′中的迁移, 将迁移列表T′中当前迁移t与列表中后面的迁移的各个组成部分一一比较, 如果存在互为弱等价或互为等价的迁移, 则将它们加入到迁移列表T1′中, 如果不存在, 则将添加到T′′中；5) 合并迁移列表T1′中的迁移将其变为等价迁移列表T1′′, 保留T1′′中的其中一条迁移添加到迁移T′′, 实现等价迁移的合并, 返回第4)步.6) 最终获得状态集合S′以及迁移集合T′′, 即RT-EFSM模型.

2.3 基于使用场景构建的RT-EFSM模型完整性验证

(1)模型完整性准则

由于使用场景Scene难以涵盖应用系统的所有行为, 因此很难保证基于Scene构建的RT-EFSM的模型的完整性. 由于事件及其执行条件的完整性决定了系统行为模型的完整性, 因此,本文基于RT-EFSM模型迁移t上的条件Cond(t)中的时间约束以及变量约束条件考虑模型的完整性, 提出了模型完整性评估准则.

定义4. 时间约束对立迁移: 给定迁移t1=＜Head(t1),lbl(t1),Tail(t1)＞,t2=＜Head(t2),lbl(t2),Tail(t2)＞, 其中标签lbl(t)=＜Event(t),Cond(t),Action(t)＞,Cond(t)=[VC,TC], 如果Head(t1)=Head(t2),Tail(t1)!=Tail(t2),lb1(t)中的触发事件Event(t)相同, 且Cond(t1)与Cond(t2)中的同一时钟变量c的时间约束不同, 那么称t1和t2为时钟变量c的时间约束对立迁移.

根据如上定义, 互为时间约束对立迁移的多个迁移组成时钟变量c的时间约束对立迁移集TRc.

定义5. 时区[9]: 设RT-EFSM模型中实时嵌入式软件中状态转换时钟集合为L, 则L的取值范围为[0,+∞). 分布在L时间轴上的时间点L1,L2,…,Lk(L1＜L2＜…＜Lk)将时钟集合L划分为k+1个子区域, 其中每一个子区域称为一个时区.

根据如上定义以及图2的时区划分可知, 对于时间约束L1＜ω1＜L2和L2≤ω2＜L3, 分布在时钟集合L时间轴上的时区是连续的.

图2 时区划分

定义6. 变量约束对立迁移: 给定迁移t1=＜Head(t1),lbl(t1),Tail(t1)＞,t2=＜Head(t2),lbl(t2),Tail(t2)＞, 其中标签lbl(t)=＜Event(t),Cond(t),Action(t)＞,Cond(t)=[VC,TC], 如果Head(t1)=Head(t2),Tail(t1)!=Tail(t2),lb1(t)中的触发事件Event(t)相同, 且Cond(t1)与Cond(t2)中的同一非时钟变量v的约束相反, 那么称t1和t2为变量v的变量约束对立迁移.

根据上述定义, 本文提出的时间约束完整性准则以及变量约束完整性准则定义如下:

定义7. 时间约束完整性准则: 假设RT-EFSM模型上的迁移集合为T={t1,t2,…,tj,…,tn}(n＞0), 对于任意一条迁移tj, 如果tj上的任意时钟变量c存在时间约束对立迁移集TRc, 并且TRc中c的所有时间约束分布在时钟集合L时间轴上的时区是连续的, 则称该模型满足时间约束完整性准则.

定义8. 变量约束完整性准则: 假设RT-EFSM模型上的迁移集合为T={t1,t2,…,tj,…,tn}(n＞0), 对于任意一条迁移tj, 如果tj上的任意非时钟变量v存在变量约束对立迁移, 则称该模型满足变量约束完整性准则.

根据以上两种准则, 通过对已构建的RT-EFSM模型的迁移进行静态分析并进行完整性验证. 通过静态分析获得造成模型不完整的时间约束或变量约束及其所在的迁移, 根据这些信息对模型进行补全.

(2)待补全迁移生成

对于不完整的模型, 其时间约束的时区分布不连续或者变量约束的对立约束不存在, 即模型没有表征在不连续的时区范围内或变量约束的对立约束下软件的动态行为. 因此, 本文提出了最近邻时间约束迁移生成策略以及对立变量约束迁移生成策略, 生成待补全迁移并将其补充到RT-EFSM模型中.

① 最近邻时间约束迁移生成策略

假设造成RT-EFSM模型不完整的时间约束为p0≤c≤p1, 其所在的迁移为t, 则可以根据时钟变量c的时间约束对立迁移集TR获得该变量的时间约束在时钟集合L时间轴上的时区分布, 从而得到与迁移t的时间约束分布最近邻的时区及其所在迁移[p2,p3](t1),[p4,p5](t2)(其中p3＜p0,p1＜p4), 由于模型缺少对处于不连续时区(p3,p0)∪(p1,p4)中的时间点的软件行为进行表征. 因此待补全迁移表征在当前时区的最近邻时区表示的时间约束下, 触发相同的事件并满足相同的变量约束条件时, 系统可能的动态行为. 因此设待补全迁移的时间约束为p3＜c＜p0,p1＜c＜p4,构造的待补全迁移如式(1)所示:

② 对立变量约束迁移生成策略

假设造成RT-EFSM模型不完整的非时钟变量v的约束为VC, 其所在的迁移为t, 构造的待补全迁移表征为当该迁移的变量约束与迁移t的变量约束VC相反时, 在相同的源状态下, 触发相同的事件并满足相同的时钟约束条件, 系统可能的动态行为. 因此构造的待补全的迁移如式(2)所示:

根据这两个迁移补全策略, 生成了待补全的迁移列表Tf. 为了提高模型的完整性, 需要将其添加到RTEFSM模型中.

(3) RT-EFSM模型补全

为了将生成的待补全迁移列表Tf中的迁移添加到模型中, 需要识别其后续状态和操作[15], 并通过动态执行可行迁移序列来遍历待补全迁移. 即模型补全方法如下: 对于Tf= {t0,…,tj,…,tn} (n＞0)中的每一条迁移tj,找到该迁移的源节点在原模型中的位置, 以该迁移作为初始迁移, 通过前向搜索生成可行迁移序列[16], 并利用GA算法找到触发该序列的输入数据[17], 使迁移序列与迁移数据共同构成可执行路径. 并将可执行路径作为具体的测试实例, 对其进行动态执行, 从执行结果中识别待补全迁移触发的状态和后续操作.

如果触发状态与所建立的RT-EFSM模型中某一状态相同, 即它们的状态名称相同, 则将该状态作为补全迁移的目标状态. 否则, 触发状态为新状态, 则将此状态添加到RT-EFSM模型的状态集合S中, 并将补全迁移的目标状态设置为新状态.

综上, 模型完整性验证与补全算法如算法2所示.

算法2. RT-EFSM模型完整性验证与补全算法1) 遍历模型的迁移及迁移上的时钟约束和变量约束, 获取模型迁移上的时钟约束对立迁移TR； 获取模型迁移上未找到变量约束对立迁移的迁移集CR.

2) 根据TR与CR以及待补全迁移生成策略生成待补全迁移集Tf.3) 对于Tf中的每一条迁移tj, 判断是否能够在RT-EFSM模型中找到一条可执行迁移路径来触发tj, 如果能找到, 则将该迁移补全到模型中, 否则将该待补全迁移tj放置在Tf 的最后, 考虑另一个待补全迁移.4) 如果Tf中所有待补全迁移拥有其相应的可执行迁移序列, 或者达到了时间预算, 那么模型补全就终止了.

3 实验分析

3.1 实验设计

(1)研究问题

为了验证本文所提方法的有效性, 实验部分主要解决以下两个主要问题:

研究问题1: 基于使用场景构建RT-EFSM模型的方法是否有效? 该方法的时间效率如何?

研究问题2: 本文提出的待补全迁移生成策略是否有效?

(2)实验对象

本文将4个实时嵌入式系统作为实验对象, 包括ATM 机、三层楼的综合电梯系统、简易飞行安全系统及飞机发动机控制软件. 表1为4个嵌入式系统的使用场景的详细信息, 包括实时系统名称、使用场景总数、Scene列表中包含的交互总数、状态总数、事件总数.

表1 嵌入式系统的使用场景信息

(3)评估指标

① 由于用户与实时嵌入式系统的交互是通过事件实现的, 事件及其执行条件导致系统的不同响应. 而使用场景记录了用户与系统进行交互时所执行的一系列行为活动, 是用例的一个实例. 可以看出, 软件的系统行为与事件及使用场景密切相关. 因此, 为了验证建模方法的有效性, 即生成的模型是否将使用场景Scene集合中包含的信息完整表征出来, 该信息不仅包括每一次用户与系统软件进行交互的信息, 还包括使用场景所表示的可行执行序列. 因此, 本文提出了事件覆盖率(Event Coverage,EC)和场景覆盖率(Scene Coverage,SC)两个度量指标来衡量本文提出的模型构建方法的有效性.

事件覆盖率(Event Coverage,EC),EC衡量RT-EFSM模型中出现的事件占Scene集合中的所有事件的比例:

其中, |RT.Event|表示生成的RT-EFSM模型中包含的事件数, |S.scene|表示在Scene集合中的总事件数.

场景覆盖率(Scene Coverage,SC),SC表示Scene集合中能够被基于RT-EFSM模型生成的可执行测试路径覆盖的Scene条数占总Scene条数的比例:

其中, |RT.scene|表示被基于RT-EFSM模型生成的测试路径覆盖的Scene条数, |S.scene|表示在Scene集合中的总Scene条数.

② 本文的模型补全方法认为, 待补全迁移成功添加到模型中的标准是通过对模型的动态执行生成可行迁移序列来遍历待补全迁移. 即在模型中能够找到一条从初始节点开始到待补全迁移的可执行序列并生成可执行测试路径. 因此, 为了评估待补全迁移生成策略的有效性, 即根据该策略生成的待补全迁移能够成功添加到模型中, 本文提出了待补全迁移可行率(for Complete Transition Feasibility,fCTF)的评估指标.

待补全迁移可行率(for Complete Transition Feasibility,fCTF)表示待补全迁移列表中能够被在原RTEFSM模型中动态模拟执行生成的可执行测试路径触发的待补全迁移条数占待补全迁移总数的比例:

其中, |Executable Paths Number|表示能够被基于RTEFSM模型生成的可执行测试路径触发的待补全迁移条数, |forComplete Transition Number|表示待补全迁移列表中的待补全迁移总数.

3.2 实验结果与分析

对研究问题1, 根据4个实时嵌入式系统的Scene集合构建其RT-EFSM模型. 如图3所示是根据ATM系统的使用场景Scene集合构建的RT-EFSM模型. 该模型中的节点代表模型的状态, 其中同心圆节点代表模型的初始节点, 边代表模型的迁移, 由模型的一个状态节点指向另一个节点. 例如图中的S0代表模型的初始节点, T1表示模型的一个迁移.

图3 ATM系统的RT-EFSM模型

表2显示了ATM系统的RT-EFSM模型的迁移信息, 包括迁移的源节点Head(t), 目标节点Tail(t),触发事件Event(t), 迁移转换条件Cond(t), 以及系统响应及操作Action(t). 通过本文的模型构建方法, 可以将从初始Scene集合中包含了198个状态和157个迁移,在合并相同的状态和迁移之后, 状态和迁移分别减少为5和19, 其中的一个状态表示ATM系统的一个功能页面, 例如S0表示“输入密码页面”, 实现了状态、迁移的有效合并.

表2 ATM系统RT-EFSM模型迁移信息

如表3所示统计了使用本文提出的建模方法构建的4个系统的RT-EFSM模型的相关信息及时间效率,包括系统名称、模型的状态数量、迁移数量、事件覆盖率(EC)、场景覆盖率(SC)以及建模的时间开销.

表3 模型构建的结果及时间效率分析

结合表1和表3可以看出, 本文的建模方法可以有效缩减模型的状态和迁移数, 例如三层楼的综合电梯系统的Scene集合中包含的状态数和迁移数分别为118和100, 而所建的RT-EFSM模型中状态和迁移数减少到5和25； 简易飞行安全系统的Scene集合中包含的状态数和迁移数分别为297和261, 所建模型中的状态和迁移分别减少到5和34. 除了状态及迁移的数量外, 我们利用两个衡量指标, 即事件覆盖率(EC)和场景覆盖率(SC)来度量各模型的覆盖情况, 以验证模型构建方法的有效性. 如表3的实验结果所示, 利用Scene构建的模型的EC和SC均为100%. 即本文提出的建模方法可以保留Scene集合中的所有事件和场景表示的执行序列信息. 此外, 针对4个实时嵌入式系统,模型构建的最大时间开销是0.5070 s, 时间成本是可以接受的.

综上, 本文提出的模型构建方法可以有效合并Scene集合中的相同状态和迁移, 同时保证了RT-EFSM模型对实时嵌入式软件动态行为的覆盖且时间开销较小.因此, 基于使用场景构建RT-EFSM的方法可以有效建立实时嵌入式软件的行为模型.

对于研究问题2, 为了评价本文提出的待补全生成策略的有效性, 本文统计了根据待补全迁移生成策略生成的待补全迁移数量、能够被基于RT-EFSM模型生成的可执行测试路径触发的待补全迁移条数(EPN),以及待补全迁移可行率 (fCTF)和不可行率(nfCTF), 其中不可行率nfCTF=1-fCTF.

由表4所示可以看出, 根据本文提出的待补全迁移生成策略可以生成待补全迁移, 例如该策略为ATM系统生成的待补全迁移数为16, 能够被基于模型生成的可执行测试路径触发的待补全迁移条数为15. 为三层楼的综合电梯系统生成了10个待补全迁移, 其中有7条待补全迁移能够被基于模型生成的可执行测试路径触发. 另一方面, 通过fCTF和nfCTF两个指标评估待补全迁移生成策略的有效性. 例如, 简易飞行安全系统的待补全迁移可行率为86.67%, 不可行迁移可行率为13.33%. 飞机发动机控制软件的待补全迁移可行率为78.57%, 不可行迁移可行率为21.43%. 其中fCTF最低为70.00%,nfCTF最高为30.00%, 并且各个实时系统的待补全迁移可行率都远远高于其不可行率, 从而说明本文提出的待补全迁移策略能够生成待补全的迁移, 并且生成的待补全迁移的可行率较高, 即待补全迁移能够有效补全到模型中.

表4 待补全迁移策略的有效性分析

4 结论与展望

本文提出了一种基于使用场景自动构建RT-EFSM模型的方法, 设计了模型完整性验证的准则, 并通过该准则验证模型的完整性. 针对不完整的模型, 利用待补全迁移生成策略生成待补全的迁移, 并利用模型补全算法将其填补到模型中. 本文完成了4个实时系统模型的构建与完整性验证, 实验表明本文提出的自动建模方法可以将用户使用场景集中的冗余状态和迁移进行有效的合并, 花费的时间开销较小. 并且根据待补全迁移策略生成的待补全迁移能够有效补全到模型中,从而提高了模型的完整性. 在后续工作中, 将扩大实验规模, 并进一步优化补全模型的方法和策略, 从而提高本文方法的有效性.