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