一种基于模型检查的嵌入式软件验证方法

嵌入式软件广泛应用于不同领域，如消费电子、工业控制、汽车电子、移动通信等。嵌入式软件的可靠性保证十分关键。嵌入式软件中常见的错误包括状态机错误、时序错误、栈溢出／存储溢出等，在开发过程中对嵌入式软件进行验证十分重要。

对嵌入式软件的验证一般依赖于形式化的方法。

形式化的方法可以对嵌入式软件系统进行严格的规约，并可以对系统进行不同视角的验证。验证主要是分析系统是否具有期望的性质。常见的验证技术主要有模型检查和定理证明。模型检查自动化程度高，并且当系统不具有期望性质时能给出反例，但它存在状态爆炸问题。定理证明能基于无穷状态空间分析，但是自动化程度不高，需要人工干预，并且在证明失败后不能给出易于理解的反例。本文使用符号模型检查技术来验证嵌入式软件系统，并通过触摸屏检测算法来说明该方法的应用。

1 模型检查

模型检查是一种验证有限状态系统的自动化技术，使用时序逻辑来描述系统性质。本文使用时序逻辑CTL来描述嵌入式系统满足的性质。CTL有分支时间和线性时间2种算子，其中分支时间算子是指路径量词A("对所有计算路径")和E("对某些计算路径")，线性时间算子包括G("always"，总是)、F("somet：imes"，有时)、X("next-time"，下一时刻)和U("until"，直到)。其中线性时间算子G、F、X和U之前必须有1个路径量词。如图1所示，CTL公式用于描述有限状态系统上计算路径的相关性质。图1(a)表示EFg，即"存在一条计算路径，在某个状态，布尔量公式g为真"；图1(b)表示AFg，即"对所有计算路径，在每个计算路径的某个状态，布尔量公式g为真"；图1(c)表示EG，即"存在一条计算路径，在此路径的所有状态，布尔量公式g为真"；图1(d)表示AG，即"在所有计算路径的所有状态，布尔量公式g都为真"。

2 模型检查工具SMV

常见的模型检查工具有贝尔实验室开发的SPIN、赫尔辛基工业大学计算机理论实验室开发的PR()D和MA-RIA、美国CMU计算机学院开发的SMV等。本文使用SMV作为对嵌入式软件验证的模型检查工具。

SMV基于"符号模型检查"(Symbolic Model Claec-king)技术，开始是为了研究符号模型检查应用的可能性而开发的一种对硬件进行检查的实验工具，现在已经发展成为广为流行的分析有限状态系统的常用工具。

本文中，软件系统模型用SMV语言描述。1个SMV程序由2部分组成：1个有限状态转换系统和1组CTL公式。SMV把初始状态和转换关系表示成二叉树图BDD(Binary Deciding Diagram)，CTL公式表示系统模型的属性，也表示成BDD。通过模型检查算法遍历系统状态空间，给出1个声明的属性是正确或者不正确的验证结果，并给出1个不满足该属性的反例。1个CTL公式真正的值通过遍历状态图的方式确定，这种遍历的时间复杂性和状态空间大小、公式的长度成线性关系。

3 触摸屏检测软件代码的验证

触摸屏作为人机界面的输入设备已经广泛应用于各种嵌入式系统中，如手持设备、工业控制、车载设备等。对于有些应用，触摸屏是关键的输入设备，触摸屏失效会导致整个系统不可用。因此设计高效、清晰、可靠的触摸屏驱动程序非常重要。本文使用有限状态机来描述触摸屏检测算法，然后使用SMV语言来描述此有限状态系统模型，最后使用SMV工具对此模型进行验证。

3．1 触摸屏检测的有限状态机

本文为了描述的简单，简化了触摸屏检测的过程。如图2所示，将触摸屏检测分为5个状态：触摸屏空闲(Tou-ch-Idle)、触摸屏抬起状态(Touch_Up)、触摸屏按下检测状态(Touch_ChkDown)、触摸屏按下状态(Touch_Down)以及触摸屏抬起检测状态(Touch_ChkUp)。触摸屏状态机是由事件触发来进行状态变换的，触发事件有触笔按下中断、触笔按下消抖定时溢出、触笔抬起中断、触笔抬起消抖定时溢出。

3．2 触摸屏检测的SMV模型

本节使用SMV语言对3．1节描述的触摸屏检测有限状态机进行建模，具体描述如下：

上述语言描述中，模块Touch_Detect()是触摸屏检测有限状态机的实现，它有3个布尔量参数：pen_irq、d_jittery_delay和u_jittery_delay。其中pen_irq表示触笔中断，当pen_irq为1时，表示触笔没有按下，为0时表示有触笔按下中断；d_jittery_delay为1表示触笔按下消抖时间到；u_jittery_delay表示触笔抬起消抖时间到。

本文主要验证了触摸屏检测状态机的可达属性。属性用公式(1)和(2)描述。公式(1)的含义是，从检测状态为抬起并其触笔无按下开始的所有计算路径中，总存在1条计算路径，能够到达检测状态为按下。公式(2)的含义是，从检测状态为按下并其触笔为按下开始的所有计算路径中，总存在1条计算路径，能够到达检测状态为抬起。