论文部分内容阅读
随着软硬件系统规模和功能的不断扩充，状态空间爆炸问题严重影响了模型检验的进一步发展与应用，成为验证大规模系统的瓶颈。在显式模型检验工具Murphi的基础上，针对其可达状态空间组织存在的问题进行改进，提出了基于整型指针与Fibonaeei散列的可达状态空间组织方法，实现了一个高效的显式模型检验原型系统，在确保验证正确的同时有效缩短了验证时间，并能在系统规范不可满足的情况下给出反例，有助于系统设计人员快速定位错误。理论分析和实验结果表明了本方法的有效性。