《软件质量概述》PPT课件.ppt

《《软件质量概述》PPT课件.ppt》由会员分享，可在线阅读，更多相关《《软件质量概述》PPT课件.ppt（84页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、软件质量概述软件质量概述软件质量概述软件质量概述 1/82高级软件工程高级软件工程第第 七七 讲讲软件质量概述软件质量概述软件质量概述软件质量概述软件质量概述软件质量概述 2/82高级软件工程高级软件工程内内 容容 一、软件面临的问题一、软件面临的问题二、问题分析二、问题分析三、从质量到可信三、从质量到可信四、设计质量四、设计质量五、安全漏洞五、安全漏洞软件质量概述软件质量概述软件质量概述软件质量概述 3/82高级软件工程高级软件工程一、软件面临的问题一、软件面临的问题从与软件相关的一些重大事故谈起软件质量概述软件质量概述软件质量概述软件质量概述 4/82高级软件工程高级软件工程2014年年

2、3 月月 22日：日：漏洞报告平台乌云网在其官网上公布了一条网络安全漏洞信息漏洞报告平台乌云网在其官网上公布了一条网络安全漏洞信息指出指出“携程携程”安全支付日志可遍历下载安全支付日志可遍历下载导致大量用户银行卡信息泄露导致大量用户银行卡信息泄露(包含持卡人姓名身份证、银行卡号、卡包含持卡人姓名身份证、银行卡号、卡CVV码、码、6位卡位卡Bin)并称已将细节通知厂商并且等待厂商处理中并称已将细节通知厂商并且等待厂商处理中此外，携程还被曝某分站源代码包可直接下载此外，携程还被曝某分站源代码包可直接下载(涉及数据库配置和支付接口信息涉及数据库配置和支付接口信息)携程网曝支付日志漏洞携程网曝支付日志

3、漏洞软件质量概述软件质量概述软件质量概述软件质量概述 5/82高级软件工程高级软件工程CSDN 网站网站 600 万用户密码泄露万用户密码泄露继CSDN后，天涯、开心网、多玩、世纪佳缘、珍爱网、美空网、百合网、178、7K7K等知名网站也被网友爆出采用明文密码，用户数据资料被放到网上公开下载2011年年12月月21日，新浪微博爆出日，新浪微博爆出 CSDN 网站网站 600 多万用户的账多万用户的账户明文密码库泄露，当天出现迅雷快传链接户明文密码库泄露，当天出现迅雷快传链接12月月22日晚，日晚，CSDN发表声明：发表声明：向公安机关正式报案向公安机关正式报案临时关闭用户登录临时关闭用户登录并

4、要求并要求“2009年年4月以前注册的帐号，且月以前注册的帐号，且2010年年9月之后月之后没有修改过密码没有修改过密码”的用户立即修改密码的用户立即修改密码软件质量概述软件质量概述软件质量概述软件质量概述 6/82高级软件工程高级软件工程2012年年3月月20日，北京警方宣布成功侦破了曾在互联网上造成日，北京警方宣布成功侦破了曾在互联网上造成巨大影响的网站用户数据泄露案，涉案犯罪嫌疑人巨大影响的网站用户数据泄露案，涉案犯罪嫌疑人已经被刑事拘留已经被刑事拘留2012年年2月月4日，专案组在浙江温州将网民曾某抓获，曾某承日，专案组在浙江温州将网民曾某抓获，曾某承认，认，2010年年 4 月利用月

5、利用 CSDN 网站漏洞，非法侵入服务器获取网站漏洞，非法侵入服务器获取用户数据。在审查中，犯罪用户数据。在审查中，犯罪 嫌疑人曾某交代，他曾经入侵过嫌疑人曾某交代，他曾经入侵过某充值平台及某股票系统。警方介绍，在追查某充值平台及某股票系统。警方介绍，在追查 CSDN 数据库数据库泄露源头的过程中，侦查员又破获了另外起网络泄密案，泄露源头的过程中，侦查员又破获了另外起网络泄密案，先后抓获先后抓获 4 名名“黑客黑客”。关键线索：关键线索：”2010 年年 9 月，一网民发帖自称掌握月，一网民发帖自称掌握 CSDN 数据数据库，要求与公司进行合作库，要求与公司进行合作”。软件质量概述软件质量概述

