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

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

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

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

　　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公式真正的值通过遍历状态图的方式确定，这种遍历的时间复杂性和状态空间大小、公式的长度成线性关系。