通过后向分析生成属性导向的潜在不变式

本文解决了在线性实数/整数算术片段中，基于 k-归纳的转移系统形式化分析中的引理生成问题。利用量词消去技术的后向分析被用于输出证明目标否定的原像，这些原像被视为未授权状态或灰色状态。提出了两种启发式方法以利用这一信息源。首先，通过对灰色状态空间可能划分的彻底探索，发现状态变量之间的新关系，代表潜在不变式。其次，不精确的探索对灰色状态空间的不相交区域进行归类和过近似，同样旨在发现状态变量之间的新关系。利用 k-归纳法隔离这些不变式，并检查它们是否加强了证明目标。这些启发式方法可用于后向探索的第一个原像，并且每当输出一个新的原像时，都会细化关于灰色状态的信息。在我们关键的航空嵌入式系统背景下，我们表明我们的方法在应用领域的相关示例上能够优于其他学术或商业工具。该方法通过两个主要示例进行介绍和论证，其中一个由 Rockwell Collins 在协作形式化验证框架中提供。