6、软件质量概述软件质量概述 7/82高级软件工程高级软件工程黑客入侵深圳福彩黑客入侵深圳福彩 篡改数据欲骗篡改数据欲骗3305万巨奖万巨奖l事件：事件：2009年年6月月9日，双色球日，双色球2009066 期开奖，全国共期开奖，全国共中出一等奖中出一等奖9注，其中深圳有注，其中深圳有5注。深圳市福彩中心在开注。深圳市福彩中心在开奖（程序）结束后发现系统出现异常。经多次数据检验，奖（程序）结束后发现系统出现异常。经多次数据检验，工作人员判断，福彩中心销售系统工作人员判断，福彩中心销售系统 疑被非法入侵，中疑被非法入侵，中奖彩票数据记录被人为篡改，奖彩票数据记录被人为篡改，5注一等奖中奖数据系伪注

7、一等奖中奖数据系伪造。造。6月月10日凌晨日凌晨2时，福彩中心工作人员报案时，福彩中心工作人员报案l结果：经调查，这是一起企图利用计算机网络信息系统结果：经调查，这是一起企图利用计算机网络信息系统技术诈骗彩票奖金的案件，所涉金额高达技术诈骗彩票奖金的案件，所涉金额高达3305万元万元l原因：深圳市某信息技术公司软件开发工程师程某，利原因：深圳市某信息技术公司软件开发工程师程某，利用在深圳福彩中心实施其它技术合作项目的机会，通过用在深圳福彩中心实施其它技术合作项目的机会，通过木马攻击程序，恶意篡改彩票数据，以达到伪造双色球木马攻击程序，恶意篡改彩票数据，以达到伪造双色球一等奖中奖事实一等奖中奖事

8、实 软件质量概述软件质量概述软件质量概述软件质量概述 8/82高级软件工程高级软件工程l2007年年10月月30日，奥运门票第二阶段阶段预售首日日，奥运门票第二阶段阶段预售首日科技科技奥运？奥运？软件质量概述软件质量概述软件质量概述软件质量概述 9/82高级软件工程高级软件工程l2007年8月14日14时，美国洛杉矶国际机场电脑发生故障，60个航班的2万旅客无法入关。直至次日凌晨时分，所有滞留旅客才全部入关。l原因分析：包含旅客姓名和犯罪记录的部分数据系统(海关和边境保护系统：决定旅客是否可以进入美国领土)瘫痪 2004年9月发生过类似问题软件质量概述软件质量概述软件质量概述软件质量概述 10

9、/82高级软件工程高级软件工程l2006年3月2日14点10分，沪深大盘忽然发生罕见大跳水，7分钟之内上证指数跌去近 20 点。l原因分析：当日下午刚上市的招商银行认股权证成交量巨大，导致其行情显示时总成交量字段溢出，使其价格在股票分析软件上成为一条不再波动的直线，让市场产生了恐慌。软件质量概述软件质量概述软件质量概述软件质量概述 11/82高级软件工程高级软件工程l2005年4月20日上午10时56分，中国银联系统通信网络和主机出现故障，造成辖内跨行交易全部中断。这是2002年中国银联成立以来，首次全国性因系统故障造成的跨行交易全面瘫痪。l原因：银联新近准备上线的某外围设备的隐性缺陷诱发了跨

10、行交易系统主机的缺陷，使主机发生故障 软件能否提供支持?软件质量概述软件质量概述软件质量概述软件质量概述 12/82高级软件工程高级软件工程l2003年8月14日下午4时10分，美国及加拿大部分地区发生历史上最大的停电事故。15日晚逐步恢复l后果：经济损失250亿到300亿之间l原因分析 俄亥俄州的第一能源（FirstEnergy）公司x下属的电力监测与控制管理系统软件 XA/21 出现错误，系统中重要的预警部分出现严重故障，负责预警服务的主服务器与备份服务器连接失控，错误没有得到及时通报和处理，最终多个重要设备出现故障，导致大规模停电2003年国际十大软件质量概述软件质量概述软件质量概述软件

