模型检验技术

《模型检验技术》由会员分享，可在线阅读，更多相关《模型检验技术（60页珍藏版）》请在金锄头文库上搜索。

1、模型检验技术 李 宣 东李 宣 东 南京大学计算机科学与技术系 提纲 软件可信性 形式化方法 模型检验概述 软件系统的模型检验软件系统的模型检验 实时和混成系统的模型检验 实时和混成系统的模型检验 研究背景：提高软件可信性 随着计算机技术在各行各业应用的日益普及, 计算机已经渗透到我们工作和生活的方方面计算机已经渗透到我们工作和生活的方方面 面，成为我们工作和生活的一部分，从而极 大地促进了社会的发展和生产力的提高。 与此同时，工作在我们身边的各种计算机系 统由于其中的软件系统失效经常表现不尽人统由于其中的软件系统失效经常表现不尽人 意，呈现出脆弱、难以信任的特征，甚至造 成不可挽回的损失，因

2、此研究相关的可信软 件关键技术以提高软件系统的可信性已经成 为十分迫切的需求。 欧洲阿丽亚娜 型火箭欧洲阿丽亚娜5型火箭 1996年6月4日 因软件失效在因软件失效在 发射40秒后爆 炸原因是惯炸，原因是惯 性参考系统 软件的数据软件的数据 转换异常造 成的失效成的失效。 美国22猛禽战斗机美国F-22猛禽战斗机 2007年2月9 日同样因软 件问题延迟 在日本部署 2004年12月20日美空军第422测试评估大队的2004年12月20日，美空军第422测试评估大队的一 架F-22战斗机因软件问题在起飞过程中失控坠毁。 美国电力监测与控制管理系统美国电力监测与控制管理系统 多计算机多计算机 系

3、统试图 同时访问同时访问 同一资源 引起的软引起的软 件失效 美国空管软件美国空管软件 原因是 空管软空管软 件时钟 缺陷缺陷 东京证券交易软件 2005年11月1日， 东京证券交易所 因为软件升级出因为软件升级出 现系统故障，导 致早间股市“停早间市停 摆”。 “熊猫烧香”病毒“熊猫烧香”病毒 近乎一夜之 间该病毒间，该病毒 使上百万台 计算机感染计算机感染 并遭到破坏 互联网软件安全的几个数据互联网软件安全的几个数据 约80%的家庭用户感染了Spyware 美国2004年网络犯罪非法谋利105亿美元 50%以上的安全漏洞是由软件缺陷引起的 50%以上的安全漏洞是由软件缺陷引起的 误杀百万电

4、脑 诺顿致歉 由于误将中文Windows XP 中的系统文件当作木马程序 屏蔽掉，2007年5月17日和 18日，诺顿杀毒软件导致全 部安装了该软件的计算机系部安装了该软件的计算机系 统瘫痪。根据保守估计，被 误杀的电脑在中国内地不下误杀的电脑在中国内地不下 百万台。昨天，诺顿产品的 母公司赛门铁克公司发表声 明，向用户致歉并发布了官 方解决方案。 2002年NIST估计软件 造成美国年经济损失 约600亿美元，GDP的 0.6% 我们的信息基础设施我们的信息基础设施我们的信息基础设施我们的信息基础设施 正建立在脆弱的软件之上正建立在脆弱的软件之上正建立在脆弱的软件之上正建立在脆弱的软件之上

5、为什么？ 软件的根本问题： 任何机构和个人都无法确保所开发的软件一 定没有问题。定没有问题。 Microsoft的承诺 就间接损害不赔付责任： 在法律所允许的最大范围内，Microsoft Corporation 或其他供应商绝不绝不就因使用或不能使用本“软件产 品”所发生的其他损害负赔偿责任即使Mif品”所发生的其他损害负赔偿责任，即使Microsoft Corporation事先被告知该损害发生的可能性。 若为Windows的每一次Bug出现赔偿1美分，比 尔盖茨贫如洗尔盖茨早已一贫如洗。 建立人与机器之间的信任关系 计算机系统（软件系统）： 数学系统生物系统数学系统生物系统 人与机器之间

