形式化方法

是指建立在严格数学基础上的系统开发 方法。它是保证设计正确性的一条重要的途径。其中，逻辑、 代数、自动机、图论等构成 了形 式化方法的数学基础。形 式化方法的目的是希望所设计的系统具有较高的可信度和 正确性，并能使系统具有 良好的结构、易维护、能较好地满 足用户要求。实践证明，通过形式规约确实可以增强对系统 发现其它方法难以发现的错误。越来越多的实践证明，形式 化方法在系统设计和验证，特别是高可靠性系统的设计和 验证中有着不可取代的地位。经过 30多年的研究和应用， 如今，形式化方法这一领域取得了大量重要的成果，其应用 也是逐渐融入软件开发过程的各个阶段：从需求系统分析、 功能描述 、（体系结构/算法)设计、编程、测试直至维护。

形式化方法主要包括形式化规约和形式化验证技术。 形式规约是对系统需要达到的功能和性质的数学描述。它 是系统设计的出发点，也是验证系统是否正确的依据，通过 形式化描述可 以尽早发现需求和设计中的错误 。

形式规约的方法主要可分为两类 ：一类是对系统建模， 该方法的 目标是用合适的数学工具建立系统模型，借此精 确地刻画系统的行为特征；另一类是性质描述 ，该方法的 目 标是用合适 的数学工具来描述系统的性质 ，借此对系统进 行深入的研究。

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

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