11、质量概述 13/82高级软件工程高级软件工程l1996年6月4日，欧洲空间局的阿丽亚娜火箭，发射后37秒爆炸。损失6亿美元l原因分析：ADA语言编写的一段程序，将一个64位浮点整数转换为16位有符号整数时，产生溢出，导致系统惯性参考系统完全崩溃软件质量概述软件质量概述软件质量概述软件质量概述 14/82高级软件工程高级软件工程l1994年12月30日，美国弗吉尼亚州 Lynchburg 大学的博士使用装有 Pentium 芯片的计算机时发现错误：（4195835/3145727)*3145727-4195835!=0l后果：Intel 花费4亿多美元更换缺陷芯片l原因：Pentium 刻录了一

12、个软件缺陷（浮点除法）软件质量概述软件质量概述软件质量概述软件质量概述 15/82高级软件工程高级软件工程2002年6月28日美国商务部的国家标准技术研究所（NIST）发布报告：“据推测，（美国）由于软件缺陷而引起的损失据推测，（美国）由于软件缺陷而引起的损失额每年高达额每年高达 595 亿美元。亿美元。这一数字相当于美国国内生产总值的这一数字相当于美国国内生产总值的 0.6%”。软件质量概述软件质量概述软件质量概述软件质量概述 16/82高级软件工程高级软件工程二、问题分析从质量谈起1、什么是质量？、什么是质量？2、什么是软件质量？、什么是软件质量？3 3、为什么软件质量保障困难？、为什么软

13、件质量保障困难？、为什么软件质量保障困难？、为什么软件质量保障困难？软件质量概述软件质量概述软件质量概述软件质量概述 17/82高级软件工程高级软件工程1、什么是、什么是“质量质量”“好坏程度好坏程度”ISO 9000(2000版版)质量是质量是（产品）的（产品）的 一组一组固有固有特性特性满足满足要求要求的的程度程度软件质量概述软件质量概述软件质量概述软件质量概述 18/82高级软件工程高级软件工程特性特性：可区分的特征可区分的特征 物理特征：机械运动、温度、电流等物理特征：机械运动、温度、电流等 化学特征：成分组合、合成、分解等化学特征：成分组合、合成、分解等固有特性固有特性：某事物中本来

14、就有的、持久的特征某事物中本来就有的、持久的特征直径、硬度、高度、频率直径、硬度、高度、频率 赋予特性：对事物增加的特性赋予特性：对事物增加的特性 价格、位置价格、位置二者有一定的相对性二者有一定的相对性软件质量概述软件质量概述软件质量概述软件质量概述 19/82高级软件工程高级软件工程要求：要求：显式要求显式要求：有明确规定的要求（行业标准或用户指定）有明确规定的要求（行业标准或用户指定）计算机屏幕尺寸计算机屏幕尺寸隐式要求：隐式要求：约定成俗的要求约定成俗的要求大楼要有楼梯大楼要有楼梯产品质量特性产品质量特性：内部特性、外部特性内部特性、外部特性满足的满足的 程度！程度！满足的满足的 成本

15、成本!软件质量概述软件质量概述软件质量概述软件质量概述 20/82高级软件工程高级软件工程2、什么是软件质量？、什么是软件质量？软件质量是：软件质量是：软件产品软件产品满足规定的和隐含的与需求能力有关的全部特征和特性满足规定的和隐含的与需求能力有关的全部特征和特性软件质量概述软件质量概述软件质量概述软件质量概述 21/82高级软件工程高级软件工程来源于来源于 Barry Boehm的软件质量模型的软件质量模型形成了形成了 ISO-9126ISO-9126的软件质量模型框架的软件质量模型框架的软件质量模型框架的软件质量模型框架影响了影响了影响了影响了 软件生存周期中的不同阶段软件生存周期中的不同

16、阶段 区分不同的软件区分不同的软件!软件质量概述软件质量概述软件质量概述软件质量概述 22/82高级软件工程高级软件工程Barry Boehm的软件质量模型的软件质量模型阐述性阐述性互用性互用性互用性互用性数据公开性数据公开性正确性正确性正确性正确性可靠性可靠性可靠性可靠性效率效率效率效率完整性完整性完整性完整性可用性可用性可用性可用性可维护性可维护性可维护性可维护性可测试性可测试性可测试性可测试性灵活性灵活性灵活性灵活性可移植性可移植性可移植性可移植性重复性重复性重复性重复性连贯性连贯性容错性容错性执行效率执行效率/储存效率储存效率存取控制存取控制/存取检查存取检查可训练可训练沟通良好沟通良

