陈　丹

摘要:形式化方法作为一种以数学为基础的方法,能够清晰、精确、抽象、简明地规范和验证软件系统及其性质,能够极大地提高软件的安全性和可靠性。本文从形式化方法的研究内容、分类以及发展等方面出发,对基于形式化方法的软件开发的基本思想作了介绍,分析了使用形式化开发软件系统的优势和可靠性。

关键词:管理信息系统;本体;原型;实践教学

1 引言

随着软件系统复杂度的不断增长,开发正确、可靠的软件,成为一个急待解决的问题。解决此问题的一个有前途、有希望的技术是形式化方法的应用。形式化方法需要形式化规约说明语言的支持。形式化方法建立在严格的数学基础上,能够清晰、精确、抽象、简明地规范和验证软件系统及其性质,其目标是希望能使系统具有较高的可信度和正确性,并能使系统具有良好的结构,使其易维护,关键是能较好地满足用户需求。

2 形式化方法的研究内容

形式化方法可以分为形式化描述和建立在形式化描述基础之上的形式化开发。形式化的描述就是用形式化的语言(具有严格的语法语义定义的语言)做描述。形式化的软件开发,就是用形式化的语言来描述软件需求和特征,并且通过推理验证来保证最终的软件产品是否满足这些需求和具备这些特征。形式化方法研究的目的就是希望能够提供更好的理论、方法和工具,扩大形式化方法的应用范围和使用价值。

形式化方法的一个重要研究内容是形式规约(Formal Specification,也称形式规范或形式化描述),它是用具有精确语义的形式语言书写的程序功能描述,它是设计和编制程序的出发点,也是验证程序是否正确的依据。对形式规约通常要讨论其一致性和完备性等性质。形式规约的方法主要可分为两类:一类是面向模型的方法也称为系统建模,该方法通过构造系统的计算模型来刻画系统的不同行为特征;另一类是面向性质的方法也称为性质描述,该方法通过定义系统必须满足的一些性质来描述一个系统。不同的形式规约方法要求不同的形式规约语言,即用于书写形式规约的语言(也称形式化描述语言)。形式验证形式化方法的另一重要研究内容是形式验证(Formal Verification)。形式验证与形式规约之间具有紧密的联系,形式验证就是验证已有的程序系统是否满足其规约的要求,它也是形式化方法所要解决的核心问题。传统的验证方法包括模拟(simulation)和测试(testing),它们都是通过实验的方法对系统进行查错。

3 形式化方法的分类

根据说明目标软件系统的方式,形式化方法可以分为两类:

(1)面向模型的形式化方法。面向模型的方法通过构造一个数学模型来说明系统的行为。

(2)面向属性的形式化方法。面向属性的方法通过描述目标软件系统的各种属性来间接定义系统行为。

根据表达能力,形式化方法可以分为五类:

(1)基于模型的方法:通过明确定义状态和操作来建立一个系统模型(使系统从一个状态转换到另一个状态)。

(2)基于逻辑的方法:用逻辑描述系统预期的性能,包括底层规约、时序和可能性行为。采用与所选逻辑相关的公理系统证明系统具有预期的性能。用具体的编程构造扩充逻辑从而得到一种广谱形式化方法,通过保持正确性的细化步骤集来开发系统。

(3)代数方法:通过将未定义状态下不同的操作行为相联系,给出操作的显式定义。与基于模型的方法相同的是,没有给出并发的显式表示。

(4)过程代数方法:通过限制所有容许的可观察的过程间通信来表示系统行为。此类方法允许并发过程的显式表示。

(5)基于网络的方法:由于图形化表示法易于理解,而且非专业人员能够使用,因此是一种通用的系统确定表示法。该方法采用具有形式语义的图形语言,为系统开发和再工程带来特殊的好处。

4 形式化方法在软件开发中的应用

基于形式化方法的软件开发的基本思想是:用形式化规约语言精确地描述软件规约说明,然后由支持形式化的工具完全自动化或半自动化地转化为可执行代码。形式化方法在软件开发中能够起到的作用是多方面的。形式化方法的优势对于软件要求的描述同样适用于软件设计的描述。

