按照传统嵌入式软件开发方法，源代码级嵌入式软件开发涉及代码检查、静态分析和动态测试。每种方法都有缺点。

嵌入式软件代码检查仅依赖于检察人员的专业技术，若有大量耳机代码需要检查，则会是一项繁琐的工作。传统的静态分析技术主要依靠模式匹配方法检测不安全的代码模式，但无法证明不存在运行时错误。随着嵌入式软件日益复杂，对所有操作条件进行动态测试已经不太可能，软件测试只能发现错误，但不能证明错误不存在。

一种新的软件测试方法称为抽象解释，它以静态分析为基础，使用形式化数学证明，可发现某些运行时错误或证明它们不存在。抽象解释可直接应用于源代码，而无需执行代码。

抽象解释和基于证明的软件测试方法作为一种基于证明的软件测试方法，通过在以下问题中将三个大整数相乘可对抽象解释进行说明：虽然手动计算此问题的答案很费时，但是我们可以应用乘法法则确定答案的符号为负。确定此计算的符号就是抽象解释的一种应用。这种技巧使我们不需要对整数执行完成的乘法计算就能够准确地知道最终结果的一些属性，例如符号。利用乘法法则，我们还知道此计算的结果符号不可能为正。采用类似方式可将抽象解释应用到软件符号学中，以证明软件的某些属性。不执行程序本身，

通过软件测试源代码的某些动态属性，抽象解释在传统静态分析技术和动态测试之间架起桥梁。抽象解释在单个阶段中调查程序的所有可能行为，即所有可能值的组合，以确定如何以及在何种条件下程序会产生某些类别的运行时故障。由于抽象解释与考虑中的操作相关，我们可以用数学方法证明该技术能预测正确的结果，因此它得出的结果被认为是可靠的。