博文
review: 谓词抽象技术研究
|||
谓词抽象技术研究
屈婉霞, 李暾, 郭阳, 杨晓东
软件学报 2008 Jan
摘要:
随着软、硬件系统规模和功能的不断扩充,状态空间爆炸问题严重影响了模型检验的进一步发展与应用,
成为验证大规模系统的瓶颈.谓词抽象是解决状态空间爆炸的最有效方法之一,近年来得到迅速发展.介绍了谓词抽象的基本算法并比较了不同的求解支持工具;重点分析了反例指导的抽象求精和基于插值的抽象求精原理;分析了产生新谓词的各种方法的优、缺点;最后指出了谓词抽象技术进一步发展所面临的挑战和发展方向.
成为验证大规模系统的瓶颈.谓词抽象是解决状态空间爆炸的最有效方法之一,近年来得到迅速发展.介绍了谓词抽象的基本算法并比较了不同的求解支持工具;重点分析了反例指导的抽象求精和基于插值的抽象求精原理;分析了产生新谓词的各种方法的优、缺点;最后指出了谓词抽象技术进一步发展所面临的挑战和发展方向.
关键词: 模型检验;谓词抽象;抽象求精;反例;插值
软硬件系统协同设计：
形式化验证方法: 等价性检验、模型检验和定理证明
the drawbacks of model checking: 状态空间爆炸问题
本文主要内容: 谓词抽象基本算法、谓词抽象求解工具、抽象模型精确度问题和新谓词的产生方法等.
1 谓词抽象基本算法
2 谓词抽象求解支持工具
Cambridge 高阶逻辑定理证明器HOL(high order logic)
Stanford 原型验证系统PVS(prototype verification system)
SAT 求解器: GRASP SATO Chaff
3 抽象模型精化
3.1 反例指导的抽象精化
3.1.1 谓词集合保持不变的模型精化
3.1.2 增加新谓词的模型精化
3.2 基于插值的抽象精化
4 新谓词的产生及谓词集合的优化
新谓词的产生方法:
(1) 从系统实现的高层描述中提取
(2) 不完备的启发式方法
(3) 完备的启发式方法
(4) 量化谓词的产生
5 谓词抽象的应用
SLAM ( Mcirosoft Asia )
BLAST
MAGIC (Canegie Mellon)
I comment:
《基于抽象解释理论的程序验证技术》 no read: 基于抽象解释理论的程序验证技术.pdf
https://blog.sciencenet.cn/blog-468147-529202.html
上一篇：review: 选择性集成学习算法综述 cont.
下一篇：review: 网络计算系统的分类研究
扫一扫，分享此博文