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