程序的形式验证 - 简介 中国科学院软件研究所 张文辉 http://lcs.ios.ac.cn/~zwh/pv 1
程序的形式验证 程序正确性: 程序正确性的最终体现: 以给定程序为主要组成部分的软件系统 具备我们期望的性质 2
程序正确性 程序 + 计算环境 性质 3
程序正确性 程序 + 计算环境 性质 系统模型 公式 4
形式验证 系统模型 公式 5
程序正确性的形式验证 软件 系统 运行过程 性质 抽象描述 或 模型 验证方法 逻辑公式 6
模型 验证程序是否具有要求的性质需要: 程序及其运行模式的表示方法 抽象的程序表示方法和系统模型 避开具体程序语言的细节 简化程序验证方法的讨论 建立在这样的模型之上的程序验证方法有普遍适用性 7
程序验证 软件 系统 运行过程 性质 抽象描述 或 模型 验证方法 逻辑公式 8
逻辑 验证程序是否具有要求的性质需要: 程序或其运行模式的性质的表示方法 程序逻辑 系统性 表达能力 建立在较强表达能力的程序逻辑之上的程序验证方法有普遍适用性 9
程序验证 软件 系统 运行过程 性质 抽象描述 或 模型 验证方法 逻辑公式 10
验证方法(1) 验证程序是否具有要求的性质需要: 验证方法 推理验证 基于推理规则 模型检测 适用范围广 实用性受限于推理复杂性和设计推理方案的难度、证明失败不一定能说明什么问题 11
验证方法(2) 验证程序是否具有要求的性质需要: 验证方法 推理验证 基于状态搜索 模型检测 自动化程度高 适用于有限状态系统模型的验证，计算复杂性高、实用性受限于状态爆炸问题 12
课程内容 软件 系统 运行过程 性质 抽象描述 或 模型 验证方法 逻辑公式 13
形式验证的主要过程 用形式语言 为程序与系统建立模型 用逻辑公式 描述程序性质 用形式验证方法 证明系统模型是否具备所描述性质 14
课程内容 预备知识 程序与系统模型 程序逻辑 推理验证方法 模型检测方法 15
课程内容 预备知识 程序与系统模型 程序逻辑 推理验证方法 模型检测方法 逻辑、集合、关系、有向图 16
课程内容 预备知识 程序与系统模型 程序逻辑 推理验证方法 模型检测方法 流程图程序、迁移系统、 自动机、Petri网、通讯系统 17
课程内容 预备知识 程序与系统模型 程序逻辑 推理验证方法 模型检测方法 时序逻辑、计算树逻辑、μ演算 18
课程内容 预备知识 程序与系统模型 程序逻辑 推理验证方法 模型检测方法 迁移系统的推理、 流程图程序的推理、Hoare逻辑 19
课程内容 预备知识 程序与系统模型 程序逻辑 推理验证方法 模型检测方法 基于路径的模型检测方法、 基于状态的模型检测方法 20
预期目标 掌握并能够综合应用以下知识: 程序与 系统模型 验证方法 程序逻辑 几类 简单的 基本原理 几类 简单的 21
问题 ? 22