6、的关系 人与人之间的关系人与人之间的关系 可信性与可信软件 可信性 即“可信任的”是实体的一种属性一个实体的即可信任的，是实体的种属性。个实体的 行为总以预期方式达到既定目标，称其为可信的。 可信软件 软件系统的行为符合人们的预期，在受到干扰 （外部攻击错误操作或环境影响）时具有连续提（外部攻击、错误操作或环境影响）时，具有连续提 供服务的能力。 可靠性（ li bilit ） 可靠性（reliability） 安全性（security） 防危性（safety） 可维护性（maintainability）可维护性（maintainability） 可用性（availability） 容错性（f

7、ault tolerance） 生存性（survivability） 提高软件系统的可信性 软件系统的认识与理解 分析 分析 测试 验证 软件过程的管理与控制 过程管理 质量控制 软件系统的运行保障 容错 容错 监控 软件过程的管理与控制 软件质量定义 明确声明的功能和性能需求明确文档化过的开发标准以明确声明的功能和性能需求、明确文档化过的开发标准、以 及专业人员开发的软件所应具有的所有隐含特征都得到满足。 软件过程管理 软件过程管理 软件配置管理 软件配置管理 软件项目管理 软件项目管理 软件质量保障 软件质量保障 软件系统的运行保障 容错 监控 根据软件系统运行过程中产生的动态信息检验软件

8、 根据软件系统运行过程中产生的动态信息，检验软件 系统是否具备相关的性质 在线监控（Online）， Monitoring-Oriented PiProgramming 离线监控（Offline） 多核CPU的发展对软件容错和监控提供了强有力 的支持的支持 软件系统的认识与理解-软件分析 软件分析主要是指针对程序和相关制品的分析， 主要包括静态分析和动态分析主要包括静态分析和动态分析。 静态分析技术是指通过对程序代码进行扫描分 静态分析技术是指通过对程序代码进行扫描分 析而获得程序相关性质的技术。 动态分析技术通过对程序的执行来获得程序的 相关性质般与程序切片调试和测试技术相关性质，一般与程序

9、切片、调试和测试技术 相结合。 软件系统的认识与理解-软件分析 软件分析技术的作用主要体现在两个方面： 通过检测系统中的错误而提高软件的可靠性 通过检测系统中的错误而提高软件的可靠性 通过检测系统的安全漏洞来提高软件的安全性。 很多软件系统的错误来自于对指针或内存的误用，比如 内存泄漏和缓冲区溢出。还有一些错误和并发相关，比 如死锁以及数据共享错误这些错误很难通过测试发现如死锁以及数据共享错误。这些错误很难通过测试发现。 软件系统的安全性漏洞主要有三种类型：访问控制漏洞、软件系统的安全性漏洞主要有三种类型：访问控制漏洞、 敏感信息的泄漏、因为程序设计疏忽而导致的安全漏洞、 以及因为某些API的

10、误用而导致的安全漏洞。 软件系统的认识与理解-软件测试 以运行系统为主要手段发现系统错误 只能发现系统的错误，不能证明系统没有错，无法回 答系统一定没有错误这样一类问题答系统定没有错误这样类问题 工业界常用的途径，成本高，代价大工业界常用的途径，成本高，代价大 仿真（Simulation）：以运行系统模型为主要手段发现 系统错误 软件验证 建立系统模型，确认系统模型是否存在错误 可以从某一个角度回答系统一定没有错误这样可以从某个角度回答系统定没有错误这样 一类问题，从而进一步提高我们对系统可靠性 的可信度信度 基于形式化方法 基于形式化方法 形式化方法（Formal Methods） 形式化方

