嵌入式系统/ARM技术中的一种基于模型检查的嵌入式软件验证方法

嵌入式软件广泛应用于不同领域,如消费电子、工业控制、汽车电子、移动通信等。嵌入式软件的可靠性保证十分关键。嵌入式软件中常见的错误包括状态机错误、时序错误、栈溢出/存储溢出等,在开发过程中对嵌入式软件进行验证十分重要。 对嵌入式软件的验证一般依赖于形式化的方法。 形式化的方法可以对嵌入式软件系统进行严格的规约,并可以对系统进行不同视角的验证。验证主要是分析系统是否具有期望的性质。常见的验证技术主要有模型检查和定理证明。模型检查自动化程度高,并且当系统不具有期望性质时能给出反例,但它存在状态爆炸问题。定理证明能基于无穷状态空间分析,但是自动化程度不高,需要人工干预,并且在证明失败后不能