基于启发式NDFS的高性能软件模型验证算法

摘要

安全性是高性能安全苛求系统第一性能,为了确保其安全性,必须进行安全性验证,模型检测为系统安全品质保障和自动验证开辟了新途径.因此提出基于启发式NDFS的高 性能软件模型验证算法.在on-the-fly 判空检测算法的基础上,以广义Büchi 自动机为研究 对象,结合启发式NDFS(nested depth-first searches)算法,能较快地判断系统模型是否满足 属性性要求,并证明了算法的正确性.与以往算法相比,该算法准确性和检测效率更高,为 缓解形式化验证中的状态爆炸问题提供了有效的解决途径.