21世纪计算：模型检验和维数灾难

Model Checking and the Curse of Dimensionality

（中国软件网讯）Edmund M.Clarke是卡耐基梅隆大学计算机科学学院FORE荣誉教授、电气和计算机工程教授，以及2007年图灵奖获得者。他于1978年到1982年间在哈佛大学工作，然后加入到卡耐基梅隆大学计算机科学学院。2010年，他被选入了美国的工程学院，Clarke教授还是FORE的成员。

我非常荣幸能够受邀在这里为大家做演讲。我在北京已经呆了一周半的时间了，在这段时间里我有机会见到许多非常有才智的、有创造力的计算机科学方面的年轻学者、本科生和研究生。我很高兴看到他们目前所感兴趣的研究领域，以及他们正在尝试解决的问题。我相信未来十多年将和现在同样精彩。

我演讲的题目是“模型检验和维数灾难(Model Checking and the Curse of Dimensionality)”。模型检验是一种自动验证技术，它被成功地应用于验证电脑硬件，并也开始被用于验证电脑软件。但模型检查遇到的问题之一就是维数灾难。维数灾难最早由理查德·贝尔曼(Richard Bellman)提出，用来描述当数学空间维度增加时，它的相应体积将呈指数级增加的难题。当你再加入一个额外的组件变量到这个系统中的时候，模型检验就会遇到这样的问题。下面将给大家介绍模型检验都应用于哪些方面。

在美国，其实第一台上报出错信息的电脑就是英特尔奔腾4，这是一个分区错误(如图1)。你可以以这种方式获得很明显的错误提示。结果发现这个问题并不是出在错误本身，而是一个在芯片电路板上的逻辑错误。英特尔使用的是这样的一种算法，一个检查表，但这个检查表缺失了一项。这种硬件错误有时候比软件错误更加严重，因为你不能很快的解决这个问题。所以英特尔必须替换所有卖出去的电脑芯片，这估算将使他们损失了4到5亿美金。确实，这个错误给他们带来了巨大的损失。

图1 英特尔奔腾4报错

模型检验是一种针对有限状态迁移系统的高效自动验证技术。它是由我和几位科学家在21世纪80年代开发出来的。开始由语言学家的哲学论发明出来，起源于自然语言，而现在则被应用于计算机科学。它主要通过显式状态搜索或隐式不动点计算来验证有穷状态并发系统的模态命题性质。模型检验与其它的检验方法相比较有很多优势，首先它是一种算法，你不需要在实验室去做。另外，它和其它的方法相比较速度更快。比如说互动验证，基本上它会做出一种诊断，然后建议一系列的验证方法，而且可以做部分的设计验证。你做准则验证的时候，就可以得到一些使用结果，而且这个逻辑可以去表述许多并发的属性。

我们知道两位的计算需要两个状态，而N位的计算器需要N次方。所以它的主要弊端就是，当我们并行运算这些进程的时候，如果我们有两个状态死机，我们并行去运算就会有9个状态。一般来说，如果有M个进程，每一个有N个状态，这个系统就有有N的M次方个状态。

这也就是我们无法避免的维数灾难。但我们可以依据这些复杂的理论，并通过一些聪明的算法，一些复杂的数据结构和好的工程设计，来处理维数灾难了。通过过去30年中不断的发展，现在有两个逻辑是经常在模型检验中使用的。这种LTL也就是线性时序逻辑，我们会做一些验证，它有一个跟踪轨迹，并对第一个状态做标记，然Xa下一个状态值，FA代表a在未来可能正确的，GA就是在未来a将是完全正确的，aUb指直到b到达是真实的时候，a就是正确的。

还有一个线性时间计算模型Branching。(如图2) 可以做这样一个图形表示，如果我们把一个状态设为初始状态，也就是黑色的这个状态。它有一个过渡图，这个过渡图被演进成一个无尽的计算树，我们可以持续的做下去。

图2 线性时间计算模型Branching

最为知名的就是CTL计算树逻辑。这个公式是由TO(每个TO都包括两个部分)来量化“过去”在这个状态之中，一个TO会描述在路径上的序列，EFg，就是这样的一个分支，因为这是它的一个路径，在未来的某一个路径的点上，会有一个状态是属于g的。AFg是指这个计算树，因为在每个路径上都是A，但是在未来的某一个点上，在这个路径的某一点上是g，就是g将会必然成真的，它是不可避免的。大写的A，大写的G，小的G，在某个路径上A都是一个定量，是一个可及的状态，g是指在这个计算树的根上，因为g是肯定在这个路径上，这是一个潜在的定量，我们看到CTL这个逻辑，它使用了四个TO，它是通用的、普及的一种TO。

