软件开发过程中的形式化的规格说明方法简述

在软件开发过程中，用户需求的分析和定义是开发后期的基础。定义是否清晰明确很大程度上决定着整个软件开发的成败。因此，需求分析和规格说明的重要性是不言而喻的。根据其使用的规格说明语言的形式化程度不同，目前的软件规格说明方法大致可分三类：形式化、半形式化及非形式化。

形式化的方法采用有形式化语法和严格数学语义的语言描述规格说明。

半形式化的方法是指它的规格说明语言仅有形式化的语法，而没有严格数学意义下的语义。

非形式化的方法使用自然语言及图表描述规格说明。

形式化的规格说明方法

随着对软件质量和软件生产效率的要求的提高，目前广泛使用的非形式化的需求规格说明方法中存在的问题愈加突出，如需求规格说明潜在二义性，大量文档无法用计算机分析和管理，另外也无法检查规格说明的一致性与完整性。人们渐渐地认识到，彻底解决这些问题的最终措施是用数学的概念和方法来进行软件规格说明。

形式化规格说明方法一般具有如下的优点：

1 . 使用形式化规格说明语言，能在软件开发早期检查规格说明的一致性和完整性；

2 . 可对软件进行形式化的正确性证明，保证可靠性；

3 . 可按某些规则把形式化的规格说明变换成目标软件，提高软件的生产率；

4 . 对于形式化的可执行的规格说明语言，可以把需求规格说明作为系统的原型。

不过，它的最大问题是要求使用者具备较好的数学背景，因此使一般的软件开发人员望而生畏。

根据开发需求规格说明的方式，形式化方法又分为定义性方法和构造性方法。

半形式化的规格说明方法

定义规格说明

半形式化方法，均是从问题域建立 real-world模型，然后定义规格说明的。而形式化方法都假设已给定明确的用户需求。这样开发人员必须先想方法获取用户需求，然后用形式化方法进行严格定义。

不过，采用快速原型技术，这一问题可得到解决。快速原型是一种为了弥补需求分析的不彻底性，保证软件的需求规格说明符用户的要求的有效手段。采用可执行的规格说明，把规格说明作为系统原型运行，既可符合达到快速原型的目的，又不增加很多额外的工作量。

软件开发过程中，形式化方法的前景十分远大，一旦实现广泛应用，将彻底颠覆整个软件行业，大幅度提高软件研发效率及其可靠性。

望安科技是以”形式化验证”为核心技术的安全服务及产品提供商。通过形式化验证核心技术，针对基础软、硬件的形式化验证面向应用系统的形式化验证等，提供整体方案咨询和设计服务。结合客户具体的安全目标，设计特定的形式化验证解决方案，并整合公司的形式化验证工具，设计具体实施办法、评价指标体系。