形式化技术在软件工程的价值范文

1软件工程各阶段的规约描述

软件的开发周期有需求分析、详细设计、测试、可行性分析、体系结构设计和编码六个部分。形式化技术贯穿于软件开发周期的六个部分，形式化时基于参数化的数学理论形式化定义语义。下面从可行性分析、需求分析、体系结构设计和详细设计几个方法进行说明。

1.1可行性分析

软件生命周期的第一个阶段是可行性分析阶段，在这一阶段要通过大量的数据资料来说明系统的开发是否是可行的。指出项目的建议、风险预测、可行性，为项目的决策提供参考依据。在此阶段，通过将实际问题转化为可行性的研究，形成一定的文档材料，规定专业的属于，说明软件系统进行开发的处理流程、数据流程、输入输出、运行环境和开发环境等等。当前来说，专门用于可行性分析这一阶段的形式化技术还非常少，主要的原因是无法将形式化的符号和自然的语言很好的结合起来，确保使用本软件的用户可以非常清楚明白的理解形式化技术所要描述的意义。Z语言是目前一种不可执行的半形式化语言，它短小且容易阅读，采用非形式化的英语对软件的规约进行解释。

1.2需求分析

需求分析分为信息处理和分信息预处理两个阶段，将可行性分析报告作为输入。元语言是形式化语言中的一种，它是基于集合论的证明规则和谓词演算，给出抽象机状态确定模型，从而生成文档。这种形式化语言，对于程序员来说，容易实现原型而且可读性好，容易掌握。语义的设计是形式化技术中需求分析阶段主要要进行的工作之一。在需求分析这一阶段，ER图是从可行性分析的实际问题中导出来的。通过ER图给出SXL语言的事实和对象，SXL语言有助于开发团队理解和交流。SXL语言、RAISE语言和VDM元语言都是应用于需求分析阶段的比较常用的形式化技术。

1.3体系结构设计

软件设计的第三个阶段是体系结构的设计，在这一阶段是将需求分析转换为要实现的目标软件，并进行各种方案的分析和比较，最终选择较好的方案。在体系结构设计阶段采用过程代数形式化的攻击进行输入、输出的行为描述。TLG语言适合体系结构设计阶段不强调如何做仅仅说明做什么。采用形式化的说明把自然的语言融入到逻辑程序设计范型和数学函数中，这样更容易证明用户需求的一致性。GLIDE是一种半形式化的SSFL，GLIDE的好处是应用范围广，而且抽象的级别比较高，不过也有一定的局限性就是使用的时候需要适当的进行扩充和修改。

1.4详细设计

软件设计的第四个阶段就是详细设计，在详细设计阶段，要与软件系统的形式化描述一致。在详细设计阶段，要为软件系统的各个模块设计相应的内部数据结构和算法，确定最终系统实现的一个精确的描述。Larch语言是用于说明程序功能，可以适当的增强详细设计阶段的处理能力和描述能力。形式化的Trace语言作为软件详细设计阶段的形式化工具，采用将模块实现的抽象数据作为自动机说明每个模块的接口需求。Trace语言与SSFL语言不同的特点是程序自动的生成和验证在同一形式的系统内进行。

2形式化技术的评价

形式化技术在软件工程中有效的提高了开发的效率、改进了软件开发的质量、减少了开发费用。形式化的技术容易在软件的规约上取得一致性，它属于一种非常有效的交流方式。在软件工程中，形式化技术的优势在于语法定义准确、问题抽象、表达无二义性、语义清晰可操纵、描述简洁规范。形式化技术在非功能性的要求上比如安全性、保密性、结构性上利用数学工具更容易进行核查。虽然形式化技术在软件工程的各个阶段已经取得了不错的成就，但是还是存在着一定的局限性，比如缺乏在实际项目中应用的有效工具。程序功能的正确性有时候难以证明，因为形式化技术缺乏定理证明机制的支持。形式化技术的下一个发展方向应该是尽量的把形式化的语言表达的形式进行简单化，让其趋于自然语言，增强它的可理解能力。

3总结

在软件工程中，形式化技术极有好处也有弊端，有很多人支持这种技术，也有人对它持反对态度。在软件工程发展的过程中，形式化的技术也起到了相当大的作用。在四十多年对形式化技术的研究中，很多成功的案例也证明了形式化技术的巨大作用，但是我们也需要清醒的认识到它在实践和工业的应用中所存在的缺陷和困难。

作者：闻寅啸单位：苏州大学计算机科学与技术学院