基于模型检查的嵌入式软件构件化分析与验证

聂捷楠

摘 要： 对嵌入式软件构件化进行准确分析与验证，能够为嵌入式系统安全、稳定的运行提供保障。提出一种基于模型检查的嵌入式软件构件化分析与验证方法。设计一种用于检查软件构件的模型，为嵌入式软件构件化分析与验证提供理论基础；将嵌入式软件系统模型用SMV语言的形式表达，利用SMV模型检查工具实现对嵌入式软件运行状态的分析与检验。实验结果表明，该模型能够对嵌入式软件构件化的非功能性方面的设计要求进行准确分析与验证，为嵌入式系统安全稳定的运行提供了保障。

关键词： 模型检查； 嵌入式软件； 构件化； SMV

中图分类号： TN911?34； TP391 文献标识码： A 文章编号： 1004?373X（2016）24?0063?03

Embedded software component analysis and verification based on model checking

NIE Jienan

（Institute of Humanity Information Management， Chengdu Medical College， Chengdu 610500， China）

Abstract： The embedded software component is analyzed and validated accurately， which may provide the safe and stable operation for the embedded system. A analysis and validation method of the embedded software component based on model checking is put forward. A kind of model used to examine the software component is designed， which provides a theoretical foundation for analysis and verification of the embedded software component. The embedded software system model is expressed in the form of SMV language. The SMV model checking tool is used to implement analysis and test of the embedded software running status. The experimental results show that the model can accurately analyze and validate the non?functional design requirements of the embedded software component， and provided the safeguard for the embedded system safe and stable operation.

Keywords： model checking； embedded software； component； SMV

嵌入式系统各种功能的实现都离不开软件[1]，软件具有极其重要的意义[2]，它是影响嵌入式系统稳定运行的关键因素，一旦关键部位中嵌入式系统的软件失效[3]，轻则造成财产损失，重则使生命受到威胁[4]。与PC机中的软件相比，嵌入式系统中的软件既要满足其功能性设计要求[5]，又要满足其非功能性的设计要求，如软件的驱动程度、运算资源的占用程度、对能量的消耗程度等[6]。因此如何对嵌入式系统中的非功能性设计要求进行分析与验证，已经成为当前IT领域中的一个热点研究课题，受到专家学者的广泛关注[7]。

目前，主要的嵌入式系统软件验证方法包括基于马尔科夫的验证方法[8]、基于定理证明的验证方法和基于调试代理软件的验证方法[9]。最常用的是基于马尔科夫的嵌入式软件验证方法。但利用传统方法进行嵌入式系统软件的验证，验证的项目主要为软件的功能性设计要求，并且只能在软件设计的后期才能进行验证，难以对非功能性的设计要求进行准确分析与验证，导致嵌入式软件的稳定性与安全性难以得到保障[10]。

针对传统方法存在的缺陷，提出一种基于模型检查的嵌入式软件构件化分析与验证方法。利用SMV检查工具对嵌入式软件运行状态进行分析与检验，实现对嵌入式软件的分析与验证。仿真实验证明了改进算法在嵌入式软件构件化分析与验证方面的优势。

1 嵌入式软件构件化验证模型设计

对嵌入式系统中的软件进行构件化验证，主要通过重复使用模块化软件来建立嵌入式软件构件化验证的模型，实现对嵌入式系统软件的验证。

通常情况下，一个完整的嵌入式系统软件包括多个子系统软件，其软件系统具有较高的构件化特征。对嵌入式系统中构件化软件进行分析与验证，能够为嵌入式系统安全稳定的运行提供保障。由于分析与验证过程需要消耗大量能量，能量成为嵌入式系统中一种特殊的资源消耗，嵌入式系统的运行时间与能量消耗呈正相关，运行时间越长，能量消耗越多。因此，可以利用能量消耗的时间特性对嵌入式软件构件化的验证过程建模。

设计一种验证模型，在验证模型中加入嵌入式系统主要可以利用资源（包括存储空间、缓冲区、消息队列、传感器）特征向量，使该模型能够反映嵌入式软件构件运行时主要可以利用资源的变化情况。设计验证模型时需要包含如下参数：假设[VP]是资源利用状态的集合，对于每一嵌入式资源利用状态都有[vi∈VP]，且[P]的初始状态为[vi∈VInitP]；[FP]为资源状态的映射集合，[FP=（f1P，f2P，…，fKP）]，其中[K]为嵌入式系统中可利用资源种类的数目；[WP]表示可利用资源的有穷集合，[WP=（VP，FP（VP））]；[ΓP]为资源利用状态的转换集。通过以上参数的描述，将嵌入式软件构件化验证的模型转化为多元组的形式进行构建：

[P=VP?FP?WP?ΓP]

2 嵌入式软件构件化验证方法设计与实现

