基于抽象-验证-细化范例的软件模型检测

摘要：

如何保证软件系统的正确性和可靠性是当前软件开发面临的主要问题之一.模型检测作为一种重要的自动化验证技术在软件的分析与验证中正取得越来越多的成功.本文以微软的SLAM和加州大学伯克利分校的BLAST为例综述性地介绍了基于抽象-验证-细化范例的软件模型检测.

关键词：模型检测、软件模型检测、谓词抽象、反例驱动的细化

所属期刊栏目：33

分类号：TP3(计算技术、计算机技术)

资助基金：国家自然科学基金60473003;教育部跨世纪优秀人才培养计划;高等学校博士学科点专项科研项目20050183065

在线出版日期：2007-01-18（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：255-260