《课程总结-讲稿---.ppt》由会员分享，可在线阅读，更多相关《课程总结-讲稿---.ppt（34页珍藏版）》请在三一文库上搜索。
1、1,程序的形式验证 内容,中国科学院软件研究所 张文辉 http:/ 逻辑/函数/有向图,程序逻辑,验证方法: 推理证明/模型检测,课程内容,程序与系统模型,隐式迁移模型,显式状态迁移模型,标号迁移系统,时间迁移系统等模型,一阶线性时序逻辑,课程内容,程序逻辑,线性时序逻辑PLTL,分枝时序逻辑CTL,时序逻辑CTL*等,课程内容,程序的推理证明,卫式迁移模型的推理,谓词迁移模型的推理,流程图模型的推理,结构化程序模型推理,课程内容,程序的模型检测,基于路径的模型检测,基于状态的模型检测,限界语义模型检测,7,课程总结,给定一个程序和一些性质 用严格的方法 证明程序是否满足给定的性质,程序,性
2、质,模型,逻辑公式,验证方法,8,主要内容,程序模型 程序逻辑 验证方法,模型,逻辑公式,验证方法,验证工具 验证实例,9,一、程序模型,隐式迁移系统描述 结构化循环程序、流程图程序 卫式迁移系统、谓词迁移系统 显式状态迁移系统描述 Kripke结构、标号Kripke结构 公平Kripke结构 标号迁移系统 标号迁移系统、自动机 交错迁移系统、交错自动机 时间迁移系统 时间迁移系统、时间自动机 混成迁移系统、 Petri网、通信系统,不同类型 模型的特点,模型之间的 关系,用模型 描述系统,10,结构化循环程序,谓词逻辑、解释、赋值 语句组合 运行、语义 前断言、后断言 推理验证方法,11,流
3、程图程序,谓词逻辑、解释、赋值 指令集合、begin - end 运行、语义 前断言、后断言 推理验证方法,12,卫式迁移系统,谓词逻辑、解释、赋值 迁移集合、初始条件 状态、状态序列、可执行迁移、运行 推理验证方法,13,谓词迁移系统,谓词逻辑、解释、赋值 迁移的谓词、初始条件 状态、状态序列、可执行迁移、运行 推理验证方法,14,Kripke结构, S: 状态集合 RSxS: 迁移关系 I S: 初始状态集合,状态、状态序列、迁移、路径、运行,15,标号Kripke结构, S: 状态集合 RSxS: 迁移关系 I S: 初始状态集合 L: S2AP: 标号函数,语言,16,公平标号Krip
4、ke结构, S: 状态集合 RSxS: 迁移关系 I S: 初始状态集合 L: S2AP: 标号函数 F 2S: 公平要求的集合,公平运行、语言,17,标号迁移系统, :标号集合 S: 状态集合 S x x S: 迁移关系 I S: 初始状态集合,运行、字符串、语言,18,Buchi自动机, :标号集合 S: 状态集合 S x x S: 迁移关系 I S: 初始状态集合 F 2S: 接受条件,不同类型 的自动机,可接受运行、可接受字符串、语言,19,交错迁移系统, :标号集合 S: 状态集合 S x x 2S: 迁移关系 I S: 初始状态集合,树结构的运行,20,交错自动机, :标号集合 S
5、: 状态集合 S x x 2S: 迁移关系 I S: 初始状态集合 F 2S: 接受条件,可接受运行、可接受字符串、语言,21,时间迁移系统, :标号集合 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: 迁移关系
6、I S: 初始状态集合 flow: S (X,X),时间字符串、时间字符串上的运行,24,Petri网, P: 位置集合 T: 迁移集合 F (P T) (T P) : 边的集合 M0 : PN 初始状态,状态、迁移、运行、可达状态,25,通信单元、通信系统, Q: 状态集合 C: 通道集合 Q (C) Q: 迁移关系 q0 Q: 初始状态,事件、可执行事件、状态、迁移、运行,26,二、程序逻辑,线性时序逻辑 命题线性时序逻辑 一阶线性时序逻辑 线性-演算 分枝时序逻辑 计算树逻辑(CTL) CTL* 模态-演算,公式之间的 关系,公式和模型 的对应关系,公式和状态集 的对应关系,用公式描述
7、系统或性质,不同逻辑的 特点,逻辑之间的 关系,27,线性时序逻辑,命题逻辑、谓词逻辑 语言 语义 逻辑公式之间的关系 逻辑公式用于描述性质和系统模型 逻辑公式对应于系统模型(自动机),28,分枝时序逻辑,命题逻辑 语言 语义 逻辑公式之间的关系 逻辑公式用于描述性质 逻辑公式对应于Kripke结构的状态集,29,三、验证方法,推理验证 卫式迁移系统 流程图程序 结构化程序 模型检测 基于状态 基于路径 限界模型检测,模型检测方法： 特点 应用 相关的结构和算法,程序推理方法： 特点 应用,30,推理验证,卫式迁移系统 程序推理规则 线性时序逻辑推理规则 流程图程序 根据操作语义证明 根据路径
8、分段证明、最弱宽松前断言计算方法 结构化程序 根据指称语义证明 根据公理语义、Hoare逻辑证明,安全性质 响应性质 部分正确 完全正确,31,模型检测,基于状态 显式状态迁移系统 符号状态迁移系统(最简二元决策图) 基于路径 用自动机表示系统 用自动机表示性质(由公式构造自动机的方法) 限界模型检测 限界模型 限界语义及应用,32,四、验证工具与实例,验证工具 程序推理辅助工具XYZ/VERI-II 模型检测工具SMV 模型检测工具SPIN 模型检测工具VERDS 验证实例 结构化程序 协议 电路,对课程内容 的总体认识,33,关于考试,各种算法和方法的使用 各种模型语言和逻辑语言的使用,34,问题 ?,