本文构建立了嵌入式软件构件化验证的模型，将嵌入式软件构件化验证模型中软件运行路径逐一遍历，直到获取正确的软件运行路径，实现模型检查算法设计，最终实现基于模型检查的嵌入式软件构件化分析与验证。

2.1 基于时序逻辑CTL算子的模型检查算法

首先获得嵌入式软件运行过程中的时序逻辑CTL算子，通过CTL算子获取嵌入式软件构件化验证模型中软件运行路径的有关性质，并逐一遍历，直到搜索出正确的软件运行路径，设计了模型检查算法。具体过程如下所述：将时序逻辑CTL划分为分支时间算子和线性时间算子。其中，分支时间算子包括软件的全部运行路径A和特定的运行路径E，线性时间算子包括G（always，经常）、F（sometimes，偶尔）、X（next time，下一时刻）和U（until，直到）。引入上述构建的嵌入式软件构件化验证模型，利用时序逻辑CTL中的分支时间算子和线性时间算子描述嵌入式软件构件化验证模型中软件运行路径的相关性质，如图1所示。图1（a）为[EFg]，表示“资源利用状态的集合[VP]中存在一条运行路径使布尔量公式[g]在某种运行状态下为真”；图1（b）为[AFg]，表示“资源状态的映射集合[FP]中所有运行路径中布尔量公式[g]在某种运行状态下为真”；图1（c）为[EGg]，表示“可利用资源的有穷集合[WP]中存在一条运算路径使得布尔量公式[g]在该路径中的全部状态下都为真”；图1（d）为[AGg]，表示“资源利用状态的转换集[ΓP]中布尔量公式[g]在全部运行路径中的全部状态下都为真”，通过对这些条件进行逐一判定，最终选择正确的软件运行路径，完成模型检查算法设计。

2.2 基于模型检查的嵌入式软件验证的实现

针对嵌入式软件进行分析与验证的模型检查工具主要包括：贝尔实验室开发的SPIN工具、赫尔辛基工业大学开发的PROD工具、CMU大学开发的SMV工具等。每种模型检查工具都有不同的特点，其中，SMV工具结构简单、运算量小、准确率高。因此本文将SMV工具作为嵌入式软件分析与验证的模型检查工具。

SMV工具是根据“符号模型检查”的原理开发，目的是通过对符号模型对软件的性能进行检查，随着SMV工具功能的不断完善，SMV工具已经被广泛应用于软件有限状态的检查。本节将上述模型检查算法利用SMV语言的形式表达，构建SMV模型检查工具，完成嵌入式软件构件化分析与验证，具体步骤如下所述：

一个完整的SMV模型检查工具由两个部分构成，分别为：一个状态转换系统；一个CTL公式组，能够准确描述嵌入式软件的属性。通过这两个部分可以将嵌入式软件的构件化验证过程描述为一个二叉树BDD的形式。SMV模型检查工具只需要对嵌入式软件二叉树BDD的运行状态进行搜索，将搜索结果进行逐一判定，判定后输出的结果分为：正确和错误，即为模型检查算法对嵌入式软件构件化的验证结果，实现了嵌入式软件的构件化验证。

2.3 部分代码设计

利用SMV模型检查工具对嵌入式系统的构件化进行验证与分析，部分程序如下所述：

MODULE main

VAR

Pen_irq；booleam；

D_jitery_delay；boolean；

U_jittery_delay；boolean；

Detect：touch_Detect（pen_irq，d_jittery_delay，u_jittery_delay）；

SPEC

AG（detect，state=Touch_up&pen_irq=0?>AF detect，state=Touch_Down）

SPEC

AG（detect，state=Touch_Down&pen_irq?>AF detect，state=Touch_up）

MODULE Touch_Detect（pen_irq，d_jittery_delay，u_jittery_delay）

state：{ Touch_Idle，Touch_up，Touch_down，Touch_ChkUp；Touch_chkDown；}

3 实验结果及分析

3.1 实验环境设置

为了验证改进算法在嵌入式软件构件化验证方面的有效性，需要进行仿真实验。嵌入式软件构件化分析与验证的运行环境为：Windows 7操作系统，利用Rational Rose 2003生成 MDL文件；以嵌入式软件的非功能性设计要求为依据，对改进算法和传统算法的性能进行比较。研究表明，资源的占用程度、投影路径中非法信息检验、能耗行为的路径是嵌入式软件构件化的具体属性，本文以手持PDA为例，以这三个属性为目标，对手持PDA软件进行构件化验证。

3.2 不同算法下仿真实验结果及分析

首先利用上述获得的SMV模型检查工具对PDA的通信的驱动程序和信息交互序列的驱动程序运行资源的占用情况进行检验。这两种驱动程序包含三类资源，分别为r1，r2和r3，软件在进行状态转换过程中需要占用的资源数量和资源种类利用向量进行描述，例如，

3.2.1 不同算法下嵌入式软件运行资源的占用情况验证