4.1 需求分析

需求分析用户的需求从初始概念转换为需求文档,需求文档是与用户交流思想的主要基础。在需求阶段使用形式化方法将会更加完善形式化方法已知的益处,形式化方法中的符号系统将会变得更全面、更完整,它不仅能描述功能性的需求,而且亦能描述非功能性的需求。

4.2 系统规范

系统规范阶段主要描述系统而不涉及环境,这对于使用代数规范技术非常有利,它采用输入、输出间的关系来描述系统的行为。在此阶段,可以应用两种可能的形式技术:一个是发展代数技术以使其可应用于大型系统的规范(尚未见到代数规范应用于大型系统中的实例),这就要求此技术能将规范模块化;另一个是可能在技术上找到一条可以减少设计自由度的途径。

4.3 体系结构设计

体系结构设计阶段描述系统的接口、功能、结构的初步实现。在此阶段应用形式化方法的主要问题是,没有能够完成需求阶段所有工作的方法或符号系统。目前,形式化方法的使用者必须选择适合其应用领域特点的方法,或使用一种折衷的方法,从不同的形式化方法中找到一个合适的方法来完成此阶段的工作。

4.4 详细设计

详细设计是由体系结构规范出发的精化过程。精化可以使我们定义和验证同一系统的两个描述之间关系的正确性、一致性。详细设计中的保持结构观点与目前的精化技术是一致的,为使形式化方法能够应用于详细设计和精化过程,有必要采用一种折衷的方法,基于一种特殊的基础,研究如何将各种形式的(Formal and Informal)规范联系起来。

4.5 实现

在此阶段,已有大量的关于形式处理的工作,即将程序与其的规范形式地对应起来。形式实现技术在顺序程序上应用较广,目前也有对并发程序方面的研究。若要使形式实现技术能广泛地应用,还须对其做较大的改进,以提高其效率,降低其使用代价。

5 使用形式化开发软件系统的主要优势

软件开发自动化技术是提高软件生产率的根本途径之一。软件自动化的前提是形式化,形式化不仅仅是对用户需求,而且也是对整个软件系统的严格定义。使用形式化方法可以克服传统的软件开发方法的缺点。具体来说,使用形式化开发软件系统的主要优势有:

(1)形式化说明以逻辑精确性为特色, 除去了在非形式化说明中不可避免的大部分含糊不清的描述,这种精确性为开发人员与用户对需求的一致性理解, 及需求的正确执行提供了更大的可能性。

(2)形式化证明通过对需求分析中所描述的系统行为提供逻辑的精确论证, 除去了需求分析中的模糊性和主观性。

(3)通过形式化说明和证明实现了系统的重复分析、一致性分析以及一个较少依赖特定分析者技术和毅力的分析过程。

(4)形式化说明和证明可以通过“裁剪”以适合于给定的项目及技术要求, 也就是说能被调整以满足具体项目的需要。

(5)形式化说明和证明能够应用于任何开发阶段,包括目前最需要分析方法的开发早期,越早发现和确定错误比晚一些发现付出的代价要小的多。

(6)形式化说明和证明是基于计算机的工具所支持,这使得一致性检查和证明等实现了自动化,提高了系统的可靠性,减少了在分析方面的费用。同时,这些工具容许证明能够被重复执行而大大增强了分析的重复性。

(7)形式化说明和证明弥补了现有的测试方法, 通过提供一个精确的形式化说明而得以获取一个好的测试计划。

参考文献

[1]郑红军,张乃孝.软件开发中的形式化方法[J].北京大学学报,2005.

[2]吴会松.一种以面向对象及形式化技术为基础的严格的软件开发方法[J].郑州工业大学学报,1997(3).

[3]罗蜜,张为群.结合形式化方法的系统开发[J].西南师范大学学报,2003(4).

[4]试论软件的可靠性及其保证[J].软件世界,2004(10).