软件形式化方法概述.docx

根据说明目标软件系统的方式，形式化方法可以分为两类：1）面向模型的形式化方法。面向模型的方法通过构造一个数学模型来说明系统的行为。2）面向属性的形式化方法。面向属性的方法通过描述目标软件系统的各种属性来间接定义系统行为。根据表达能力，形式化方法可以分为五类：1）基于模型的方法：通过明确定义状态和操作来建立一个系统模型（使系统从一个状态转换到另一个状态）。用这种方法虽可以表示非功能性需求（诸如时间需求），但不能很好地表示并发性。如：Z语言，VDM,B方法等。2）基于逻辑的方法：用逻辑描述系统预期的性能，包括底层规约、时序和可能性行为。采用与所选逻辑相关的公理系统证明系统具有预期的性能。用具体的编程构造扩充逻辑从而得到一种广谱形式化方法，通过保持正确性的细化步骤集来开发系统。如：ITL（区间时序逻辑），区段演算（DC）,hoare逻辑，WP演算，模态逻辑，时序逻辑，TAM（时序代理模型），RTTL（实时时序逻辑）等。3）代数方法：通过将未定义状态下不同的操作行为相联系，给出操作的显式定义。与基于模型的方法相同的是，没有给出并发的显式表示。如：OBJ,Larch族代数规约语言等；4）过程代数方法：通过限制所有容许的可观察的过程间通信来表示系统行为。此类方法允许并发过程的显式表示。如：通信顺序过程（CSP）,通信系统演算（CCS）,通信过程代数（ACP）,时序排序规约语言（LOTOS）,计时CSP（TCSP）,通信系统计时可能性演算（TPCCS）等。5）基于网络的方法：由于图形化表示法易于理解，而且非专业人员能够使用，因此是一种通用的系统确定表示法。该方法采用具有形式语义的图形语言，为系统开发和再工程带来特殊的好处。如Petri图,计时Petri图,状态图等。I安全模型I底层规范证明/测试编程实现S4-3形式化验证流程图norsFig4-3TbecircitofformalizationverifiesUuu友情提示：本文理论性和专业性较强，如果木有接触过该领域，读起来可能会有一点点吃力，口！本文是SUnny结合多份资料综合整理而成，有点凌乱，见谅！软件形式化方法(FOrmalMethod)在软件开发中一直都受到多方面的争议。持肯定态度的拥护者认为形式化方法会引起软件开发的革命彤，另一些持否定态度者则怀疑甚至反对将数学引入软件开发过程中二。形式化开发方法的一些争议或缺陷主要体现在：(1)形式化方法中所包含的数学理论，限制了大多数程序设计人员的学习和使用；(2)认为采用形式化方法会延误项目开发周期、增加开发费用；(3)许多流行的形式化方法对于较小规模的项目是有效的，但却很难应用于一些大型系统；(4)形式化方法不能确保开发出完全正确的软件；(5)缺乏对软件生命周期内各个阶段提供全面支持的形式化方法；等。从广义上讲，形式化方法是借助数学的方法来解决软件工程领域的问题,主要包括建立精确的数学模型以及对模型的分析活动。狭义的讲，形式化方法是运用形式化语言，进行形式化的规格描述、模型推理和验证的方法。就形式化建模而言，形式化表示必须包含一组定义其语法语义的形式化规则。这些规则可用于分析给定的表达式是否符合语法规定,或证明该表达式具有某种性质。ApplicationDomainS-SpecificationMachineDo应用领域规格说明机器领土C- machine-P - programD-domainproperties领域性质R-requirements需主既关于形式化方法：悲观者的角度为形式化方法是为数学家准备的形式化方法仅供从事形式化研究的人使用从事形式化研究的人仅使用形式化方法形式化方法的运用将延缓软件开发进度形式化方法的运用将提高软件开发成本形式化方法仅应用于开发安全要求极高的系统形式化方法仅被用于无关紧要的系统，且缺少工具支持切关于形式化方法：乐观者的角度§运用形式化方法将开发出完美的软件形式化方法可以替换传统的软件工程方法形式化方法的出发点是数学逻辑方法，其目的是开发可靠的软件产品。从软件开发来讲，形式化方法目前并非软件开发的主流。从软件发展看,早期的软件是用于数值计算,程序语言侧重于函数和算法的描述,后来数据库的应用和数据结构逐渐变得重要。现在的软件更为复杂，因此，对象、组件、接口、通讯、开放等成为非常重要的概念。从软件工程方法来讲，有一套描述这些概念的办法，比如说用图形、表格、逻辑、自然语言等，交叉使用以描述一个系统的各个方面。因此换一个角度来考虑，我们也可以以目前常用的软件开发方法为出发点，研究怎样将这些方法形式化，使软件系统的描述精确化，以减少可能的误解所带来的问题；或以目前常用的软件开发过程为出发点，研究怎样在软件开发过程中增加一些形式化方法的应用，以提高软件的可靠性。形式化方法可以分为形式化描述和建立在形式化描述基础之上的形式化开发。形式化的描述就是用形式化的语言(具有严格的语法语义定义的语言)做描述。形式化的软件开发，就是用形式化的语言来描述软件需求和特征，并且通过推理验证来保证最终的软件产品是否满足这些需求和具备这些特征。这样的验证当然得建立在严格的语法语义的基础之上的。在实际应用中，这是不容易做到的。形式化方法研究的目的就是希望能够提供更好的理论、方法和工具，扩大形式化方法的应用范围和使用价值。形式化方法的意义在于它能帮助发现其它方法不容易发现的系统描述的不一致、不明确或不完整，有助于增加软件开发人员对系统的理解，因此形式化方法是提高软件系统，特别是Safety-Critical系统的安全性与可靠性的重要手段。最早的形式化方法是逻辑与逻辑推理，它的目标是使推理机械化。从广义上讲，这一目标受到许多挫折，比如说逻辑系统的不完备性(incompleteness)、逻辑系统的不可判定性(undecidability).自动推理的难处理性(intractability)。但是在一些实际应用上，逻辑方法和自动推理还是起着非常大的作用。形式化方法在软件开发中能够起到的作用是多方面的。首先是对软件需求的描述，软件需求的描述是软件开发的基础。比如说一般非形式化的描述很可能导致描述的不明确和不一致，如果描述的不明确和不一致将导致设计、编程的错误,将来的修改所要付出的代价就非常大了，如果导致的错误没有被发现，则影响程序的可靠和使用。形式化方法则要求描述的明确性，而描述的不一致性也就相对易于发现。其次是对软件设计的描述。软件设计的描述和软件需求的描述一样重要，形式化方法的优点对于软件需求的描述同样适用于软件设计的描述，另外由于有了软件需求的形式化描述，我们可以检验软件的设计是否满足软件的要求。对于编程来讲,我们可以考虑自动代码生成。对于一些简单的系统，形式化的描述有可能直接转换成可执行程序，这就简化了软件开发过程,节约了资源和减少了出错的可能性。另外，形式化方法可以用于程序的验证，以保证程序的正确性。对于测试来讲，形式化方法可用于测试用例的自动生成，这可以节约许多时间和在一定程度上保证测试用例的覆盖率。客现世界证正确性ColTCC=CSS协调性Con 凌n(2Ke形式化方法原则上就是用数学与逻辑的方法描述和验证软件。从描述上讲，一方面是系统或程序的描述，另一方面是性质的描述。这些可以用一种或多种语言来描述。这些语言包括命题逻辑，一阶逻辑，高阶逻辑，代数，状态机，并发状态机，自动机，计算树逻辑，线性时序逻辑，进程代数，-演算，-演算，特殊的程序语言，以及程序语言的子集等。从验证来讲，主要有两类方法，一类是以逻辑推理为基础，另一类则以穷尽搜索为基础。逻辑推理有naturaldeduction,sequentcalculus,resolution以及Hoare-IogiC等方法，穷尽搜索方法统称为模型检测。这类方法与系统或程序以及系统性质的表示有很大的关系,比如说符号模型检测，其基本原理是用命题逻辑公式表示状态转换关系，用不动点算法计算状态的可达性以及这些状态是否满足某些性质。形式化方法的应用在电路设计和协议设计上都取得了很大的成绩，但是对于软件来讲还有很多没有解决的问题。软件的描述要比电路和协议复杂，一个软件描述所包含的状态空间通常来讲可以是无限的，因此验证的难度很大。逻辑推理的不足之处在于推理的难度，对于稍微复杂的系统，自动化的推理就难以胜任。人为的推理有很大的缺点，除了费时费力外，比如说一个定理推不出来，并不能说明这个定理不成立，很可能是推理方法和策略应用不当。模型检测的好处在于它有全自动化的检测过程,并且如果一个性质不满足，它能给出这个性质不满足的理由，我们即可据此对我们的系统描述进行改进。模型检测的困难首先是它所能检测的是有限状态模型。这样对于一般软件来讲，需要有一个从任意状态到有限状态的建模过程，并且这样的一个模型的状态空间会面临组合爆炸的问题。形式验证一般被称为形式化验证方法,是相对于传统的验证（模拟、仿真和测试）而言的。形式化验证方法的主要思路就是使用数学的公式、定理和系统来验证一个系统的正确性等。目前的形式化验证方法可以用于验证硬件系统、软件系统和其他系统，而且形式化验证的技术目前也已经发展到不但可以验证系统的功能正确性（有没有错误），而且可以验证系统的性能指标（功耗、散热、延迟等等）。形式化验证方法主要可以分为三种：定理证明、模型检测和等价性验证。定理证明的基本原理是选定一个数学逻辑体系，并用其中的公式来描述（如软、硬件）系统和系统性质刻画，然后在一定的数学逻辑（如hoi逻辑）体系中依据此体系的公理、定理、推导规则和系统描述公式，看看能不能推导出系统的性质刻画公式，如果可以的话验证成功。模型检测的原理比较简单但是非常实用，它将（如软、硬件）系统建模成有限状态系统（一般成为keripke结构）,系统的性质刻画用时序逻辑公式表示（CTL,LTL等），而后在此模型上来验证性质刻画的正确性，模型检测于定理证明相比是有很大优势的，他可以全自动地验证，不需要人工干预，而定理证明则在一些关键推导路径中需要数学家控制。还有一种是等价性验证,等价性验证其实是一种半形式话的技术，同前两种验证正确性的技术不同，它验证的是设计的一致性，即不同设计阶段的设计是否功能相同，这种技术中一般采用符号的方法和增量的方法，而且由于这种方法和硬件电路紧密结合，所以电路验证的一些传统方法也大量应用于此中方法中来，比如ATPG技术等。如大家使用的Synopsys的Formality本质上就是一个等价性验证器。形式化验证是非常有用的，只是国内作这一行的人太少。大家可以看看Synopsys和Cadence两家公司z它们都是从形式化验证起家的，然后转到目前流行的将设计和验证统一在一起,即设计验证领域。SynOPSySAcceleratingInnovationcadence软件形式化方法研究内容：形式化语言（形式化描述、形式规约）：怎样描述软件系统及其行为模式；更好地刻画软件系统的性质，比如说，通讯、分布、开放、移动；各种语言的应用、比较，语言与语言之间的转换；开发相应的软件工具。形式化验证（形式验证）：怎样验证软件系统符合给定的行为模式；更有效地验证软件系统的性质，比如说，自动化、速度快、内存需求少；各种方法的应用、比较；开发相应的软件工具。具体来说，软件形式化方法包括以下几个主要研究方向：（1）基础概念：复合、抽象、重用模型、数学理论组合、数据结构及算法。需要对如何复合方法、复合规格、复合模型、复合理论、复合证明等进一步的理解；需要开发出将整体特性分解为易于验证的局部特性的有效方法；实际系统在规格和验证之前都要进行某种程度上的抽象，需要研究出评判抽象层次合理与否的方法；重用不仅可以提高开发效率,而且可以提高软件的可靠性，应当研究可重用模型和理论；许多安全关键反应式系统是数字和模拟混合的，需要连续和离散两个范畴内数学基础支撑的混杂系统理论和技术支撑；大规模、复杂软件中搜索空间是巨大的，需要研究出新的数据结构和算法。(2)形式化方法与面向对象方法的结合：这已经成为软件工程领域的一个研究热点，例如：Statecharts.Petri网、Z语言、VDM等，以及与面向对象方法结合产生的Objectcharts、面向对象Petri网、ObjectsZ+、VDM+等。这方面的研究体现在两个方面：利用面向对象结构来提高形式符号的表达能力；使用形式化方法来分析面向对象的语义或提高这些标记符号的表达对象概念的能力。形式化方法和其他传统软件开发方法相结合以达到取长补短的目的，也是值得研究的课题。(3)工具开发：具有良好用户界面、易于学习和操作简单的形式化方法支撑工具，对于形式化方法的推广应用是大有裨益的。追求通用的完善的形式化方法及其支撑工具是不现实的，侧重于如下某一个或几个方面准则的特色方法和工具是未来研究的重点。这些准则包括：一旦开始使用之后尽早得到明显的效益；效益随着开发者的了解深入和熟练而增加；单一规格可以在软件开发生命周期的多个阶段取得效益；能和其他通用编程语言或方法交互使用；工具应当像编译器那样易于使用、输出，也易于阅读；概念和工具应当易于入门和学习掌握；软件特性分析有所侧重；支持渐进软件开发，允许部分规格和验证。此外，特定问题域的形式化方法及其工具研究也是非常重要的。高等学校研究生系列教材1软的形式化方法FormalMethodsOfSoftwareDevelopment【作者：刘伟