- 1、本文档共112页,可阅读全部内容。
- 2、有哪些信誉好的足球投注网站(book118)网站文档一经付费(服务费),不意味着购买了该文档的版权,仅供个人/单位学习、研究之用,不得用于商业用途,未经授权,严禁复制、发行、汇编、翻译或者网络传播等,侵权必究。
- 3、本站所有内容均由合作方或网友上传,本站不对文档的完整性、权威性及其观点立场正确性做任何保证或承诺!文档内容仅供研究参考,付费前请自行鉴别。如您付费,意味着您自己接受本站规则且自行承担风险,本站不退款、不进行额外附加服务;查看《如何避免下载的几个坑》。如果您已付费下载过本站文档,您可以点击 这里二次下载。
- 4、如文档侵犯商业秘密、侵犯著作权、侵犯人身权等,请点击“版权申诉”(推荐),也可以打举报电话:400-050-0827(电话支持时间:9:00-18:30)。
查看更多
中国科大 第6章 模型检测 验证是提高软件可信程度的重要方法 模型检测 基于逻辑推理的程序验证 模型检测 一种验证系统?满足性质? (? ? ? )的方法。它操作在系统的模型?(语义)上,而不是在系统的描述(语法)上 通过遍历系统所有状态空间,能够对有穷状态系统进行自动验证,并自动构造不满足验证性质的反例 第6章 模型检测 模型检测的应用 常用于硬件验证和通信协议的验证中 现在开始用于软件的验证 模型检测过程的大体步骤 由用户描述的一个模型开始 判断用户所断言的假设在模型中是否有效 若无效,则产生由执行轨迹构成的反例 第6章 模型检测 内容概述 命题逻辑和谓词逻辑的简短回顾 线性时态逻辑及其在模型检测中的应用 计算树逻辑及其在模型检测中的应用 命题逻辑的回顾 合适公式的归纳定义 ? ::= p | (? ? ) | (? ? ? ) | (? ? ? ) | (? ? ? ) 推理规则(包括公理) (? i) (?e1) (?e2) 语法推论 若从?1, ?2, …, ?n 可以证明?,表示成 ?1, ?2, …, ?n ? ? , 简写成 ? ? ? 逻辑等价 ? ? ? 并且 ? ? ? 命题逻辑的回顾 命题逻辑的语义 定义真值集合(给p, q指派真值) 把各逻辑连接词映射到真值集合上的运算(真值表方式) 各推理规则在该模型中成立 语义推论 若?1, ?2, …, ?n的值都为真, 则? 值也为真, 写成 ?1, ?2, …, ?n ? ? , 简写成 ? ? ? 语义等价 ? ? ?并且? ? ? 可满足性 ?是可满足的,若存在一种指派使?的值为真 命题逻辑的回顾 命题逻辑是可靠的和完备的 命题逻辑的可靠性 若? ? ?是有效的(可证明的),则 ? ? ?成立 命题逻辑的完备性 若? ? ?成立,则 ? ? ?是有效的 命题逻辑的可靠性和完备性 ? ? ?有效,当且仅当 ? ? ?成立 谓词逻辑的回顾 合式公式 谓词符号集合?、函数符号集合?(包括常量符号) 基于?来定义项集 t ::= x | c | f(t, …, t) 归纳地定义基于( ?, ? )的合适公式 ? ::= P(t1, t2, …, tn) | (? ? ) | (? ? ? ) | (? ? ? ) | (? ? ? ) | (?x ? ) | (? x ? ) ( P? ? ) 自由变量、约束变量、代换 谓词逻辑的回顾 新增推理规则(包括公理) 项相等的证明规则 全称量词证明规则 存在量词证明规则 量词间的等价规则 语义模型、可靠性、完备性 它们都可以基于命题逻辑相应概念进行拓展 ? ? ? 和 ? ? ?的意思与前面的一致 ? ? ? 表示?在模型?中成立 形式验证的动机 形式验证技术由三部分组成 用于系统建模的框架,通常是某种描述语言 用于描述待验证性质的规范语言 用来确立系统描述是否满足规范的验证方法 基于逻辑推理的方法 系统描述是适当逻辑中的一组公式? 待证性质的规范是另一个公式? 验证就是试图通过该逻辑的公理和推理规则来证明? ? ? 形式验证的动机 形式验证技术由三部分组成 基于逻辑推理的方法 系统描述是适当逻辑中的一组公式? 待证性质的规范是另一个公式? 验证就是通过该逻辑来证明? ? ? 基于模型的方法 系统由适当逻辑的某个模型?表示 待证性质的规范仍由公式?表示 验证就是计算模型?是否满足?(? ? ?) 形式验证的动机 形式验证技术由三部分组成 基于逻辑推理的方法 系统描述是适当逻辑中的一组公式? 待证性质的规范是另一个公式? 验证就是通过该逻辑来证明? ? ? 基于模型的方法 系统由适当逻辑的某个模型?表示 待证性质的规范仍由公式?表示 验证就是计算模型?是否满足?(? ? ?) 比基于证明方法简单,因为只考虑单个模型? 形式验证的一些特性 自动化程度 基于模型的方法高于基于逻辑的方法 性质验证和完全验证 规范可描述单个性质或全部行为 完全验证的代价要高昂得多 潜在应用领域 硬件或软件、串行或并发、反应式或终止式 开发前与开发后 开发前验证可及早发现错误,降低纠错代价 模型检测及所用逻辑概述 模型检测 基于模型的性质验证的自动化方法 最初试图用于并发、反应式系统 作为一种开发后的方法论问世 模型检测的大体步骤 由用户描述的一个模型开始 判断用户所断言的假设在模型中是否有效 若无效,则产生由执行轨迹构成的反例 模型检测及所用逻辑概述 Model checking, narrowly interpreted Decision procedures for checking if
您可能关注的文档
- 第1章 三相交流异步电动机及机械特性.ppt
- 第1章 塑料制件的设计原则.ppt
- 第1章 通信电缆的类型与结构.ppt
- 第1章 图形变换学案.doc
- 第1章 网页设计——初识网站和网页.ppt
- 第1章 移动通信基本原理.ppt
- 第1章:大众传媒与流行文化概述.ppt
- 第1章:复数与复变函数.doc
- 第1章_湿空气的物理性质及其焓湿图.ppt
- 第1章《数据库原理及应用》之演示稿绪论.ppt
- 2024年江西省寻乌县九上数学开学复习检测模拟试题【含答案】.doc
- 2024年江西省省宜春市袁州区数学九上开学学业水平测试模拟试题【含答案】.doc
- 《GB/T 44275.2-2024工业自动化系统与集成 开放技术字典及其在主数据中的应用 第2部分:术语》.pdf
- 中国国家标准 GB/T 44275.2-2024工业自动化系统与集成 开放技术字典及其在主数据中的应用 第2部分:术语.pdf
- GB/T 44285.1-2024卡及身份识别安全设备 通过移动设备进行身份管理的构件 第1部分:移动电子身份系统的通用系统架构.pdf
- 《GB/T 44285.1-2024卡及身份识别安全设备 通过移动设备进行身份管理的构件 第1部分:移动电子身份系统的通用系统架构》.pdf
- 中国国家标准 GB/T 44285.1-2024卡及身份识别安全设备 通过移动设备进行身份管理的构件 第1部分:移动电子身份系统的通用系统架构.pdf
- GB/T 44275.11-2024工业自动化系统与集成 开放技术字典及其在主数据中的应用 第11部分:术语制定指南.pdf
- 中国国家标准 GB/T 44275.11-2024工业自动化系统与集成 开放技术字典及其在主数据中的应用 第11部分:术语制定指南.pdf
- 《GB/T 44275.11-2024工业自动化系统与集成 开放技术字典及其在主数据中的应用 第11部分:术语制定指南》.pdf
文档评论(0)