还有一种更加具有表述性的CTL，能够让我们做更加复杂的建网。这个模型检验问题非常容易理解，如果给了一个状态过渡图，我们要去定义所有的这些状态，也就是M.S=f，也就是在这个状态下，f是真的。为了解决这个逻辑，我们就可以用这些算法。我谈到的这些逻辑都使用到了，其中有一个算法是线性的，是状态大小，以及等式的长度，在实际上它的可用性是有限的，因为电脑内存的有限性。

下面我们再举一个小例子，来解释如何使用这种模型检验(如图3)。假设你发明了一个新的微波炉，或者你开发了一个新的电视机，很简单我们假设这个过渡系统，也就是控制这个微波炉的半导体或者说是这个芯片的部分。你可以关闭微波炉的门，点开始键，这个微波炉就可以加热了。比如说设定一个加热的时间，你可以使用TL来指定微波炉系统的属性，其中一个要检查的属性就是如果微波炉关上的时候，但是这个微波炉没有加热。你一定要说只要当门关上的时候，这个微波炉才能加热，否则会把人烫伤。为此需要设计一个条件，有当门关上的时候才能加热。所以我们可以设定这样一个时间逻辑，在模型检验中，我们需要一个硬件的描述，或者软件描述，在这个案例下是硬件的描述。这个时候我们就要验证属性的规范，我们可以编译硬件到一个过渡系统TSB。通常这个是非正式的表述，是用自然语言规范的表述，我们可以手动的把它做成一个TLF，也就是这种TL的等式，我们可以去做一个算法的验证来看我们做的这个公式在这个过渡系统中是否是正确的。

图3 微波炉过渡系统

另外一个例子，我们提到了关于这个逻辑的重要性。假设我们有一个状态过渡的示意图，是在我们这张图之下的，我们看到停止的标签，是从我们最初的状态是否可及的，就是这个蓝色的箭头，初始状态下很容易看到它的属性，检查一个不好的状态是无法可及的，是不能满足的。所有这些箭头会领导着我们从达到某一个停止的标签的地方，如果有这样一个指示是停止状态，这个安全的状态就能得到满足。然后这个模型检验，用它的属性可以达到检验的状态，像计算器一样，它可以能够按照这个箭头，按照这样的程序，或者这样一个电路来实现。

真实系统的第一个例子是1992年使用模型检验IEEE这个协议。令人更加震惊的是，因为这个协议的设计是从1988年开始的，但是以前的验证都是属于非正式的，现在我们只是照着这个去做，但出现很多错误，到1992年的时候，我们能发现这些错误。这里面有四个突破性的进展，在我们这个状态空间爆炸的问题上，我们来构建这样一个模型。第一个突破性进展，就是一种符号模型检验(Symbolic Moded Checking)。我们做这个模型检验，电脑反映出一些状态，一些过渡的图形，一些结构，就表明了这个图形。我们把这样一个图做一种隐性的使用，非常有效的去检查一些非常大的系统，来利用这样一种理念，来检查10的20次方可及的状态，然后能够达到检验10的120次的状态。很显然我们并不是使用单个的状态，我们使用的是状态集的状态。另外一个突破性进展，我们在开发这样一个逻辑的时候减少偏序数量。在这样一个比较复杂的系统里，有两个动作是要来回进行的，在A或者B的状态下，你不需要探索路径，你可以减少状态的数量。

另外一个大的突破，受到了约束式的模型检验，它使用这样一些快速状态的模式。我们也都知道这个问题是一个MP的，有很多人是表示怀疑的，能否检查比较大的方程式。对很多方程式，我们的检验是否能够很快的得到满足。通过使用这样一个快速的验证，能够应对系统成千上万的状态变量。这是一个简单的例子。假设，这个V是一个向量，或者叫做矢量，V的随着时间的变化而发生变化，我们可以用V0、V1表示，并认为初始的状态是可以使用的。如果V能满足这样一个公式，从V1到V2。还有这个公式不会在其中某一个状态上停滞不前，我们可以给这个公式有一个验证系统，能够发现属性失败。

这是一个现实状态，我的一个学生给我的。这个电路有1万个路径，我们采用公式，里面有400万的变量，还有1200个子句，然后找到最短的一个路径，它的长度37，可以在69秒中找到，以前我们还没有面对处理这么复杂的系统，现在做到了。

