模型检验幻灯片.pptVIP

模型检验 钱思佑 模型检验概述 时态逻辑TL 线性TL 分支时态逻辑（CTL） CTL模型检验 模型检验的定义 模型检验是一个自动化的验证工具，其可以很快的发现设计错误。它的基本思想是用CTL公式表达系统的所期望性质，用有限状态机FSM表示系统的状态转移结构，通过遍历FSM来检验时态逻辑公式的正确性。如果不能验证公式的正确性，则系统将给出一个反例，使用户发现公式不成立的原因。 One of the major applications of temporal logics in computer science is temporal specification and verification of programs. These mean: to specify by means of temporal formulae the properties which a program must satisfy, and given a program to verify formally that the specifications are met. 运用时态逻辑证明程序所声明的性质的两种方法： 定理证明：运用定理来严格的推理论证一个程序所声明的性质。 模型检验：通过建立有限状态的模型结构来描述程序，并运用时态逻辑公式来证明它所声明的性质。 模型检验相对于定理证明的主要优点： 它是完全自动化的，不需要人的干预，而不象定理证明那样需要专业人员才能对其进行操作。 它不是一个一般性的定理证明方法，但是如果它一旦是可用的，那么它的适应性就会更好，而且也更有效。 计算复杂性相对较低。 当出错时能通过产生反例来告知用户使其发现公式不成立的原因. 形式化验证的基本概念 例：组合电路的形式化验证 输入：a,b,c,d 输出：x x=f(a,b,c,d) 电路行为是： F=c ∧d ∨a∧b ∧d∨ ┐ a∧ ┐ b∧d∨ ┐ a∧ ┐ c∧d a 。 b 。 c 。 d 。 则我们根据电路得出其输出为： f(a,b,c,d)= ┐(┐(┐a ∨b ∨c) ∨ ┐d) 于是证明电路的实现与它的规范问题就化为了利用布尔代数的定律证明函数F与f的等价性问题。 f= ┐(┐(┐a ∨b ∨c) ∨ ┐d) ((┐a ∨b )∨c) ∧d ((┐a ∨(┐a ∧ ┐ b)) ∨a∧b∨c) ∧d ((c∨┐a) ∨┐a∧┐b∨a∧b∨c) ∧d (c∧d∨a∧b∧d∨┐a∧┐b∧d∨┐a∧┐c∧d) F 电路的结构描述必须要转化为形式逻辑的描述，行为描述已经是逻辑描述，不用转化了，然后再运用验证程序进行形式化验证。 时态逻辑 时态逻辑是一种模态逻辑，其实也是模态逻辑的扩展，它涉及了含有时间信息的状态，表示系统的各个事件在时间上的次序。 Temporal logic 与 classical logic 的比较 Temporal logic 相对 classical logic 加入了时序操作。 Classical logic describes a snapshot of the universe. Temporal logic pictures a movie of the universe. TL的分类 线性的 …… 分支的 线性TL就是把系统的状态序列按时间处理成线性，对于它的每个状态，其下一个状态都是确定的。 而在分支TL中，对于其中某些状态，其后续状态是不确定的。有几种可能，就有几个分支。 因为分支TL的状态图呈树状，所以称为CTL（Computional Tree Logic）。 线性TL 对于线性TL，因为状态是线性的，所以不需要考虑分支的情况。 其时序操作算子有： □ Always □A表示“A总为真”。 ……