17、好 简单性简单性易操作的易操作的工具工具自我操作性自我操作性扩展性扩展性一般性一般性模块性模块性软件系统独立性软件系统独立性机器独立性机器独立性通讯公开性通讯公开性正确性正确性可操作性可操作性软件质量概述软件质量概述软件质量概述软件质量概述 23/82高级软件工程高级软件工程ISO-9126的软件质量模型框架的软件质量模型框架外部测量内部内部质量质量属性外部外部质量质量属性使用使用质量质量属性过程过程质量质量过程过程过程测量内部测量使用质量的测量软件产品软件产品软件产品的效用软件产品的效用使用条件影响影响影响依赖依赖依赖过程质量过程质量 有助于提高有助于提高 产品质量产品质量产品质量产品质量

18、有助于提高有助于提高 使用质量使用质量软件质量概述软件质量概述软件质量概述软件质量概述 24/82高级软件工程高级软件工程用户质量用户质量要求要求使用使用质量质量内部质量内部质量需求需求内部内部质量质量外部质量外部质量需求需求外部外部质量质量使用和反馈确认确认验证验证有助于确定指示指示有助于确定软件生存周期中的质量软件生存周期中的质量 软件质量概述软件质量概述软件质量概述软件质量概述 25/82高级软件工程高级软件工程外部和内部质量外部和内部质量功能性功能性可靠性可靠性易用性易用性效率效率维护性维护性可移植性可移植性适合性适合性准确性准确性互操作性互操作性保密安全性保密安全性功能性的功能性的依

19、从性依从性成熟性成熟性容错性容错性易恢复性易恢复性可靠性的可靠性的依从性依从性易理解性易理解性易学性易学性易操作性易操作性吸引性吸引性易用性的易用性的依从性依从性时间特性时间特性资源利用性资源利用性效率的依效率的依从性从性易分析性易分析性易改变性易改变性稳定性稳定性易测试性易测试性维护性的维护性的依从性依从性适应性适应性易安装性易安装性共存性共存性易替换性易替换性可移植性的可移植性的依从性依从性*的依从性：的依从性：软件产品遵循与软件产品遵循与*相关的标准、约定或法规以及类似规定的能力相关的标准、约定或法规以及类似规定的能力软件质量概述软件质量概述软件质量概述软件质量概述 26/82高级软件工

20、程高级软件工程使用质量使用质量有效性有效性生产率生产率安全性安全性满意度满意度软件质量概述软件质量概述软件质量概述软件质量概述 27/82高级软件工程高级软件工程3、为什么软件质量保障困难？、为什么软件质量保障困难？（1）软件产品与需求符合的程度）软件产品与需求符合的程度（2）软件的本质）软件的本质（3）软件度量困难）软件度量困难软件质量概述软件质量概述软件质量概述软件质量概述 28/82高级软件工程高级软件工程（1）软件产品与需求符合的）软件产品与需求符合的程度程度需求与需求与成本之间的矛盾成本之间的矛盾需求是永无止境的需求是永无止境的成本是永远有限的成本是永远有限的微软：质量只要好到能使大

21、量的产品卖给客户微软：质量只要好到能使大量的产品卖给客户NASA：可靠性要达到：可靠性要达到 99.999%Motorola：6 软件产品属性完全满足用户需求是不现实的软件产品属性完全满足用户需求是不现实的 软件质量概述软件质量概述软件质量概述软件质量概述 29/82高级软件工程高级软件工程（2）软件的本质）软件的本质规模、复杂性、演化性规模、复杂性、演化性网络环境网络环境软件研发过程缺乏基础理论支撑软件研发过程缺乏基础理论支撑软件产品的验证缺乏基础理论支持软件产品的验证缺乏基础理论支持软件质量概述软件质量概述软件质量概述软件质量概述 30/82高级软件工程高级软件工程（3）软件度量困难）软件

