软件工程中的形式化方法研究综述

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

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

中图分类号：TP311.5 文献标识码：A 文章编号：1007-9416（2015）10-0000-00

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

1 形式化方法

1.1 形式化方法

软件工程中的形式化方法就是通过严格的符号系统和数学模型来描述和验证一个目标软件系统的行为和特性，包括需求规格、设计和实现等[2]。形式化方法所使用的是严格的数学语言，其语法和语义都是无二义的、精确的。

1.2 主要研究内容

形式化方法的研究主要集中在形式规约（ Formal Specification）和建立在形式规约基础上的形式验证（ Formal Verification）两个方面[3]。

形式规约是指通过具有精确语义的形式语言对程序功能进行描述。描述结果将作为程序设计和验证的重要依据。

形式验证是对现有的程序系统进行验证，检查其是否符合规约的要求。传统的验证方式是通过实验对系统进行查错，包括模拟（simulation）和测试（testing）[2]。

1.3 形式化方法的分类

根据描述方式，可将形式化方法归为两类[4]：

（1）模型描述的形式化方法。通过构造一个数学模型来直接描述系统或程序。

（2）性质描述的形式化方法。通过对目标软件系统中不同性质的描述来间接描述系统或程序。

根据表达能力，可将形式化方法大概分为五类[Barroca*1992][5]：

（1）模型方法——对系统状态和改变系统状态的动作直接给出抽象定义，并进行显式描述。该方法的缺陷是不能显式地表示并发。

（2）代数方法——通过定义不同操作的关系，隐式地描述操作。与模型方法相同，代数方法也不能显式地表示并发。

（3）进程代数方法——通过一个显式模型来描述并发过程。将并发性归结为非确定性，通过交错语义（interleaving semantics）[6]来表示系统行为。如：CCS，CSP，ACP等。

（4）逻辑方法——通过描述程序状态规范和时间状态规范的逻辑方法来描述系统特性，如：CTL，LTL。

（5）网络模型方法——通过独立描述网络中的每一个节点，显式地给出系统的并发模型。如：Petri网。

2 软件方法学

2.1 软件危机

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

2.2 软件方法学

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

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

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

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

3.1 形式化方法开发过程

按照软件工程“自顶向下、逐步求精”的原则，软件生命周期可分为六个阶段：可行性分析、需求分析、体系结构设计、详细设计、编码、测试发布，形式化方法贯穿软件工程整个生命周期[10]。

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

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

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

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

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

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

3.2 综合评价

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

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

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

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

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

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

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

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

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

参考文献

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

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

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

[4]罗保山.基于形式化方法的软件开发技术[J].电脑知识与技术，2008（23）：1290-1292.

[5]郑红军，张乃孝.软件开发中的形式化方法[J].计算机科学，1997，24（6）：90-96.

[6]I.Czaja， R.J.V.Glabbeek， U.Goltz. Interleaving Semantics and Action Refinement with Atomic Choice[J].in “Advances in Petri Nets，1991，609（12）：89-107.

[7]朱少民，软件工程导论[M].北京：清华大学出版社，2009.

[8]邹晓辉，邹顺鹏.软件工程学科何以独特——形式化方法的双重路径[J].软件，2011，32（7）.

[9]陈火旺，罗朝晖，马庆鸣.程序设计方法学基础[M].长沙：湖南科学技术出版社，1987.

[10]苗德成，冯黎波.形式化方法在软件工程中的应用研究[J].河北：河北科技大学学报，2011，32（6）.

[11]吕毅.形式化方法介绍及其在工程中的应用[J].微电子学与计算机，2003，20（10）：26-3.

收稿日期：2015-09-14

作者简介：李婉璐（1991—），女，汉族，宁夏盐池人，硕士在读，就读于：宁夏大学数学计算机学院计算机软件与理论专业，研究方向：形式化方法。

推荐访问:形式化 软件工程 综述 方法 研究