另外一个技术，我们叫做本地化的减少，或者叫做Counter example。简单的解释这个概念。CEGAR，是用于多数软件的模型检查。我们假设来推断电路的情况，抽取有关性来解释比较复杂的程序。假设一个具体的模式，这个M，我们可以抽取F值，这些状态群跟相关的状态结合起来，这样我们在抽取的模型上去映射到相关的类别上。我们抽取一些基本状态，用一种自然的方式去做，由红色向绿色过渡，这是我的一个映射。在相关的范畴，从红色到绿色的过渡，因为从某些红的状态向绿的状态过渡，还有红色状态向蓝色状态过渡。这也是在原始机器上使用。蓝色状态的过渡，从一种蓝色状态向另一种蓝色状态过渡，我们能够证明保留的路径就是针对这样一些属性。在这样一些系统里边，如果这个属性拥有一种抽象的模型，还有具体的模型。一个比较小的抽象模型跟它的具体模型相比来说，里面可能有一些技术条件是必要的，对于这样一个Theorem是真实的。

考虑到一些比较简单的，像交通灯一样，包括一些红绿灯，这样一个公式是AGAF red，它有中间过渡，还有其它颜色映射到红色去，让我们把绿色状态、黄色状态结合在一起。我们能够把它叫做结合状态，从red到go，就是行的状态，这两个红色是停的状态，会有一个过渡从红色到go这个状态，因为它是从红色到绿色状态的过渡。还有从go到红色，也是有一个从黄色状态向红色状态过渡;还有一个过渡是从go到它自己本身的，因为这里面涉及到绿色到红色，然后这个Spurious。现在这个公式已经不再是真实的了，在我们抽象机器上用了一个反例，就是在go状态一直保持下去。在最初的机器上并不是一个反例，当时在抽取系统是不行的，因为它这种行为并不是真实行为，只是一个抽象系统，我们把它叫做是反例：永远是go，它是一种虚假的状态。

图4 交通信号灯Spurious例子

这是一个抽象的验证使用过程，可以来验证硬件和软件，自动抽取，或者抽象的做法。我们从初始的抽象开始，可以得到一个虚假的反例，然后进一步推敲，如果继续执行下去，这个公式或者是有效的，或者是一个真实的反例情况。CEGAR就是反例抽象的取消，我们可以抽象一个过渡程序，也可以抽象一个过渡优化的电路程序。使用模型检验来论证我们抽象出的这个模型。并不是一个非常强大的论证，如果没有发现任何问题的话，在抽象的模型上也能验证这个电路是有效的。如果是反例的话，我们必须来模拟一个模拟器的反例，在具体的电路上，还有原始电路上模拟，来了解这是一个小的故障。如果这个模拟成功的话，我们可以找到这个小故障，如果不成功我们就必须有这样一个虚假的反例，所有这些信息都是在反例中做抽取。这就给我们带来了一个在模型检验中的一个大挑战，就是无法对软件做模型检验。

事实上对于软件的模型检验，微软一直都非常重视，这也是一个很大的挑战。对那些大型的不受束缚的基础状态，还有各种各样部署的单元。我可以不断部署各种模块，还有一些通用值，以及二级存储数据库，同时在基础数据呼叫，还有代码，像自建模码，还有从规模上，微软有100多万条的代码。其实对软件进行模型检验最常使用的方法把静态分析和模型检验联合使用。在信息复制和编译器优化上经常可以用到静态分析，从一个模型中抽取出来，然后使用模型检验判断是否属于某一种属性。在模型检验中有很多例子，比较成功的一个就是slim，也就是微软的系统，它用模型检验证明Windows计算机的模码，编程员在编程的时候确实符合数学模型的，如果这个驱动程序并不吻合这个模型，STV会发出报告。

还有一方面我非常感兴趣，就是对这种电路板做模型检验。这种比一般奔腾处理器的错误更加的有意思，它是P53NDM2。这样一个DNA修复，它是一种叫做被动式的入境，P53是一种蛋白质，它是一个非常重要的蛋白质，P53的通道主要是去涡旋细胞压力反应，P53可以启动DNA恢复，也就是叫做细胞循环捕获。也就是如果一个细胞内部出现问题，这个路径将首先尝试修复，如果无法修复，这个电路本身自杀。如果是形成了一个肿瘤，我们就可以预防肿瘤，P53被形容成为是基因的守护者。因为它能够防止细胞变异，在1993年也被称为分子的一年，这是《科学杂志》的说法。

现在我有一个项目就是做软件和硬件的，还有另外一个项目是做使用模型检验验证人的细胞内部的电路。我的一个博士学生，她是中国人，一位女士，她在微软实习。她在这个学期和剑桥微软研究院的生物系统的研究员一起，正在研究一个非常重要的癌症相关的项目。我相信对于在座的所有人来说未来都是非常光明的，我们有很多令人兴奋的工作可以去做，去打造更加复杂的软件系统，并且把这个技术用于其他的系统。谢谢大家!