22、度量困难 “You cant control what you dont measure”Tom DeMarco,1982对比物理属性：尺子、秤、时钟、温度计、测速仪对比物理属性：尺子、秤、时钟、温度计、测速仪 它们的发展过程它们的发展过程!代码、过程、组织代码、过程、组织度量无处不在！度量无处不在！软件质量概述软件质量概述软件质量概述软件质量概述 31/82高级软件工程高级软件工程三、从质量到可信三、从质量到可信1、什么是可信？2、什么样的软件是可信的？Compaq、HP、IBM、Intel和和Microsoft等发起等发起(1999):Trusted Computing Platform

23、Alliance 后来增加软件：后来增加软件：Trusted Computing Group（2003）微软倡导微软倡导(2002):Trustworthy Computing软件质量概述软件质量概述软件质量概述软件质量概述 32/82高级软件工程高级软件工程1、什么是可信？TrustedTrustworthyDependabilityConfidenceAssurance一个实体在实现给定目标时，其行为与结果总是可以预期的一个实体在实现给定目标时，其行为与结果总是可以预期的软件质量概述软件质量概述软件质量概述软件质量概述 33/82高级软件工程高级软件工程可信软件软件是可信的,如果:其服务总

24、是与用户的预期相符(质量?)即使在运行过程中出现一些特殊情况软件质量概述软件质量概述软件质量概述软件质量概述 34/82高级软件工程高级软件工程1、硬件环境（计算机、网络）发生故障2、低层软件（操作系统、数据库）出现错误 3、其它软件（病毒软件、流氓软件）对其产生影响4、出现有意（攻击）、无意（误操作）的错误操作什么特殊情况?软件质量概述软件质量概述软件质量概述软件质量概述 35/82高级软件工程高级软件工程2、什么样的软件是可信的？可用功能：正确、不少、不多可靠性（容错）：高安全性（机密性、完整性）：高响应时间（从输入到输出）：小维护费用（监测、演化）：小软件质量概述软件质量概述软件质量概述

25、软件质量概述 36/82高级软件工程高级软件工程质量与可信（1）l可信更多关主体与客体的关系是系统“承诺”与实际表现的符合程度。存在这样一种情形，质量不是很高，但有具体的说明，仍然有高的可信性。同一个系统的质量是确定的，但对不同主体的可信度可能不一样：一个受侵害的系统，对于实际用户是不可信的，对于黑客是可信的对于同一个系统，当用户对其信息掌握得有限时，可信度低，掌握了较多的正面信息时，可信度提升软件质量概述软件质量概述软件质量概述软件质量概述 37/82高级软件工程高级软件工程质量与可信（2）l质量主要是针对客体自身而言的质量与可信之间的关系 类似于 软件与服务之间的关系服务、可信服务、可信

26、更多地关注更多地关注 主体：最终用户主体：最终用户软件、质量软件、质量 更多地关注更多地关注 客体：软件自身客体：软件自身软件质量概述软件质量概述软件质量概述软件质量概述 38/82高级软件工程高级软件工程1、例子2、模型检测概述3、模型检测算法概览4、模型检测工具四、设计质量四、设计质量软件质量概述软件质量概述软件质量概述软件质量概述 39/82高级软件工程高级软件工程Needham-Schroeder 身份认证协议身份认证协议N,S1ZS1,S2NS2Z通信过程可能被窃听！加密可以防止窃听！如何约定加密数字？每人 有自己的标识：N每人 公布自己的公钥:只有N才能解开的消息：*N每个对话过程

27、 用一对数字对内容加密:S1,S2每次对话前 需要首先建立这对数字该协议于1978年被提出并得到广泛应用NZ1、例子、例子软件质量概述软件质量概述软件质量概述软件质量概述 40/82高级软件工程高级软件工程N,S1WS1,S2NS2WN,S1ZS1,S2NS2Z1996年，发现该协议存在设计缺陷：年，发现该协议存在设计缺陷：攻击者可以伪装一方的身份攻击者可以伪装一方的身份利用模型检测方法！利用模型检测方法！被欺骗！被欺骗！不可信！不可信！开始伪装开始伪装ZWN软件质量概述软件质量概述软件质量概述软件质量概述 41/82高级软件工程高级软件工程1992 年，美国年，美国CMU 的的 Clarke

