计算机科学 ›› 2006, Vol. 33 ›› Issue (12): 255-260.
• 计算机网络与信息安全 • 上一篇 下一篇
出版日期:
发布日期:
基金资助:
Online:
Published:
摘要： 如何保证软件系统的正确性和可靠性是当前软件开发面临的主要问题之一。模型检测作为一种重要的自动化验证技术在软件的分析与验证中正取得越来越多的成功。本文以微软的SLAM和加州大学伯克利分校的BLAST为例综述性地介绍了基于抽象-验证-细化范例的软件模型检测。
关键词: 模型检测 软件模型检测 谓词抽象 反例驱动的细化
Abstract: How to assure the correctness and reliability of software systems is one of the main problems in software development. Being an important automatic verification technique, Model checking is more and more successful in software analysis and verification. T
Key words: Model checking, Software model checking,Predicate abstraction,Counterexample-driven refinement
. 基于抽象-验证-细化范例的软件模型检测[J]. 计算机科学, 2006, 33(12): 255-260. https://doi.org/
0 / / 推荐
导出引用管理器 EndNote|Reference Manager|ProCite|BibTeX|RefWorks
链接本文: https://www.jsjkx.com/CN/
https://www.jsjkx.com/CN/Y2006/V33/I12/255
Cited
首页