首先利用不同算法对手持PDA软件进行资源的占用情况方面验证，以验证软件在状态转换的过程中需要占用的资源是否满足设计要求。利用传统算法进行验证结果表明：传统算法只能检测出软件在状态转换的过程中需要占用的资源种类为3种，但不能检测出具体的资源名称和占用资源的数量；而利用改进算法进行验证结果表明：手持PDA通信的驱动程序在进行转换的过程中有一个资源处于非法状态，即（s4|s1），该程序在进行状态转换的过程中需要的资源为[r1，2]，[r2，5]，[r3，3]。（s4|s1）状态在转换的过程中对资源r2的需求量为5，而在实际程序中r2的资源总的数量为4，因此可推出该状态在转换的过程中有1个资源不符合设计要求，体现了改进算法的巨大优势。

3.2.2 不同算法下嵌入式软件运行中投影路径中非法

信息检验验证

为了进一步验证改进算法的有效性，本文以PDA中信息交互序列的驱动程序为例，对信息交互过程中投影路径中的非法信息进行检验。结果表明，利用传统算法进行投影路径中非法信息检验，没有搜索出对应的投影路径中存在的非法信息；而改进算法结果表明：PDA在进行信息交互的过程中，在组合状态空间内存在一个与信息交互行为相对应的投影路径，但是该路径存在一个非法状态（s2|s1），占用资源[r2，r3]，表明在此信息交互行为的状态下，嵌入式软件系统不满足设定的资源限制条件，需要PDA软件的编写者对软件进行及时修改，以保证嵌入式软件的安全性。嵌入式软件的非法信息验证界面如图2所示。

3.2.3 不同算法下嵌入式软件运行中能耗行为的路径

比对验证

在PDA中，为了对比不同算法在嵌入式软件能耗行为的路径方面的验证性能。利用不同算法对PDA非功能性的能耗行为的路径进行检验。首先搜索出满足非功能性行为的路径共19条。然后利用不同算法对这19条路径消耗的能耗进行对比。

实验结果为：实际情况下所有有路径中最大能量为44.6，对应的投影路径为s0|s0（0，0）2.9→s1|s1（0，0）5.5→s2|s1（0，2）4.1→s3|s1（0，4）5.4→s4|s1（0，7）5.6→s5|s1（0，9）4.8，改进算法下所有路径中最大能量为46.3，对应的投影路径为s0|s0（0，0）2.9→s1|s1（0，0）5.5→s2|s1（0，2）4.1→s3|s1（0，4）5.4→s4|s1（0，7）5.6→s5|s1（0，9）4.8；传统算法下最大能量为29.7，对应的投影路径为s0|s0（0，0）2.8→s1|s1（0，0）5.5→s2|s1（0，1）4.0→s3|s1（0，3）5.3→s4|s1（0，5）5.3→s5|s1（0，9）4.7。通过仿真实验表明，传统算法与实际的能耗值相差较大，并且对应的投影路径不一致；而改进算法与实际的能耗最为接近，并且对应的投影路径一致，充分体现了改进算法在嵌入式软件能耗行为的路径设计验证方面的优越性。

4 结 语

针对传统算法存在的缺陷，提出一种基于模型检查的嵌入式软件构件化分析与验证方法。利用SMV检查工具对嵌入式软件运行状态进行分析与检验，实现对嵌入式软件的分析与验证。仿真表明，改进算法能够对嵌入式软件构件化的非功能性方面的设计要求进行准确分析与验证，为嵌入式系统安全稳定的运行提供了保障。

参考文献

[1] 王锋，张弛.构件化嵌入式软件设计模型验证工具的研究[J].通讯世界，2014（21）：36.

[2] 王博，白晓颖，贺飞.可组合嵌入式软件建模与验证技术研究综述[J].软件学报，2014，25（2）：234?253.

[3] 符宁，杜承烈，李建良，等.AADL分级调度模型的分析与验证[J].计算机研究与发展，2015，52（1）：167?176.

[4] 胡宁，叶宏.嵌入式操作系统的形式化验证方法[J].航空计算技术，2015（2）：96?100.

[5] 白海洋，李静，赵娜.基于时间自动机的嵌入式软件模型可调度性验证[J].计算机工程与科学，2013，35（3）：121?127.

[6] 赵竞雄.嵌入式系统威胁与风险评估过程仿真分析[J].计算机仿真，2014，31（4）：295?298.

[7] 黄传林，黄志球，胡军，等.基于扩展SysML活动图的嵌入式系统设计安全性验证方法研究[J].小型微型计算机系统，2015（3）：408?417.

[8] 谢开斌，陈海明，崔莉.物联网软件体系结构中的感执模型的求精[J].软件学报，2014，25（8）：1659?1670.

[9] 王诚.硬件构件化的嵌入式底层构件开发技术分析[J].中国科技博览，2013（9）：134.

[10] 黄菲.嵌入式实时软件的构件化开发技术探究[J].信息技术与信息化，2015（10）：197?198.