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

3．3 验证结果

在Intel CPU通过这个验证结果，可知3．2节中描述的触摸屏检测算法模型满足状态可达性。

4 总 结

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