基于不可满足核的近似逼近可达性分析

近年来，形式化验证技术受到了越来越多的关注，它在保障安全关键领域系统的安全性和正确性方面发挥着重要的作用.模型检测作为形式化验证中自动化程度较高的分支，具有十分广阔的发展前景.本文中我们研究并提出了一种新的模型检测技术，可以有效地对迁移系统进行模型检测，包括不安全性检测和证明安全性.与现有的模型检测算法不同，我们提出的这种方法——基于不可满足核（unsatisfiable core，UC）的近似逼近可达性分析（UC-based approximate incremental reachability，UAIR），主要利用不可满足核来求解一系列的候选安全不变式直至生成最终的不变式，以此来实现安全性证明和不安全性检测（漏洞查找）.在基于SAT求解器的符号模型检测中，我们使用由可满足性求解器得到的UC构造候选安全不变式，如果迁移系统本身是安全的，我们得到的初始不变式只是安全不变式的一个近似.然后，我们在检查安全性的同时，逐步改进候选安全不变式，直到找到一个真正的不变式，证明系统是安全的；如果系统是不安全的，我们的方法最终可以找到一个反例证明系统是不安全的.作为一种全新的方法，我们利用不可满足核进行安全性模型检测，取得了相当好的效果.众所周知，模型检测领域没有绝对最好的方法，尽管我们的方法在基准的可解数量上无法超越当前的成熟方法例如IC3、CAR等，但是我们的方法却可以解出3个其他方法都无法解出的案例，相信本方法可以作为模型检测工具集很有价值的补充.

UC-based Approximate Incremental Reachability

In recent years, formal verification technology has received more and more attention, and it plays an important role in ensuring the safety and correctness of systems in critical areas of safety. As a branch of formal verification with a high degree of automation, model checking has a very broad development prospect. In this paper, we study and propose a new model checking technique, which can effectively check transition systems, including bug-finding and safety proof. Different from existing model checking algorithms, our proposed method, UC-based approximate incremental reachability (UAIR) based on unsatisfiable core (UC), mainly utilizes the unsatisfiable core to solve a series of candidate safety invariants until the final invariant is generated, so as to realize safety proof and bug-finding. In symbolic model checking based on the SAT solver, we use the UC obtained by the satisfiability solver to construct candidate safety invariant, and if the transition system itself is safe, the initial invariant we get is only an approximation of the safety invariant. Then, while checking the safety, we gradually improve the candidate safety invariant until we find a real invariant that proves the system is safe; if the system is unsafe, our method can finally find a counterexample to prove the system is unsafe. As a brand new method, we exploit unsatisfiable cores for safety model checking and achieve quite good results. As we all know, there is no absolute best method in the field of model checking, although our method cannot surpass the current mature methods such as IC3, CAR, etc, it is believed that this method can be a valuable addition to the model checking toolset.