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

摘要：

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

关键词： 模型检测 安全苛求系统 高性能 on-the-fly 判空检测 安全性验证

作者: 王曦 徐中伟

作者单位: 同济大学电子与信息工程学院, 上海 201804

会议类型: 国内会议

会议名称: 2010年全国高性能计算学术年会(HPC china2010)

会议地点: 北京

会议语种:中文

页码: 249-259

在线出版日期: 2010-10-27（万方平台首次上网日期，不代表论文的发表时间）