软件形式化方法PPT学习课件.ppt

通过软件形式化方法、陈铁明/王婷tmchen/wangting、1、课程介绍和本课程的学习，使同学了解软件开发中形式化方法的基本概念和原理，并提供了一些常用的软件系统形式化描述方法(有限状态机、CSP、z语言、时分析问题，锻炼解决问题的能力，逻辑思维。 2，课程参考教材，软件开发的形式化方法，古天龙篇，2005，高等教育出版社课程PPT，3，课程评价，总成绩=课程作业(50% )期末考试(50% )，4，形式化思想，广义上，抛弃事物内容，只采取形式结构，只考虑形式上的内容。 以数学为例，可以表现为完全形式化，所有数学都可以通过符号来形式化表现。 概念形式化：原理形式化：在十字定理三角形ABC中，873c=90。 三边a、b、c满足a2 b2=c2两个基本特征：自然语言符号化，抽象摘要将形式语言的直观语义推理关系描述为语义描述和语法描述。 5、5、例如：电梯控制系统(自然语言描述)、6、例如： UML描述(半形式化)、7、具有良好语法和语义定义的形式描述方法不能或不太能支持基于数学的形式分析和推理过程，例如：电梯控制系统(程序语言描述)、8、 例如，电梯控制系统(有限状态机描述)，9具有良好语法和语义定义的形式描述方法，能够有效地支持基于机器人理论的形式化验证过程，软件规约表示可以包括自然语言、图、表等形式化方式描述。 由于非形式化方法本身存在的矛盾、二义性、模糊性、描述规约时的不完整性、抽象层次混合等情况，得到的规约无法正确描述系统模型，甚至可以在后续的软件开发中弥补错误的危险。 对于形式化的方法，由于在严格的数学基础上具有严格的语法和语义定义，因此能够准确描述系统模型，消除矛盾、二义性、模糊性等，最终得到相对完整正确的系统模型。 10、软件危机，1968年，北约会议发表了“软件危机”一词。 软件危机如何保持持续膨胀的软件产品，以满足软件开发、发展和复杂化的需求，包括两个问题。 软件危机主要体现了以下几个方面难以管理开发成本高的项目进展，难以保证维护的质量，-11-、难以管理项目进展，难以制定软件开发进展。 如果有10个人月的工作量的话，一个人完成需要10个月，从10个人完成需要1个月。 虽然这种工作量的估算方式只适用于各部分的工作相互干扰的情况，但作为整体还需要研究合作，这种讨论交流活动增加了工作量。 软件系统结构复杂，各部分关联非常大。 布鲁克提出了“如果着力于落后的软件项目，就难以按期完成”的法则。 1995年，美国取消了总计810亿美元的软件项目，其中31%未取消，53%的项目延长了一半时间，9%按期完成，未超过期限。 1998年，美国企业应用项目28%的项目被取消，40%的项目无限长，超过了预算。 2008年的数据显示，按计划交付并完成功能的成功项目仅占32%。 -12-、软件维护困难，软件维护任务特别重要。 正式使用的商用软件总是有一定数量的错误。 随着时间的推移，各种运行条件下软件发生故障，需要修改维护。 软件维修不是更换某个备件，而是必须修正逻辑上的缺陷。当软件系统变得庞大、问题变得复杂时，“纠正一个错误会带来更新的错误！ 经常发生，-13-，典型的软件项目开发，14，质量保证不了，Therac-25是加拿大原子能公司AECL和法国公司CGR共同开发的医疗设备，高能束和电子流可以杀死人体毒瘤，伤害了毒瘤附近的人体健康组织1985年6月至1987年1月，由于软件的缺陷，电子流和x射线束的过度使用引起了6起医疗事故，造成了4人死亡，2人受重伤的严重结果。 1996年，欧洲宇宙局阿里安5型火箭发射40秒后爆炸，有2名法国士兵死亡，损失资产达到10亿美元巨大，历时9年的宇宙计划遭到严重挫折。 爆炸的原因是惯性导航系统的软件技术要求和设计错误。 2011年7月23日20时30分05秒，北京南站开往福州站的D301列车和杭州站开往福州南站的D3115列车发生列车追尾事故，造成40人死亡，172人受伤，32小时35分中断运行，直接经济损失19371.65万元。 初步掌握的情况分析显示，“723”高速车事故在温州南站信号设备设计上存在重大缺陷，雷击故障后，红灯和应该显示的区间信号灯错误地显示为绿灯。 -15-、软件质量的关键方面，16、如何解决软件危机17、软件工程方法软件工程：控制和管理工程软件开发过程、软件设计、生产、生产不规范不规范严格的方法/没有技术成熟的方法/技术。 旨在形成工程化软件开发的原理、方法和技术。 软件施工生命周期，5个活动需求分析和规范软件设计：逻辑模型转换为软件方案，整体结构，模块算法代码编写软件测试：模块测试，装配测试，整体测试执行维护，-18-，软件但问题依然是项目成本、进展依然在软件开发的后续阶段发现不少前期设计错误，纠正错误成本高分发执行软件往往会崩溃， 维护成本依然如许多软件工程方法所指出的那样，即使遵循了许多优秀的设计标准和优秀的编码规范，程序中也可能包含许多错误，因此能够使用一些方法来消除程序中的人为错误19、为软件开发使用形式化方法的原因，形式化方法的目的是为开发过程提供技术和工具，发现和指出软件实现中潜在的缺陷问题。 软件要求描述：非形式描述极有可能导致描述模糊性和不匹配的形式化方法要求描述的明确性，并且相对容易发现描述不匹配。 软件设计说明：软件设计说明与软件要求说明一样重要。 对于编程：自动代码生成。 对于测试：自动生成测试用例。 20、为什么在软件开发中使用形式化的方法，要保证质量是为了得到高质量的软件，企业必须采用最好的实践，使他们的软件过程成熟。 形式化方法是最先进的技术，研究表明，该技术对希望将软件产品缺陷出现率降至最低的公司非常有用。 节省成本的必要性有证据表明使用形式化的方法降低了项目成本。 例如，IBM的大型CICS事务项目的独立审计表明，9%的成本节约是通过形式化方法实现的。 对于T800型变换计算机的Inmos浮点单元的独立监测，形式化方法的使用也证明可以减少12个月的测试时间。21、演示、形式化规约和验证工具PAT(ProcessAnalysisToolkit )演示哲学家就餐问题SlidingGameShuntingGame，22 .SG/pat/WP-source/resources/pat3_ 5 pat3.setup.3.5.1.MSI，哲学家的饮食问题，n个哲学家围着桌子坐着，桌子上n个筷子哲学家想吃饭的时候总是拿下右边的筷子，左边的筷子哲学家拿两个筷子之后再吃饭，23， 形式化方法包括formalmethodsarematicallibbasedlanguges、techniquesandtoolsforspecifying、designingandverifighardwareandsoftwarewaresystem 是在软件生命的各个阶段(需求分析、设计、实现、测试等)渗透的数学方法或者具有严格数学基础的软件开发方法。 形式化方法的基本含义是用数学方法研究计算机科学中的问题。 24、形式化方法的主要内容，形式化开发过程的任务是：模型检索、模型验证、模型转换模型检索：从现实世界向模型表示的转换、软件生命周期中的需求分析、标准、与设计活动相对应的模型验证：是否具有满足需求、预期的特性模型转换：从模型表示到计算机系统这些任务支持三方面的活动：形式化规约、形式化验证、程序要求、25、形式化方法的发展20世纪60年代：程序正确性证明研究20世纪80年代：硬件电路设计的形式化方法的应用(时序逻辑和模型检验的产生) 20世纪90年代：形式化方法在通信协议和智能控制系统中的应用(工业应用的快速发展)本世纪：交互式并发软件系统的形式化方法的应用，26，经典案例和应用，牛津大学和Hursley研究所于20世纪80年代将z语言应用于IBM商务信息控制系统根据IBM对整个开发进行的测试，z语言的应用明显改善了产品质量，大大减少了错误，减少了早期诊断错误。 IBM预计总体开发成本将降低9%。 这项成就获得了皇家技术奖。 27、经典案例与应用，Praxis公司1992年交给英国民航局的信息显示系统是伦敦机场新空中交通管理系统的一部分。 在此系统的需求分析阶段，在将经格式化的描述与非格式化的需求概念相结合的系统规范阶段，在采用抽象VDM模型的设计阶段，抽象VDM被细分为更具体的规范。 项目开发的生产效率等同于采用非形式化技术，更好。 同时，软件质量大大提高，软件故障率仅为0.75千行代码，远远低于采用非形式化技术提供的软件故障率(约220千行代码)。 28、经典案例与应用，加利福尼亚大学安全关键系统研究小组开发的航空交通防撞系统的形式化需求规范TCASII，采用基于Statecharts的需求状态机语言RSML，解决了开发过程中遇到的诸多问题。 TCASII项目显示了复杂的过程控制系统写形式化要求规格的可能性和应用技术人员不接受专业训练，制作易读易评价的形式化规格的可能性。29、除经典案例和应用外，(1)数据库：存储患者监测信息的HP医疗器械实时数据库系统。 (2)核反应堆系统：核反应器安全系统、核发电系统切换装置。 (3)电信系统： ATT的5ESS电话交换系统，德国电信的电话业务系统。 (4)安全系统：北约控制指令和控制系统安全战略模型，多网关系统数据安全传输，美国国家标准和技术院令牌访问控制系统。 (5)通信协议：协议规格、测试集的生成、协议转换。 (6)运输系统：巴黎地铁自动列车保护系统、英国铁路信号控制、以色列机载航空电子软件。 30、形式化方法的讨论、形式化方法的抽象数学符号和理论确实给软件工程师的使用带来不便，人们必须花