28、 和学生尝试用和学生尝试用 SMV 验验证证IEEE Future+cache coherence 协议协议 发现协议设计中的几个以前未被发现的错误发现协议设计中的几个以前未被发现的错误 这是这是 首次首次 用形式化方法发现用形式化方法发现 IEEE 标准中的错误标准中的错误 尽管从尽管从1988年就开始制定协议，以前都是使用非形年就开始制定协议，以前都是使用非形式化的方法验证协议式化的方法验证协议软件质量概述软件质量概述软件质量概述软件质量概述 42/82高级软件工程高级软件工程1992年，美国斯坦福大学的年，美国斯坦福大学的 Dill 和学生用和学生用 Murphito 验证验证 IEEE

29、 cache coherence 协议中的协议中的Scalable Coherent 接口接口 发现了几个错误，包括未初始化的变量和逻辑错误等发现了几个错误，包括未初始化的变量和逻辑错误等 在上述协议的完整版也存在错误，尽管协议被深入地在上述协议的完整版也存在错误，尽管协议被深入地讨论、模拟甚至实现讨论、模拟甚至实现软件质量概述软件质量概述软件质量概述软件质量概述 43/82高级软件工程高级软件工程AT&T 的 NewCoRe 项目(89-92)第一个将形式化验证方法应用于软件项目 在CCITT ISDN User Part 协议的开发中，使用了一个特殊的 model checker 5个“验

30、证工程师”分析了 145 条需求 7,500 lines of SDL 源码被验证 发现了112 个错误，大约55%的院士设计需求存在逻辑不一致软件质量概述软件质量概述软件质量概述软件质量概述 44/82高级软件工程高级软件工程ACM 2007年度图灵奖（年度图灵奖（Turing Award）Edmund M.Clarke,E Allen Emerson,Joseph Sifakisl1981年，美国的年，美国的Edmund Clarke和和Allen Emerson以及以及在法国的在法国的Sifakis分别提出了模型检测（分别提出了模型检测（Model Checking）的最初概念）的最初概

31、念l他们开发了一套用于判断硬件和软件设计的理论模型他们开发了一套用于判断硬件和软件设计的理论模型是否满足规范的方法是否满足规范的方法l当系统检测失败时，还能利用它确定问题存在的位置当系统检测失败时，还能利用它确定问题存在的位置软件质量概述软件质量概述软件质量概述软件质量概述 45/82高级软件工程高级软件工程软件设计模型？Statecharts 用于软件？用于软件？软件代码？Use static analysis to extract a finite state synchronization skeleton from the program.Model check the result.

32、Bandera-Kansas State Java PathFinder-NASA Ames Slam Project(Bebop)-Microsoft软件质量概述软件质量概述软件质量概述软件质量概述 46/82高级软件工程高级软件工程2、模型检测概述、模型检测概述1）基本情况）基本情况2）什么是模型检测）什么是模型检测3）基本思想）基本思想4）过程描述）过程描述软件质量概述软件质量概述软件质量概述软件质量概述 47/82高级软件工程高级软件工程l产生产生 20世纪80年代初，Clarke,Emerson等提出了用于并发系统性质的CTL逻辑，设计了检测有穷状态系统是否满足给定CTL公式的算法l

33、特性特性能给出反例自动化程度高l应用应用计算机硬件、通信协议、控制系统、安全认证协议、软件安全 等1）基本情况）基本情况软件质量概述软件质量概述软件质量概述软件质量概述 48/82高级软件工程高级软件工程l定义定义Clarke&Emerson 1981“Model checking is an automated technique that,given a finite-state model of a system and a logical property,systematically checks whether this property holds for(a given ini

34、tial state in)that model.”给定一个系统的有限状态模型，和一个逻辑性质，系统地检测：这个模型（含初始状态）满足该性质2）什么是模型检测）什么是模型检测软件质量概述软件质量概述软件质量概述软件质量概述 49/82高级软件工程高级软件工程3）基本思想）基本思想 （1）用状态迁移系统）用状态迁移系统(S)表示系统的行为，用模态表示系统的行为，用模态/时序逻辑公式时序逻辑公式(F)描述系统的性质。描述系统的性质。（2）“系统是否具有某种期望的性质系统是否具有某种期望的性质”就转化数学就转化数学问题问题“状态迁移系统状态迁移系统S是否是公式是否是公式F的一个模型？的一个模型？”公

