软件形式化方法概述

根据说明目标软件系统的方式，形式化方法可以分为两类：

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图，状态图等。

友情提示：本文理论性和专业性较强，如果木有接触过该领域，读起来可能会有一点点吃力，成，有点凌乱，见谅！

！本文是Sunny结合多份资料综合整理而

软件形式化方法(Formal Method)在软件开发中一直都受到多方面的争议。持肯定态度的拥护者认为形式化方法会引起软件开发的革命，另一些持否定态度者则怀疑甚至反对将数学引入软件开发过程中。

形式化开发方法的一些争议或缺陷主要体现在：

(1) 形式化方法中所包含的数学理论，限制了大多数程序设计人员的学习和使用；

(2) 认为采用形式化方法会延误项目开发周期、增加开发费用； (3) 许多流行的形式化方法对于较小规模的项目是有效的，但却很难应用于一些大型系统；

(4) 形式化方法不能确保开发出完全正确的软件；

(5) 缺乏对软件生命周期内各个阶段提供全面支持的形式化方法； 等。

从广义上讲，形式化方法是借助数学的方法来解决软件工程领域的问题，主要包括建立精确的数学模型以及对模型的分析活动。狭义的讲，形式化方法是运用形式化语言，进行形式化的规格描述、模型推理和验证的方法。就形式化建模而言，形式化表示必须包含一组定义其语法语义的形式化规则。这些规则可用于分析给定的表达式是否符合语法规定，或证明该表达式具有某种性质。

关于形式化方法：悲观者的角度

形式化方法是为数学家准备的

形式化方法仅供从事形式化研究的人使用 从事形式化研究的人仅使用形式化方法 形式化方法的运用将延缓软件开发进度 形式化方法的运用将提高软件开发成本 形式化方法仅应用于开发安全要求极高的系统

形式化方法仅被用于无关紧要的系统，且缺少工具支持

关于形式化方法：乐观者的角度

运用形式化方法将开发出完美的软件 形式化方法可以替换传统的软件工程方法

形式化方法的出发点是数学逻辑方法，其目的是开发可靠的软件产品。从软件开发来讲，形式化方法目前并非软件开发的主流。从软件发展看，早期的软件是用于数值计算，程序语言侧重于函数和算法的描述，后来数据库的应用和数据结构逐渐变得重要。现在的软件更为复杂，因此，对象、组件、接口、通讯、开放等成为非常重要的概念。从软件工程方法来讲，有一套描述这些概念的办法，比如说用图形、表格、逻辑、自然语言等，交叉使用以描述一个系统的各个方面。因此换一个角度来考虑，我们也可以以目前常用的软件开发方法为出发点，研究怎样将这些方法形式化，使软件系统的描述精确化，以减少可能的误解所带来的问题；或以目前常用的软件开发过程为出发点，研究怎样在软件开发过程中增加一些形式化方法的应用，以提高软件的可靠性。