摘 要：软件工程中的形式化方法是以数学理论为基础，建立的一种用来解决软件工程领域问题的系统性分析方法。形式化方法通过具有明确语义的形式语言来描述目标软件系统的行为和特征，为目标系统开发提供了一个模型化的有效设计和分析途径，保障了系统的安全性和可靠性。本文简单介绍了形式化方法的研究内容及分类，在软件方法学的研究背景下，对形式化方法在软件系统开发每一个阶段的应用进行了详细分析和综合评价。

关键词：形式化方法;软件方法学;形式化的软件开发

早期软件系统规模较小，20世纪60年代之前，对软件系统的开发一直通过“手工”方式，具有个人化及技艺化的开发特点。60年代中期，计算机的容量和速度有了显著提升，软件系统规模越来越大，软件开发生产率不再能满足现状，软件危机开始爆发。60年代后期，针对“软件危机”提出两类解决办法：一是将工程化应用于软件的开发过程，即“软件工程”的出现和发展;二是建立严格的理论基础，采用形式化方法来指导软件开发过程。经过近半个世纪的探索和应用，形式化方法这一领域已经取得了大量的研究成果。

1 形式化方法

软件工程中的形式化方法就是通过严格的符号系统和数学模型来描述和验证一个目标软件系统的行为和特性，包括需求规格、设计和实现等。形式化方法所使用的是严格的数学语言，其语法和语义都是无二义的、精确的。形式化方法的研究主要集中在形式规约（Formal Specification）和建立在形式规约基础上的形式验证（Formal Verification）两个方面。

2 软件方法学

2.1 软件危机

60年代后期，软件系统的规模逐步增大，程序实现地复杂度也越来越高，可靠性问题成为越来越多人关注的焦点。由于软件开发生产率不再能满足计算机应用迅速深入的趋势，软件危机开始爆发。1968年北大西洋公约组织的计算机科学家在联邦德国召开国际会议，第一次讨论软件危机问题，并正式提出“软件工程”。

2.2 软件方法学

近年来，国外出现了许多指导软件开发的方法。“软件方法学”（Software Methodology）以软件方法为研究对象，用来指导软件设计的原理和原则，以及基于这些原理和原则的方法和技术。软件方法学是“软件工程”中的一个主要内容。狭义的软件方法学指某种特定的软件设计指导规则和方法体系。软件方法学的主要目的是高效地设计正确的软件。根据性质可分为以下两类：

（1）形式化方法：形式方法通过精确的数学语言对系统的各类属性和开发过程做出严格的描述和验证，定义了如一致性、完全性、正确性、规约等概念。无需通过实际运行来证明软件规约是可实现的、建立的系统是可正确实现的、系统具有某些性质等。

（2）非形式化方法：非形式方法则不考虑系统的严格性，通常采用文本、图表等模型描述系统。

3 基于形式化方法的软件开发

3.1 形式化方法

（1）可行性分析：可行性分析是对待开发系统提供一种综合性的分析方法。综合各方面因素论证待开发系统是否可行，为开发过程提出综合评价和决策依据。由于形式化方法的符号演算系统仍不能完全表达自然语言，所以在此阶段的应用仍是一项巨大挑战。

（2）需求分析：需求分析是在软件开发过程的早期阶段，将用户需求转换为说明文档。一般非形式化的描述可能导致描述的不明确和需求的不一致，可能导致编程错误，影响程序的使用和可靠性。形式化方法则要求明确描述用户需求。

（3）体系结构设计：体系结构设计阶段的根本目的是将用户需求转换为计算机可以实现的目标系统。本阶段侧重描述软件系统的接口、功能和结构。形式化方法对于软件需求描述的优点同样适用于软件设计的描述。由于需求阶段功能描述并不能完全实现，所以形式化方法在此阶段的应用仍存在问题。使用者可采用半形式化方法来完成此阶段的工作。

（4）详细设计：详细设计阶段的形式化是以体系结构规范为基础进行精化描述的过程。通过此阶段的形式化描述能够检验需求描述和用户需求是否一致。为使形式化方法更适用于详细设计和精化过程，可将各种形式的规范联系起来。

（5）编码：自动代码生成器目前能将一些规模较小软件系统的形式化描述直接转换成可执行程序。在简化软件开发过程的同时既节约了资源又增强了软件的可靠性。

（6）测试发布：软件开发的最后阶段是测试发布。在软件投入运行前，需要对软件开发各阶段的文档以及程序源代码进行检查。对于测试来讲，形式化方法可用于测试用例的自动生成，保证测试用例的覆盖率。

3.2 综合评价

形式化方法开发软件系统的优势有：

（1）软件开发的基础是对软件需求的描述。形式化方法要求描述的明确性，很大程度上保证了需求的一致性，减少了可能的误解，为正确实现用户需求提供了更大的可能性。

（2）形式化验证对形式化描述的需求文档提供明确的逻辑论证，通过推理验证来保证最终的软件产品能够满足用户需求。

（3）形式化描述和验证实现了系统的一致性分析和重复分析，提供了一个几乎不依赖特定分析者的分析过程。

（4）形式化描述和验证基于计算机和严格符号系统的支持，实现了开发和验证的自动化，节约了人力资源并且保证了软件的可靠性。

形式化方法开发软件系统的缺陷：

（1）形式化方法的使用建立在数学理论的基础上，限制了大多数人员的学习和使用。

（2）缺乏一种通用的形式化方法来支持软件生命周期每一阶段。

（3）不同的数学规范在不同的模型和工程环境中可能不只有一种解释，为形式验证带来困难。

参考文献：

[1]张广泉.关于软件形式化方法[J].重慶师范学院学报（自然科学版），2002（02）.

[2]张玮玮，陈珊.软件开发中的形式化方法介绍[J].张家口职业技术学院学报，2005，18（01）：54-57.

[3]陈丹.基于形式化方法的软件开发技术[J].软件工程师，2009：52-53.

作者简介：熊小超（1992-），女，江西丰城人，研究生，研究方向：形式化方法。