35、公式表示：式表示：S|=F?对于有限状态迁移系统，这个问题是可以判定的。对于有限状态迁移系统，这个问题是可以判定的。软件质量概述软件质量概述软件质量概述软件质量概述 50/82高级软件工程高级软件工程4）过程描述）过程描述OKError traceor1、建立模型、建立模型Finite-state model2、描述系统性质、描述系统性质Temporal logic formula3、输入工具、输入工具Model Checker (F W)Line 5:Line 12:Line 15:Line 21:Line 25:Line 27:Line 41:Line 47:软件质量概述软件质量概述软件质

36、量概述软件质量概述 51/82高级软件工程高级软件工程3、模型检测算法概览、模型检测算法概览1）系统的表示（建立模型）系统的表示（建立模型）2）属性的表示（描述系统性质）属性的表示（描述系统性质）3）搜索状态空间（工具分析）搜索状态空间（工具分析）2个例子：CTL 与 LTL软件质量概述软件质量概述软件质量概述软件质量概述 52/82高级软件工程高级软件工程1）系统的表示）系统的表示通常用有限状态自动机通常用有限状态自动机通常用有限状态自动机通常用有限状态自动机l状态集合状态集合Ss1,s2,s3l标记标记(观察观察)集合集合Ap,ql迁移关系迁移关系 S Ss1 s2,l标记函数标记函数L:

37、S P(A)L(s1)=p,软件质量概述软件质量概述软件质量概述软件质量概述 53/82高级软件工程高级软件工程例子例子:微波炉系统微波炉系统StartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatError1324675start ovenopen dooropen doorclose dooropen doorcookwarmupstart ovenresetstart cookingclos

38、e door软件质量概述软件质量概述软件质量概述软件质量概述 54/82高级软件工程高级软件工程2）属性表示）属性表示(Property Specification)用各种模态用各种模态/时序逻辑表示：时序逻辑表示：线性时序逻辑线性时序逻辑（LTL:Linear Temporal Logic）计算树逻辑（计算树逻辑（CTL:Computation Tree Logic）模态命题模态命题 u-演算（演算（u-Calculus）主要检测属性类型：主要检测属性类型：安全性（安全性（safety）：坏的事情不会发生。例如：无死锁）：坏的事情不会发生。例如：无死锁活性（活性（liveness）：好的事情

39、终会发生。例如：请求响应）：好的事情终会发生。例如：请求响应公平性（公平性（fairness）：）：一致性（一致性（consistency）：）：软件质量概述软件质量概述软件质量概述软件质量概述 55/82高级软件工程高级软件工程LTL（线线性性时态逻辑时态逻辑）的特点）的特点将将时间时间建模成状建模成状态态的序列，无限延伸到未来的序列，无限延伸到未来该该状状态态序列称序列称为计为计算路径或路径算路径或路径使用指示未来的使用指示未来的连连接接词词未来一般不确定，出未来一般不确定，出现现若干可能路径若干可能路径主要主要时态连时态连接接词词：下一个状下一个状态态(X)未来某状未来某状态态(F)未来

40、所有状未来所有状态态(G)直到直到(U)软件质量概述软件质量概述软件质量概述软件质量概述 56/82高级软件工程高级软件工程几个例子：几个例子：G(started ready)永永远远不可能不可能“尚未就尚未就绪绪”就就“已已经经启启动动”了了G(requested F acknowledged)对资对资源的源的请请求最求最终终会得到确会得到确认认G F enabled在每条在每条计计算路径上算路径上,某某进进程无限多次程无限多次处处于于enabledF G deadlock某某进进程最程最终终会被永久地死会被永久地死锁锁软件质量概述软件质量概述软件质量概述软件质量概述 57/82高级软件工程

