模型检验技术

《模型检验技术》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

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

2、成为十分迫切的需求。欧洲阿丽亚娜5型火箭1996年6月4日因软件失效在发射40秒后爆炸，原因是惯性参考系统软件的数据转换异常造成的失效。美国F-22猛禽战斗机2007年2月9日同样因软件问题延迟在日本部署2004年12月20日，美空军第422测试评估大队的一架F-22战斗机因软件问题在起飞过程中失控坠毁。美国电力监测与控制管理系统多计算机系统试图同时访问同一资源引起的软件失效美国空管软件原因是空管软件时钟缺陷东京证券交易软件2005年11月1日，东京证券交易所因为软件升级出现系统故障，导致早间股

3、市“停摆”。“熊猫烧香”病毒近乎一夜之间，该病毒使上百万台计算机感染并遭到破坏互联网软件安全的几个数据•约80%的家庭用户感染了Spyware•美国2004年网络犯罪非法谋利105亿美元•50%以上的安全漏洞是由软件缺陷引起的误杀百万电脑诺顿致歉由于误将中文WindowsXP中的系统文件当作木马程序屏蔽掉，2007年5月17日和18日，诺顿杀毒软件导致全部安装了该软件的计算机系统瘫痪。根据保守估计，被误杀的电脑在中国内地不下百万台。昨天，诺顿产品的母公司赛门铁克公司发表声明，向用户致歉并发布了官

4、方解决方案。2002年NIST估计软件造成美国年经济损失约600亿美元，GDP的0.6%我们的信息基础设施正建立在脆弱的软件之上为什么？•软件的根本问题：任何机构和个人都无法确保所开发的软件一定没有问题。Microsoft的承诺•就间接损害不赔付责任：–在法律所允许的最大范围内，MicrosoftCorporation或其他供应商绝不就因使用或不能使用本“软件产品”所发生的其他损害负赔偿责任，即使MicrosoftCorporation事先被告知该损害发生的可能性。•若为Windows的每一次B

5、ug出现赔偿1美分，比尔盖茨早已一贫如洗。建立人与机器之间的信任关系•计算机系统（软件系统）：数学系统生物系统•人与机器之间的关系人与人之间的关系可信性与可信软件•可信性即“可信任的”，是实体的一种属性。一个实体的行为总以预期方式达到既定目标，称其为可信的。•可信软件软件系统的行为符合人们的预期，在受到干扰（外部攻击、错误操作或环境影响）时，具有连续提供服务的能力。–可靠性（relibilitliability）–安全性（security）–防危性（safety）–可维护性（maintainab

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

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

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