基于SOFL软件开发过程

摘要：介绍了SOFL在软件开发过程中的运用以及它作为一种优秀的形式化工程方法的优点，SOFL的软件开发过程经历所需分析，抽象设计，演化，细节设计，编程，验证几个阶段，坚实的教学基础以及逐步求精的分解过程保证了系统软件的可靠性和稳定性。
关键词：形式化方法SOFL
软件设计是这样一个过程：用户需求 软件开发 软件系统。需要考虑2个问题：(1)如何使软件系统完全符合用户需求。(2)传统的测试方法是否可以保证软件的质量及可靠性。有鉴于此，需要一种规范化的形式来定义用户需求和设计软件体系结构。形式化方法是指具有坚实数学基础的方法，它是数学上的综合、分析技术的应用，用于开发计算机控制的系统，经常有推理工具的支持，它可提供一个用于模型设计和分析的一个严格而有效的途径应用形式方法构建系统可使其在需求分析阶段消除语义的二义性从而具有较高的可信度、正确性、良好的结构、易维护等优点。
1、方法
SOFL既是一种方法也是一种语言：作为一种方法，SOFL强调系统设计的非形式化、半形式化和形式化规范说明3个阶段，它首先采用结构化方法设计系统，然后再从结构化抽象设计向面向对象的细节设计转化并进行程序实现，此外，它也可以提供有效的、系统的准确的审查和测试技术用来验证规范和程序的正确性；作为一种语言，它融合数据流图（DFD）、Petri网络和VDM-SL相关知识。

2、使用SOFL进行软件开发的过程

那么使用SOFL如何进行软件开发呢？可以分为需求分析抽象设计 演化 详细设计编码 验证这几个阶段。需求分析是发现、理解、文档化用户需求的过程。这通常是在可行性分析之后构建系统的起点。这个过程中开发者与用户需要频繁交流，由于客户的教育背景不同，所以为了增进二者之间的沟通与理解，这个过程形成的规范说明使用非形式化语言和半形式化语言配以可理解的符号集来描述。

2.1 非形式化规范说明

在SOFL中提出了在非形式化的规范说明中应该体现的3个方面内容：(1)需要实现的功能；(2)使用到的资源；(3)功能和资源上的必要约束。在这个阶段，不必过多的关注功能、资源、约束之间的联系，这将会在半形式化规范描述中来进行体现。

2.2 半形式化规范说明

它的目标是阐述以及定义所有在上一步中体现的功能、资源和约束条件以及将这3部分有机联系起来的关系。由于半形式化规范说明仍然是开发者与用户沟通的相似度检测手段，所以它不可以是完全形式化的，那么半形式化规范说明最独特的特征是规范的格式遵循规范语言的语法，但是模块中所有过程的前、后置条件仍采用有组织的自然语言来描述或定义。
半形式化规范说明的任务和特征包括以下5个方面：(1)模块中的关联数据资源，约束条件以及函数；(2)一系列相关的模块集合。每个模块既阐述了在informal规范中给定的函数，又给出了基于现存模块的分解。(3)规范中所使用到的数据应该是在模块中被精确定义的适合数据类型，但是它们的限制条件通常是使用不变体来定义，这可以采用非形式化的定义方法；(4)每个模块给出相应的CDFD；(5)在一个CDFD中所涉及的过程和函数都应该在相应的模块中被定义。如此的定义包括输入数据流、输出数据流、代表相关存储的外部变量的声明。至于前置条件和后置条件的说明内容通常采用非形式化的说明方式。

2.3 抽象设计

抽象设计是将半形式化的需求规范说明转化为能够描述整个系统体系结构同时对其组分进行功能性定义的形式化规范说明。需求规范说明与设计规范说明之间存在这本质性的不同：前者关注的是用户的需求的描述，而后者关注的是系统的体系，以便于提供解决问题的方案。因此，这样的转化不仅仅是形式化的，同时也是满足用户需求的系统结构的产生过程。

2.4 演化

在从非形式化半形式化形式化规范说明的过程中，要设计到演化过程，它主要包括3个内容

摘自：写毕业论文经典的网站www.udooo.com

：精化——细化系统功能；扩展——增加系统功能；修改——改善系统功能。这些操作的目的都是对于规范说明的逐步求精。这3方面的有机结合在很大程度上会保证规范说明的一致性和正确性。

2.5 细节设计

这个过程要完成两个目标：(1)将implicit规范说明转化为explicit规范说明。由于一个高层的过程是由它的分解来定义的，所以也就不需要进行转化。只有最底层的过程才需要进行这个过程的转化，但数据的精化并没有过多的要求。(2)将结构化抽象设计规范转化成基于面向对象的规范。这个过程的主要任务就是建立适合的类以及建立类与类之间的联系。这个类可以是实体，可以使功能函数。

2.6 编程

编程是使用规范语言描述的细节设计的实现。与implicit规范说明同explicit规范说明的转化相比，这个过程需要处理的是对在设计规范中定义的抽象数据类型进行精化，以便转化为使用编程语言描述的具体的数据类型。通常，需要进行4个层次的转化：抽象数据类型的转化；过程，方法和功能的详细规范说明的转化；模块的转化；类的转化。

2.7 验证（Validation and Verification）

Validation的目的是为了确保规范说明能够准确、完整地满足用户的需求；而Verification的目的是保证规范说明内部是连续的、可满足的并且可实现的。
3、结语
本文介绍了如何使用SOFL这样的形式化工程方法来进行软件系统的开发，它的语言规范基于严谨的数据逻辑基础，这就保证了描述的准确性、无二义性。抽象设计，演化和细节设计保证了逐步求精的过程，从根本上降低了系统风险，提高了系统可靠性和稳定性。这对于要求高严密性，高可靠性的领域，例如航天、银行等都有着非凡的意义。
参考文献
傅权岷.基于SOFL的设计时怎么写作组合方法的研究[D].上海交通大学,2011.
李孔仁.面向商业银行业务流程的需求分析方法研究与应用[D].厦门大学,2008.
[3]Liu Shaoying. Formal Engineering for Industrial Software Development using the SOFL Method.Springer-Verlag, 2004.