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

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