论文部分内容阅读
随着软、硬件系统规模和功能的不断扩充，状态空间爆炸问题严重影响了模型检验的进一步发展与应用，成为验证大规模系统的瓶颈．谓词抽象是解决状态空间爆炸的最有效方法之一，近年来得到迅速发展．介绍了谓词抽象的基本算法并比较了不同的求解支持工具；重点分析了反例指导的抽象求精和基于插值的抽象求精原理；分析了产生新谓词的各种方法的优、缺点；最后指出了谓词抽象技术进一步发展所面临的挑战和发展方向。