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

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条计算路径，能够到达检测状态为抬起。
3．3 验证结果
在Intel CPU
通过这个验证结果，可知3．2节中描述的触摸屏检测算法模型满足状态可达性。

4 总 结
本文采用有限状态机对嵌入式软件进行建模，使用SMV语言描述状态机模型，并通过符号模型检查工具SMV对SMV语言描述的状态机模型进行验证。嵌入式软件系统的正确性、可靠性占据至关重要的地位。基于模型检查的验证方法可以在嵌入式软件开发的早期发现错误，从而避免大量重复性的劳动，减少导致严重后果的因素。