课程总结-讲稿---ppt课件

1、1程序的方式验证 内容中国科学院软件研讨所张文辉lcs.ios.ac/zwh/pv课程主要内容程序与系统模型预备知识: 逻辑/函数/有向图程序逻辑验证方法: 推理证明/模型检测课程内容程序与系统模型隐式迁移模型显式形状迁移模型标号迁移系统时间迁移系统等模型一阶线性时序逻辑课程内容程序逻辑线性时序逻辑PLTL分枝时序逻辑CTL时序逻辑CTL*等课程内容程序的推理证明卫式迁移模型的推理谓词迁移模型的推理流程图模型的推理构造化程序模型推理课程内容程序的模型检测基于途径的模型检测基于形状的模型检测限界语义模型检测7课程总结给定一个程序和一些性质用严厉的方法证明程序能否满足给定的性质程序性质模型逻辑公式

2、验证方法8主要内容 程序模型 程序逻辑 验证方法模型逻辑公式验证方法 验证工具 验证明例9一、程序模型 隐式迁移系统描画 构造化循环程序、流程图程序 卫式迁移系统、谓词迁移系统 显式形状迁移系统描画 Kripke构造、标号Kripke构造 公平Kripke构造 标号迁移系统 标号迁移系统、自动机 交错迁移系统、交错自动机 时间迁移系统 时间迁移系统、时间自动机 混成迁移系统、 Petri网、通讯系统不同类型模型的特点模型之间的关系用模型描画系统10构造化循环程序 谓词逻辑、解释、赋值 语句组合 运转、语义 前断言、后断言 推理验证方法11流程图程序 谓词逻辑、解释、赋值 指令集合、begin

3、- end 运转、语义 前断言、后断言 推理验证方法12卫式迁移系统 谓词逻辑、解释、赋值 迁移集合、初始条件 形状、形状序列、可执行迁移、运转 推理验证方法13谓词迁移系统 谓词逻辑、解释、赋值 迁移的谓词、初始条件 形状、形状序列、可执行迁移、运转 推理验证方法14Kripke构造 S: 形状集合 RSxS: 迁移关系 I S: 初始形状集合形状、形状序列、迁移、途径、运转15标号Kripke构造 S: 形状集合 RSxS: 迁移关系 I S: 初始形状集合 L: S2AP: 标号函数言语16公平标号Kripke构造 S: 形状集合 RSxS: 迁移关系 I S: 初始形状集合 L: S2

4、AP: 标号函数 F 2S: 公平要求的集合公平运转、言语17标号迁移系统 :标号集合 S: 形状集合 S x x S: 迁移关系 I S: 初始形状集合运转、字符串、言语18Buchi自动机 :标号集合 S: 形状集合 S x x S: 迁移关系 I S: 初始形状集合 F 2S: 接受条件不同类型的自动机可接受运转、可接受字符串、言语19交错迁移系统 :标号集合 S: 形状集合 S x x 2S: 迁移关系 I S: 初始形状集合树构造的运转20交错自动机 :标号集合 S: 形状集合 S x x 2S: 迁移关系 I S: 初始形状集合 F 2S: 接受条件可接受运转、可接受字符串、言语2

5、1时间迁移系统 :标号集合 S: 形状集合 C: 时钟集合 S x x 2C x(C)xS: 迁移关系 I S: 初始形状集合时间字符串、时间字符串上的运转22时间自动机 :标号集合 S: 形状集合 X: 时钟集合 S x x 2X x(X)xS: 迁移关系 I S: 初始形状集合 F 2S: 接受条件可接受运转、可接受时间字符串、言语23混成迁移系统 :标号集合 S: 形状集合 X: 实数变量集合 S x x (X) x (X) x S: 迁移关系 I S: 初始形状集合 flow: S (X,X) 时间字符串、时间字符串上的运转24Petri网 P: 位置集合 T: 迁移集合 F (P T

6、) (T P) : 边的集合 M0 : PN 初始形状形状、迁移、运转、可达形状25通讯单元、通讯系统 Q: 形状集合 C: 通道集合 Q (C) Q: 迁移关系 q0 Q: 初始形状事件、可执行事件、形状、迁移、运转26二、程序逻辑 线性时序逻辑 命题线性时序逻辑 一阶线性时序逻辑 线性-演算 分枝时序逻辑 计算树逻辑(CTL) CTL* 模态-演算公式之间的关系公式和模型的对应关系公式和形状集的对应关系用公式描画系统或性质不同逻辑的特点逻辑之间的关系27线性时序逻辑 命题逻辑、谓词逻辑 言语 语义 逻辑公式之间的关系 逻辑公式用于描画性质和系统模型 逻辑公式对应于系统模型(自动机)28分枝

7、时序逻辑 命题逻辑 言语 语义 逻辑公式之间的关系 逻辑公式用于描画性质 逻辑公式对应于Kripke构造的形状集29三、验证方法 推理验证 卫式迁移系统 流程图程序 构造化程序 模型检测 基于形状 基于途径 限界模型检测模型检测方法：特点运用相关的构造和算法程序推理方法：特点运用30推理验证 卫式迁移系统 程序推理规那么 线性时序逻辑推理规那么 流程图程序 根据操作语义证明 根据途径分段证明、最弱宽松前断言计算方法 构造化程序 根据指称语义证明 根据公理语义、Hoare逻辑证明平安性质呼应性质部分正确完全正确31模型检测 基于形状 显式形状迁移系统 符号形状迁移系统(最简二元决策图) 基于途径 用自动机表示系统 用自动机表示性质(由公式构造自动机的方法) 限界模型检测 限界模型 限界语义及运用32四、验证工具与实例 验证工具 程序推理辅助工具XYZ/VERI-II 模型检测工具SMV 模型检测工