41、高级软件工程lLTL表达不了的事情表达不了的事情从任何状从任何状态态出出发发，都可能（即存在一条路径）到，都可能（即存在一条路径）到达重新启达重新启动动状状态态电电梯可以在第梯可以在第3层层保持关保持关门闲门闲置（即存在一条从置（即存在一条从该层该层到到该层该层的路径，沿的路径，沿该该路径路径电电梯停留在原地）梯停留在原地）表达表达这这些事情需要些事情需要对对路径使用存在量路径使用存在量词词，可以采，可以采用用计计算算树逻辑树逻辑解决解决软件质量概述软件质量概述软件质量概述软件质量概述 58/82高级软件工程高级软件工程A(Always):对所有分支G(Global):现在和以后所有状态 E(

42、Exist):对于某一个分支U(Until):直到某一状态F(Future):现在和以后某一状态X(Next-Time):CTL（计计算算树逻辑树逻辑）特点）特点时间时间建模建模为树为树状状结结构，未来有不同的路径构，未来有不同的路径软件质量概述软件质量概述软件质量概述软件质量概述 59/82高级软件工程高级软件工程For any reachable state:if “Start”holds,then along all outgoing paths,“Heat”eventually holds.AG(Start AF Heat)微波炉系统的一个命题：微波炉系统的一个命题：只要按了只要按了只

43、要按了只要按了“启动启动启动启动”，最终总会加热，最终总会加热，最终总会加热，最终总会加热软件质量概述软件质量概述软件质量概述软件质量概述 60/82高级软件工程高级软件工程3）搜索状态空间）搜索状态空间逻辑表达式转换：E(Exist):对于某一个分支U(Until):直到某一状态G(Global):现在和以后所有状态 A(Always):对所有分支F(Future):现在和以后某一状态X(Next-Time):EF(Start EG Heat)AG =EF()AF =A(true U)A(U)=.AG(Start AF Heat)软件质量概述软件质量概述软件质量概述软件质量概述 61/82高

44、级软件工程高级软件工程StartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatError1324675start ovenopen dooropen doorclose dooropen doorcookwarmupstart ovenresetstart cookingclose doorEF(Start EG Heat)1.S(Start)=2,5,6,72.S(Heat)=1,2,3,5,6

45、3.S=S(Heat)=1,2,3,5,6 SCC=1,2,3,5T=1,2,3,5 =S(EG Heat)=1,2,3,54.S=2,55.S=1,2,3,4,5,6,76.S=软件质量概述软件质量概述软件质量概述软件质量概述 62/82高级软件工程高级软件工程Needham-Schroeder 身份认证协议身份认证协议mtype=msg1,msg2,msg3,alice,bob,intruder,nonceA,nonceB,nonceI,keyA,keyB,keyI,ok;typedef Crypt /*the encrypted part of a message*/mtype key,

46、d1,d2;chan network=0 of mtype,/*msg#*/mtype,/*receiver*/Crypt;mtype partnerA,partnerB;mtype statusA,statusB;/*Knowledge about nonces gained by the intruder.*/bool knowNA,knowNB;(http:/www.loria.fr/merz/papers/NeedhamSchroder.spin)利用 Promela（protocol meta language）语言描述系统模型：软件质量概述软件质量概述软件质量概述软件质量概述 63

47、/82高级软件工程高级软件工程active proctype Alice()/*honest initiator for one protocol run*/mtype partner_key,partner_nonce;Crypt data;if/*nondeterministically choose a partner for this run*/:partnerA=bob;partner_key=keyB;:partnerA=intruder;partner_key=keyI;fi;d_step /*Construct msg1 and send it to chosen partne

48、r*/data.key=partner_key;data.d1=alice;data.d2=nonceA;network!msg1(partnerA,data);软件质量概述软件质量概述软件质量概述软件质量概述 64/82高级软件工程高级软件工程/*wait for partner to send back msg2 and decipher it*/network?msg2(alice,data);end_errA:/*make sure the partner used As key and that the first nonce matches,otherwise block.*/(d

49、ata.key=keyA)&(data.d1=nonceA);partner_nonce=data.d2;d_step /*respond with msg3 and declare success*/data.key=partner_key;data.d1=partner_nonce;data.d2=0;network!msg3(partnerA,data);statusA=ok;/*proctype Alice()*/软件质量概述软件质量概述软件质量概述软件质量概述 65/82高级软件工程高级软件工程active proctype Bob()/*honest responder for o

50、ne run*/mtype partner_key,partner_nonce;Crypt data;network?msg1(bob,data);end_errB1:(data.key=keyB);partnerB=data.d1;d_step partner_nonce=data.d2;if :(partnerB=alice)-partner_key=keyA;:(partnerB=bob)-partner_key=keyB;/*shouldnt happen*/:(partnerB=intruder)-partner_key=keyI;fi;/*respond with msg2*/da