模型检验(闵应骅).docxVIP

. . . . 模型检验（ 模型检验（ 1）（ 091230 ） 大家承认，计算机领域的 ACM 图灵奖相当于自然科学的诺贝尔奖。 2007 年图灵奖授予 Edmund M. Clarke ，E. Allen Emerson, 和 Joseph Sifakis 。他们创立了模型检验 --- 一种验证技术， 用算法的方式确定一个硬件或软件设计是否满足用时态逻辑表述的形式规范。 如果不能满足， 则提 供反例。他们在 1981 年提出这个方法，经过 28 年的发展，已经在 VLSI 电路、通信协议、软件设 备驱动器、 实时嵌入式系统和安全算法的验证方面得到了实际应用。相应的商业工具也已出现， 估 计今后将对未来的硬件和软件产业产生重大影响。 2009 年 11 月 CACM 发表了三位对模型检验的新的诠释。本人将用几次对他们的诠释做一个通俗的介绍，对我自己也是一个学习的过程。 Edmund M. Clarke 现在是美国卡内基梅隆大学 （ CMU ）计算机科学系教授。 E. Allen Emerson 是在美国奥斯汀的德州大学计算机科学系教授。 Joseph Sifakis 是法国国家科学研究中心研究员， Verimag 实验室的创立者。 模型检验（ 2）（ 091231 ） 程序正确性的形式验证依靠数学逻辑的使用。 程序是一个很好定义了的、可能很复杂、 直观上不好理解的行为。而数学逻辑能精确地描述这些行为。过去，人们倾向于正确性的形式证明。而模 型检验回避了这种证明。在上世纪 60 年代，流行的是佛洛伊德 -霍尔式的演绎验证。这种办法像手动证明一样，使用公理和推论规则，比较困难，而且要求人的独创性。一个很短的程序也许需要很 长的一个证明。 不搞程序正确性证明，可以使用时态逻辑，一种按时间描述逻辑值变化的形式化。 如果一个程序可以用时态逻辑来指定， 那它就可以用有限自动机来实现。 模型检验就是去检验一个有限状态图 是否是一个时态逻辑规范的一个模型。 对于正在运行的并发程序，它们一般是非确定性的，像硬件电路、微处理器、操作系统、银行 网络、通信协议、汽车电子及近代医学设备。时态逻辑所用的基本算子是 F（有时）， G（总是）， X（下一次）， U （直到）。现在叫线性时间逻辑（ LTL ）。 另一种常用的逻辑是计算树逻辑（ CTL ）。它的基本时态是 A （对所有以后的交易）， E （对某些以后的交易），跟随着 F， G， X， U 之一。复合公式是线性时间逻辑子公式的嵌套和组合。 例如 AFp （以后， p 终将成立，因此是必然的。） EFp （以后， p 最后可能成立。）如图 1 所示。 时态逻辑公式可以在给定的有限状态图上加以解释。所以又称为克里普克（ kripke ）结构。 M 包含一个状态集 S ，一个完全的二进制转换关系 R ? S ×S, 和一个状态标签 L，其原子事实为真。用 M, s0 |= f 表示 “在结构 M 中，于状态 s0， f 为真。 ”或者简写为 M |= f. 例如， M, s0 |= AFp 当且仅当对在 M 中的所有通路 x = s0, s1, s2, . . . 我们有对任何 i =0, P ∈ L(si). 当我们写规范的时候，我们只写 AFp ，断言公式 p 是必然的。一个线性时间逻辑公式 h 意味着在整个结构皆为真， 即 Ah。在线性时间逻辑中， G? (C1 ∧ C2) 表明进程 C1 和 C2 总是互相排斥的。而在计算树逻辑中则写成 AG? (C1 ∧ C2) 。AG(T1 ? AFC1) 意味着只要进程 1 进入它的尝试区域 T1 ，它总是进入它的关键段 C1 。AGEFstart 表示系统总是可以重新启动的。 这在线性时间逻辑中是无法表示的。 而 CTL* 中的 EGFsend 则表明存在一个公平的行为，使得 send 条件可以重复出现。 这些逻辑已经在工业界得到广泛应用，包括基于 CTL 的 IBM Sugar ，基于 LTL 的 Intel For-Spec ， 和 IEEE 1850 标准所用的 PSL 用 了 CTL* 。 还有命题演算，非常一般的 TL。它允许时态正确性的不动点递归定义。例如 EFp = p ∨ EX(EFp) 。时态正确性的不动点特征在模型检验的算法和工具中都很有用。 模型检验（ 3）（ 091231 ） 时态逻辑用来描述正确的系统行为， 模型检验提供实用的硬件和软件验证方法。 模型验证可形式地描述如下：给定一个有限结构 M，状态 s，和一个时态逻辑公式，问 M, s |= f ? 即问：在结构M 中，于状态 s0 ，f 是否为真？或者说，给定 M 和 f,计算这个集合 {s : M, s