11、法是指为说明和验证复杂计算机系 统所采用的基于数学的语言技术和具统所采用的基于数学的语言、技术和工具。 形式化方法不能确保系统的可靠性，但其可 以通过揭示系统的不一致性歧义性和不完以通过揭示系统的不一致性、歧义性和不完 备性来增加我们对系统的理解程度，从而提 高我们对系统可靠性的可信度高我们对系统可靠性的可信度。 形式验证 形式化方法包括： 规约（specification） 验证（verification）验证（verification） 形式验证包括： 模型检验（d l hki）模型检验（model checking） 推理验证（theorem proving）pg 模型检验 模型检验是一

12、种自动验证有穷状态系统的技术。 模型检验的基本思想是通过遍历系统模型的状 态空间来检验系统模型是否满足给定的性质态空间来检验系统模型是否满足给定的性质。 模型检验技术的创始人（1981）： EM Clarke, EA Emerson (USA) JP Quielle, J Sifakis (France) 模型检验 在模型检验中涉及两种形式说明语言： 性质说明语言用于描述系统的性质; 模型描述语言用于描述系统的模型模型描述语言用于描述系统的模型。 模型检验技术用于检验由模型描述语言 描述的系统模型是否满足由性质说明语描述的系统模型是否满足由性质说明语 言描述的系统性质。 模型检验的过程 建模（

13、Modeling） 规约（Specification） 规约（Specification） 验证（Verification） 模型检验 OK Finite-state model or Model Checker ( ) Error trace Line 5: Temporal logic formula () Line 5: Line 12: Line 15: Line 21: Line 25: Line 27: Line 41: Line 47: 模型检验中的关键技术问题 模型检验中的关键技术问题是如何设计数据结 构和算法用以表示和遍历大规模的系统模型构和算法，用以表示和遍历大规模的系统模

14、型 状态空间。 解决由多个系统模型的并行组合而形成的状态解决由多个系统模型的并行组合而形成的状态 空间爆炸问题。 解决状态空间爆炸问题的途径 符号化模型检验技术 （Symbolic representation of state space） 偏序规约技术（Partial order reduction） 偏序规约技术（Partial order reduction） On-the-fly技术 对称技术（Symmetry） 抽象和组合技术（Ab tti& 抽象和组合技术（Abstraction & Composition） 符号化模型检验技术 1993年KL McMillan基于RE Byra

15、nt的有序二叉 判定图（OBDD）来有效地表示状态迁移系统判定图（OBDD）来有效地表示状态迁移系统， 提出了符号化模型检验，大大地提高了可有效 应用模型检验技术的系统规模（10 120） 使得模应用模型检验技术的系统规模（10），使得模 型检验在工业界逐步得到应用。 用布尔公式刻画状态集合和状态对集合，用 OBDD来表示这些布尔公式，使用OBDD上的OBDD来表示这些布尔公式，使用OBDD上的 布尔操作来计算谓词转换子（其不动点刻画了 CTL模态子），从而使模型检验在压缩了的符模子，从使模检在缩的符 号化状态空间上来验证CTL性质。 偏序规约技术 通过发掘系统中并发执行的迁移的交换 性，减少

16、本质上相同的状态，从而仅生 成足以检验性质的小部分状态空间 。成足以检验性质的小部分状态空间 On-the-fly技术 把状态空间生成和检验它是否满足性质 合在一起做，而不去预先生成整个状态 空间，从而尽可能避免状态爆炸。空间，从而尽可能避免状态爆炸 对称技术 针对由多个完全类似的进程组成的系统， 利用其模型的状态空间的对称性来生成 压缩的且对模型检验等价的模型压缩的对模型检验等价的模型 抽象和组合技术 抽象方法通过把原来模型中与待验证性质无关 的信息去掉而获得简化模型的方式来减小模型的信息去掉而获得简化模型的方式来减小模型 检验时问题的规模，抽象必须是保持性质的， 即若简化的模型满足性质则原来的模