《软件形式化方法》PPT课件

单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,*,软件形式化方法,陈铁明,/,王婷,课程介绍,通过本课程的学习，使同学了解软件开发中形式化方法的基本概念和原理，掌握几种常用的软件系统形式化描述方法（有限状态机、CSP、Z语言、时序逻辑等）和验证方法，并能够应用这些技术对软件系统进行形式描述和分析。,分析问题、解决问题的能力，锻炼逻辑思维。,课程参考教材,软件开发的形式化方法，古天龙编，2005，高等教育出版社,课程PPT,课程考核,总成绩,=,课程作业（,50%,）,+,期末考试（,50%,）,形式化思想,广义上，舍弃事物物质内容，只取形式结构，只考虑形式不考虑内容的一种看待、处理问题的思想。,以数学为例，可以表示为完全形式化的东西，一切数学都可以由符号加以形式地表述。,概念形式化：,原理形式化：勾股定理,在三角形,ABC,中，,C=90,。,，则三条边,a,b,c,满足,a,2,+b,2,=c,2,具有两个基本特点：,自然语言符号化，抽象概括为形式语言；,对直观意义的推理关系进行语义刻画和语法刻画。,例子：电梯控制系统,（自然语言描述）,6,例子：UML描述（半形式化）,一种具有良好语法和语义定义的形式描述方法,但,无法或很少支持,以数学为基础的,形式,分析和推理过程,7,例子：电梯控制系统,（程序语言描述）,8,例子：电梯控制系统,（有限状态机描述）,一种具有良好语法和语义定义的形式描述方法,有效支持,以自动机理论为基础的,形式,化验证,过程,9,软件的规约表示,软件的规约表示可以采用非形式化的方式来描述，包括自然语言、图、表等，也可以采用形式化方式来描述。,由于,非形式化方法,本身所存在的矛盾、二义性、含糊性，以及描述规约时的不完整性、抽象层次混杂等情况，使得所得到的,规约不能准确地刻画系统模型,，甚至会为后来的软件开发埋下出错的隐患。,而对于,形式化方法,来说，由于其基于严格的数学，具有严格的语法和语义定义，从而可以,准确地描述系统模型,，排除了矛盾、二义性、含糊性等情况，最终得到一个相对完整、正确的系统模型。,10,软件危机,1968,年，,NATO,会议提出了“软件危机”一词,软件危机包含两方面问题,如何开发软件，以满足不断增长、日趋复杂的需求；,如何维护数量不断膨胀的软件产品。,软件危机主要表现如下几个方面,开发成本昂贵,项目进度难控,修改维护困难,质量无法保证,11,项目进度难控,为软件开发制定进度是很困难的事情。如有10人月的工作量，则由一个人完成需要10个月，由10个入完成则需要一个月。但这种工作量估计方式仅对各部分工作互下干扰的情况下才适用，但作为整体，尚需讨论合作，这种讨论交流活动就增加了工作量。软件系统的结构很复杂，各部分附加联系极大。,Brook,提出的法则,“在已拖延的软件项目上增加入力只会使其更难按期完成”,。,1995,年，美国共取消,810,亿美元的软件项目，其中,31%,未完取消，,53%,的项目延长一半时间，,9%,按期完成且不超期。,1998,年，美国企业应用项目,28%,的项目取消，,40%,无限拖长且资金超出预算。,2008,年的数据显示，按时、在预算内交付，并且完成了应有功能的成功项目只有,32%,。,12,软件维护困难,软件的维护任务特别重。,正式投入使用的商用软件，总是存在着一定数量的错误。随着时间延伸，在不同的运行条件下，软件就会出故障，就需要修改维护。,软件维护不是更换某种备件，而是要纠正逻辑缺陷。当软件系统变得庞大，问题变得复杂时，常常会发生,“,纠正一个错误带来更多新的错误！”,13,典型的软件项目开发,14,质量无法保证,Therac-25,是加拿大原子能公司,AECL,和一家法国公司,CGR,联合开发的一种医疗设备，它产生的高能光束或电子流能够杀死人体毒瘤而不会伤害毒瘤附近的人体健康组织。在1985年6月到1987年1月，因为软件缺陷引发了6起由于电子流或,X-,光束的过量使用的医疗事故，造成4人死亡、2人重伤的严重后果。,1996年，欧洲航天局,阿丽亚娜5型（,Ariane5）,火箭在发射后40秒钟后发生爆炸，2名法国士兵当场死亡，损耗资产达10亿美元之巨，历时9年的航天计划因此严重受挫。爆炸原因在于惯性导航系统软件技术要求和设计的错误。,2011,年,7,月,23,日,20,时,30,分,05,秒，由北京南站开往福州站的,D301,次列车与杭州站开往福州南站的,D3115,次列车发生动车组列车追尾事故，造成,40,人死亡、,172,人受伤，中断行车,32,小时,35,分，直接经济损失,19371.65,万元。根据初步掌握的情况分析，“,723”,动车事故是由于温州南站信号设备在设计上存在严重缺陷，遭雷击发生故障后，导致本应显示为红灯的区间信号机错误显示为绿灯。,15,软件质量的重要方面,16,如何解决软件危机,软件工程方法,Software Engineering,软件工程：工程化软件开发过程控制与管理，追求软件设计、生产、维护的规范化及科学化。,不规范,规范；不严格,严格；无方法,/,技术,成熟的,方法,/,技术。,旨在形成工程化的软件开发的原理、方法及技术。,17,软件工程中的生命周期,五个活动,需求分析和规格,软件设计：逻辑模型,转换,为软件方案，总体结构、模块算法,代码编写,软件测试：模块测试、组装测试、整体测试,运行维护,18,软件工程 vs 形式化方法,软件工程方法试图,指导软件的开发过程。,然而问题依然存在,项目成本、进度依然无法保证,软件开发的后续阶段常常发现许多前期设计错误，更正错误代价高昂,发布运行软件时常崩溃，维护代价依然很高,正如许多软件工程方法所指出的，即使遵循了很多优秀设计准则和优良编码规范，程序仍可能包含很多错误，因此，使用一些方法来消除程序中的人为错误就变得更加重要了。,19,软件开发中为什么使用形式化方法,形式化方法的目的是为开发过程提供一些,技术和工具，用于发现并指出软件实现中潜在的缺陷问题。,对软件需求的描述：,非形式化的描述很可能导致描述的不明确和不一致；形式化方法则要求描述的明确性，而描述的不一致性也就相对易于发现。,对软件设计的描述：,软件设计的描述和软件需求的描述一样重要。,对于编程：,自动代码生成。,对于测试：,测试用例的自动生成。,20,软件开发中为什么使用形式化方法,保证质量的需要,为了得到高质量的软件，企业要采用最好的实践，使他们的软件过程变得成熟起来。形式化方法是一种前沿技术，研究表明，这种技术非常有助于那些希望把软件产品的缺陷出现率减到最小的公司。,节约成本的需要,有证据显示，形式方法的使用减少了项目成本。例如，,IBM,的大型,CICS,事务处理项目的独立审核表明，,9,的成本节约要归功于形式方法的使用。对,T800,型变换计算机的,Inmos,浮点单元的独立审核也证明，形式化方法的使用估计可以减少,12,个月的测试时间。,演示,形式化规约和验证工具,PAT,（,Process Analysis Toolkit,）演示,哲学家吃饭问题,Sliding Game,Shunting Game,22,哲学家吃饭问题,N,个哲学家围着桌子坐，桌子上有,N,个筷子,哲学家想吃饭时总是先拿起右边的筷子再拿起左边的筷子,哲学家只有得到,2,个筷子后才能吃饭,形式化方法,Formal methods are,mathematically,based languages,techniques and tools for,specifying,designing,and,verifying,hardware and software systems,.,形式化方法是渗透在软件生命期中各个环节（需求分析、设计、实现、测试等）的数学方法或者具有严格数学基础的软件开发方法。,形式化方法的基本含义是借助数学的方法来研究计算机科学中的有关问题。,24,形式化方法的主要内容,形式化开发过程的任务分为：模型获取、模型验证、模型变换,模型获取：,从现实世界向模型表示转换，对应软件生命周期中的需求分析、规格、设计活动；,模型验证：,是否满足需求及具有所期望的特性；,模型变换：,从模型表示向计算机系统变换的过程。,这些任务对应三方面的活动：,形式化规约、形式化验证、程序求精,25,形式化方法的发展,20,世纪,60,年代：程序正确性证明研究,20,世纪,80,年代：硬件电路设计的形式化方法应用（时序逻辑和模型检验的诞生）,20,世纪,90,年代：通信协议和智能控制系统中的形式化方法应用（工业界应用高速发展）,本世纪：交互式并发软件系统的形式化方法应用,26,经典案例及应用,牛津大学和Hursley实验室于20世纪80年代合作将Z语言用于IBM商用信息控制系统。IBM对整个开发进行的测试表明，Z语言的应用明显地改善了产品质量、大量减少了错误和早期诊断错误。IBM估计使总体开发成本降低9。这一成果获皇家技术成就奖。,经典案例及应用,Praxis,公司于,1992,年交付给英国民航局的信息显示系统是伦敦机场新空中交通管理系统的一部分。在该系统的需求分析阶段，形式化描述和非形式结构化的需求概念相结合；在系统规格阶段，采用了抽象的,VDM,模型；在设计阶段，抽象,VDM,细化为更为具体的规格。项目开发的生产效率和采用非形式化技术相当，甚至更好。同时，软件质量得到了很大的提高，软件的故障率仅为,0.75,每千行代码，大大低于采用非形式化技术所提供的软件的故障率（约为,220,每千行代码）。,经典案例及应用,加州大学的安全关键系统研究组所开发的空中交通防碰撞系统的形式化需求规格TCASII，采用了基于Statecharts的需求状态机语言RSML，解决了开发过程中遇到的许多问题。TCASII项目表明了复杂过程控制系统列写形式化需求规格的可能性以及应用工程师们不经任何专门培训建立易读且易评判的形式化规格的可行性。,经典案例及应用,除此之外还有：,（,1,）数据库：用于存储病人监护信息的,HP,医用仪器实时数据库系统。,（,2,）核反应堆系统：核反应器安全系统、核发电系统的切换装置。,（,3,）电信系统：,AT&T,的,5ESS,电话交换系统、德国电信的电话业务系统。,（,4,）保密系统：,NATO,控制指挥和控制系统中的保密策略模型、,Multinet,网关系统的数据安全传输、美国国家标准和技术院的令牌访问控制系统。,（,5,）通信协议：协议规格、测试集的生成、协议转换。,（,6,）运输系统：巴黎地铁的自动火车保护系统、英国铁路信号控制、以色列机载航空电子软件。,形式化方法讨论,形式化方法中的抽象数学符号及理论确实对软件工程师的使用带来一些,不便,，以致于人们要花一定的时间和精力去学习和掌握。,但是，,采用形式化方法可以极大地减少了系统设计开发早期阶段的错误，避免了后期错误修改所带来的高额成本开销，这样早期人员培训的成本开销会在后期的系统测试和维护中的高额回报中得到补偿，在某种程度上还,降低了软件开发的成本,。同时，采用形式化方法还会提高系统的,设计开发效率,，并且形式化方法是,高质量、高可靠,软件开发的有效途径，是软件自动化的根本前提。形式化方法,不会完全代替传统的软件开发方法,和面向对象方法，需要根据所解决问题的特点结合或,选择使用,。,31,