模型检验（4）（091231）
闵应骅
    模型检验的成功之处在于它用自动搜索代替手动证明来解决验证的问题。模型检验包括三部分：1。基于命题时态逻辑的规范语言，2。表示被验证系统的编码状态机的方法，3。验证算法，对状态空间的智能搜索以确定规范是真还是假。如果规范没有被实现，模型检验能够给出反例。这一条非常重要，因为它帮助我们debug。如图2所示。
    状态爆炸是模型检验中的一个大问题，因为现在的复杂系统，其状态数都是天文数字。n个相互异步的进程，如果每个进程有m个状态，其状态数为m的n次方（m^n)。近年来，正是在这方面有许多突破。
    有序的二进制判决图（OBDD）提供了处理大系统进行符号模型检验的可能性。例如某些具有10^20状态的实例进行了符号模型检验。
    软件进程之间往往是异步的，状态数就会指数级增加。两个事件称为是独立的，如果不论它们按什么顺序执行，其结果是相同的整体状态。用偏序简化方法可以部分地解决异步进程的状态爆炸问题。
    近年来，布尔可满足性问题（SAT）的进展，对模型检验提出了有界模型检验（BMC）对硬件设计验证特别有效。其主要想法如下。假如要检验形如Fp的性质，BMC要确定是否存在一个长度为k的反例，即是否存在一条长度为k的通路，结束于一个循环，其每一个状态都有¬p。这里所谓有界就是指这个k。有人对9510个锁存器和9499个输入的电路做了BMC。
    抽象映射是简化模型检验的另一种方法，如图4所示，把一堆状态简化为一个状态。原来系统称为具体系统，而简化了的系统称为抽象系统。抽象系统能够保持具体系统的许多性质，但也会丢失某些性质。已有许多结果揭示这一问题。
    状态爆炸的问题已经有了许多的研究，但是，并没有完全解决。这正是未来要解决的问题。



转载本文请联系原作者获取授权，同时请注明本文来自闵应骅科学网博客。
链接地址：https://wap.sciencenet.cn/blog-290937-282991.html

上一篇：模型检验（3）（091231）
下一篇：模型检验（5）（100101）