软件形式化方法概述.docx
《软件形式化方法概述.docx》由会员分享,可在线阅读,更多相关《软件形式化方法概述.docx(12页珍藏版)》请在课桌文档上搜索。
1、根据说明目标软件系统的方式,形式化方法可以分为两类:1)面向模型的形式化方法。面向模型的方法通过构造一个数学模型来说明系统的行为。2)面向属性的形式化方法。面向属性的方法通过描述目标软件系统的各种属性来间接定义系统行为。根据表达能力,形式化方法可以分为五类:1)基于模型的方法:通过明确定义状态和操作来建立一个系统模型(使系统从一个状态转换到另一个状态)。用这种方法虽可以表示非功能性需求(诸如时间需求),但不能很好地表示并发性。如:Z语言,VDM,B方法等。2)基于逻辑的方法:用逻辑描述系统预期的性能,包括底层规约、时序和可能性行为。采用与所选逻辑相关的公理系统证明系统具有预期的性能。用具体的编
2、程构造扩充逻辑从而得到一种广谱形式化方法,通过保持正确性的细化步骤集来开发系统。如:ITL(区间时序逻辑),区段演算(DC),hoare逻辑,WP演算,模态逻辑,时序逻辑,TAM(时序代理模型),RTTL(实时时序逻辑)等。3)代数方法:通过将未定义状态下不同的操作行为相联系,给出操作的显式定义。与基于模型的方法相同的是,没有给出并发的显式表示。如:OBJ,Larch族代数规约语言等;4)过程代数方法:通过限制所有容许的可观察的过程间通信来表示系统行为。此类方法允许并发过程的显式表示。如:通信顺序过程(CSP),通信系统演算(CCS),通信过程代数(ACP),时序排序规约语言(LOTOS),计
3、时CSP(TCSP),通信系统计时可能性演算(TPCCS)等。5)基于网络的方法:由于图形化表示法易于理解,而且非专业人员能够使用,因此是一种通用的系统确定表示法。该方法采用具有形式语义的图形语言,为系统开发和再工程带来特殊的好处。如Petri图,计时Petri图,状态图等。I安全模型I底层规范证明/测试编程实现S4-3形式化验证流程图norsFig4-3TbecircitofformalizationverifiesUuu友情提示:本文理论性和专业性较强,如果木有接触过该领域,读起来可能会有一点点吃力,口!本文是SUnny结合多份资料综合整理而成,有点凌乱,见谅!软件形式化方法(FOrmal
4、Method)在软件开发中一直都受到多方面的争议。持肯定态度的拥护者认为形式化方法会引起软件开发的革命彤,另一些持否定态度者则怀疑甚至反对将数学引入软件开发过程中二。形式化开发方法的一些争议或缺陷主要体现在:(1)形式化方法中所包含的数学理论,限制了大多数程序设计人员的学习和使用;(2)认为采用形式化方法会延误项目开发周期、增加开发费用;(3)许多流行的形式化方法对于较小规模的项目是有效的,但却很难应用于一些大型系统;(4)形式化方法不能确保开发出完全正确的软件;(5)缺乏对软件生命周期内各个阶段提供全面支持的形式化方法;等。从广义上讲,形式化方法是借助数学的方法来解决软件工程领域的问题,主要
5、包括建立精确的数学模型以及对模型的分析活动。狭义的讲,形式化方法是运用形式化语言,进行形式化的规格描述、模型推理和验证的方法。就形式化建模而言,形式化表示必须包含一组定义其语法语义的形式化规则。这些规则可用于分析给定的表达式是否符合语法规定,或证明该表达式具有某种性质。ApplicationDomainS-SpecificationMachineDo应用领域规格说明机器领土C- machine-P - programD-domainproperties领域性质R-requirements需主既关于形式化方法:悲观者的角度为形式化方法是为数学家准备的形式化方法仅供从事形式化研究的人使用从事形式化
6、研究的人仅使用形式化方法形式化方法的运用将延缓软件开发进度形式化方法的运用将提高软件开发成本形式化方法仅应用于开发安全要求极高的系统形式化方法仅被用于无关紧要的系统,且缺少工具支持切关于形式化方法:乐观者的角度运用形式化方法将开发出完美的软件形式化方法可以替换传统的软件工程方法形式化方法的出发点是数学逻辑方法,其目的是开发可靠的软件产品。从软件开发来讲,形式化方法目前并非软件开发的主流。从软件发展看,早期的软件是用于数值计算,程序语言侧重于函数和算法的描述,后来数据库的应用和数据结构逐渐变得重要。现在的软件更为复杂,因此,对象、组件、接口、通讯、开放等成为非常重要的概念。从软件工程方法来讲,有
7、一套描述这些概念的办法,比如说用图形、表格、逻辑、自然语言等,交叉使用以描述一个系统的各个方面。因此换一个角度来考虑,我们也可以以目前常用的软件开发方法为出发点,研究怎样将这些方法形式化,使软件系统的描述精确化,以减少可能的误解所带来的问题;或以目前常用的软件开发过程为出发点,研究怎样在软件开发过程中增加一些形式化方法的应用,以提高软件的可靠性。形式化方法可以分为形式化描述和建立在形式化描述基础之上的形式化开发。形式化的描述就是用形式化的语言(具有严格的语法语义定义的语言)做描述。形式化的软件开发,就是用形式化的语言来描述软件需求和特征,并且通过推理验证来保证最终的软件产品是否满足这些需求和具
8、备这些特征。这样的验证当然得建立在严格的语法语义的基础之上的。在实际应用中,这是不容易做到的。形式化方法研究的目的就是希望能够提供更好的理论、方法和工具,扩大形式化方法的应用范围和使用价值。形式化方法的意义在于它能帮助发现其它方法不容易发现的系统描述的不一致、不明确或不完整,有助于增加软件开发人员对系统的理解,因此形式化方法是提高软件系统,特别是Safety-Critical系统的安全性与可靠性的重要手段。最早的形式化方法是逻辑与逻辑推理,它的目标是使推理机械化。从广义上讲,这一目标受到许多挫折,比如说逻辑系统的不完备性(incompleteness)、逻辑系统的不可判定性(undecidab
9、ility).自动推理的难处理性(intractability)。但是在一些实际应用上,逻辑方法和自动推理还是起着非常大的作用。形式化方法在软件开发中能够起到的作用是多方面的。首先是对软件需求的描述,软件需求的描述是软件开发的基础。比如说一般非形式化的描述很可能导致描述的不明确和不一致,如果描述的不明确和不一致将导致设计、编程的错误,将来的修改所要付出的代价就非常大了,如果导致的错误没有被发现,则影响程序的可靠和使用。形式化方法则要求描述的明确性,而描述的不一致性也就相对易于发现。其次是对软件设计的描述。软件设计的描述和软件需求的描述一样重要,形式化方法的优点对于软件需求的描述同样适用于软件设
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 软件 形式化 方法 概述
链接地址:https://www.desk33.com/p-151213.html