软件形式化开发方法的选择策略研究

彭 成，王盼卿

（军械工程学院 河北 石家庄 050003）

自从20世纪60年代中期由于软件规模越来越庞大，结构也越来越复杂，环境的复杂性，应用领域的复杂性，交流的复杂性，爆发了软件危机．软件开发费用和进度失控，软件的可靠性差，生产出来的软件难以维护，用户对＂已完成＂的系统不满意现象经常发生，如何开发软件，以满足不断增长、日趋复杂的需求；如何维护数量不断膨胀的软件产品等一系列问题始终困扰着软件开发人员，为了解决软件危机，软件开发人员提出了两种解决问题的方法，一种就是众所周知的软件工程方法，即把工程的思想引入软件开发，另外一种方法就是形式化方法．形式化方法用于软件开发可以保证软件的正确性。形式化方法基于严格的数学，在软件开发过程中使用数学具有如下优点：数学是准确的建模媒体，能够对现象、对象、动作等进行简介、准确的描述；数学支持抽象，它使得规格的本质可以被展示出来，并可以以一种有组织的方式来表示系统规格中的抽象层次；数学提供了高层确认的手段，可以使用数学证明来揭示规格中的矛盾和不完整性，以及用来展示设计和规格之间的一致性情况[1]。

1 形式化方法的发展

形式化方法（Formal Method）的基本含义是借助数学的方法来研究计算机科学中的有关问题.《Encyclopedia of Software Engineering》对形式化方法定义为:“用于开发计算机系统的形式化方法是基于数学的用于描述系统性质的技术。这样的形式化方法提供了一个框架，人们可以在该框架中以系统的方式刻划、开发和验证系统”[2]。换言之，在软件开发的全过程中，凡是采用严格的数学语言，具有精确的数学语义的方法，都称为形式化方法。

在逻辑科学中是指分析、研究思维形式结构的方法。它把各种具有不同内容的思维形式（主要是命题和推理）加以比较，找出其中各个部分相互联结的方式，如命题中包含概念彼此间的联结，推理中则是各个命题之间的联结，抽取出它们共同的形式结构；再引入表达形式结构的符号语言，用符号与符号之间的联系表达命题或推理的形式结构。例如，把全称肯定命题，用符号形式化为“SAP”；把联言命题、假言命题分别形式化为:“p∧q、“p→q”。 又例如:一个具体的假言联言推理“如果这种金属是纯铝，那么它的物理性质必与纯铝相同；如果这种金属是纯铝，那么它的化学性质必与纯铝相同；但这种金属的物理性质和化学性质与纯铝不相同；所以，它不是纯铝。”这个推理的形式结构是:“如果p，则q；如果p，则 r；非 q且非 r；所以非 p。”可进而形式化为下列公式:（（p→q）∧（p→r）∧┐q∧┐r→ ┐p。

软件形式化方法最早是对于程序设计语言编译技术的研究，即J.Backus提出的BNF描述Algol60语言的语法，出现了各种语法分析程序自动生成器以及语法制导的编译方法，使得编译系统的开发从＂手工制作方式＂发展成具有牢固理论基础的系统方法.经过30多年的研究和应用，如今人们在形式化方法这一领域取得了大量重要的成果，从早期最简单的形式化方法一阶谓词演算方法到现在的应用于不同领域、不同阶段的基于逻辑、状态机、网络、进程代数、代数等众多形式化方法。形式化方法的发展趋势逐渐融入软件开发过程的各个阶段，从需求分析、功能描述（规约）、（体系结构/算法）设计、编程、测试直至维护。随着形式化研究的热潮，涌现出了多种形式化方法如：RSL（RAISE specification Language），B，VDM（Vienna Development Method），Z 等等。 因此，在具体的软件开发中选择何种形式化方法显得至关重要。

图1 常规方法和形式化方法的比较Fig.1 Comparison of the conventional method and formal method

2 与常规软件工程方法比较

随着信息社会的不断发展，软件系统开发呈现出复杂化的趋势，伴随着软件系统越来越庞大，常规的软件工程方法显得力不从心，而形式化方法对于开发大规模、复杂的系统显得游刃有余。

形式化方法和工程界的常规方法相比有明显的区别.它们的开发原则不同:形式化方法希望能直接构造出尽可能正确的系统；而常规方法主要是通过测试来发现系统的错误[3]。形式化方法和常规方法开发方法的比较如图1所示。

为了更加直观的展示形式化语言的特性，我们通过在企业员工管理系统中雇员信息管理中两种方法的对比可以看出形式化方法基于严格的数学的优势。用自然语言描述系统功能为：将一个公司雇员的信息登录到数据库；检查一个雇员的信息是否已经登录到数据库；返回当前在数据库中登录的雇员人数[4]。

形式化方法规格说明（RSL）

scheme STAFFDATABASE=

class

type

Staff，

StaffDB=Staff-Set

value

empty:StaffDB，

register:Staff×StaffDB→StaffDB，

check:Staff×StaffDB→Bool，

number:StaffDB→Nat

axiom

empty≡{}

∀s:Staff，stb:StaffDB·register（s，stb）≡{s}∪stb

∀s:Staff，stb:StaffDB·check （s，stb）≡s∈ stb

∀stb:StaffDB·number（stb）≡card stb

end

传统的常规方法对问题的描述易出现矛盾、二义性和含糊性，缺乏准确的语义对模型难以进行一致性检查和正确性分析，进而限制其有效性。而对于形式化方法来说，由于其基于严格的数学，具有严格的语法和语义定义，从而可以准确的描述系统模型，排除了矛盾、二义性、含糊性等情况。

3 形式化方法选择策略

3.1 常用的软件形式化方法

常用的软件形式化方法有RSL，B，VDM，Z等等。

1）RSL

RSL代表RAISE规格说明语言。RAISE是Rigorous Approach to Industrial Software Engineering的缩写，指面向工业软件工程的严格方法[5]。RAISE是在一个广谱的规范语言基础上，提供一系列工具和转换技术，形成一种开发软件的严格方法。它既可以用于书写非常抽象的、初级的规范，也可以用于书写易于自动转换到程序语言的更具体的规范。

2）B

B是目前国际上最受重视的实用性软件形式化方法之一，B语言是由Z语言发展而来的，其目的是为这种形式化方法增强模块能力和工具支持能力。B语言称为一种广谱语言和方法，它既包括高度抽象的数学描述，又包括了可执行的描述。B语言支持规格说明，并且支持继规格说明之后所有的精化和设计步骤[6]。

3）Z

Z规格说明语言是在1979年由J.Abrial和S.Schumann最早提出的，而后由Hoare所领导的牛津大学程序设计研究小组（PRG）进行了大量的研究工作[7]。Z语言以一阶谓词逻辑和集合论作为形式语义基础，利用集合、序列、包等数学概念对目标软件的结构特性和行为特性进行抽象描述，它具有简明、精确、无歧义的优点[8]。成功的应用例子有英国Hursley的IBM公司将 Z应用到 CICS（Custom lnformation and Control System）系统软件，牛津大学的PRG将Z应用于为Transputer Inmos T800版本提供的浮点运算支持等。

4）VDM

VDM是由IBM公司维也纳实验室的研究小组于20世纪70年代提出来的一种形式化方法。VDM建立的初衷，是为了实现PL/1语言的严密、精确语义规格。20世纪70年代末至80年代初，VDM在欧洲开始得到推广应用，它先是应用于开发程序语言的语义形式说明，以后逐渐成为一般软件的开发方法。进入20世纪90年代，VDM在欧美许多研究机构和大学得到了广泛的应用，当时一些大学，如英国的曼彻斯特大徐等，将VDM作为大学计算机系的必修课程。1996年，国际标准化组织ISO制订了VDM的国际化标准版本VDM-SL.目前，VDM已成为应用最为广泛的形式化规格语言之一。

4.2 特点分析

所有的形式化方法都是以数学为基础的.RSL和Z都是基于集合论和一阶谓词演算的，Z中还包含有模式的概念，B以集合论为基础，B的语义是建立在Abrial广义替换语言和用谓词变换和扩展的Dijkstra最弱前置条件演算基础上。VDM的基础是集合论和部分函数。

形式化方法采用基于模型（Model-oriented）或基于性质（Property-oriented）的方法，并且方法的严格化程度不同。基于模型的形式化利用一些已知特性的数学抽象来为目标软件系统的状态特征和行为特征构造模型。基于特性的形式化方法不直接定义系统的行为，而是用一组公理的形式来描述系统的各种性质。

B，VDM，Z是基于模型的方法，RSL是两种方法的混合体。

VDM是B，Z，VDM，RSL中最早的一种语言，其实VDM不仅是一种语言，还是一种开发方法，RSL与VDM是三值逻辑（真、假、未定义的），B，Z 是二值逻辑（真，假），但 VDM 没能提供组装/分解规格说明和精化的机制。

RSL与VDM都能描述系统功能，用于顺序程序的设计，并可描述并发，B和Z只能描述系统功能和顺序程序的设计。

RSL和B都具有广谱的特性，而VDM和Z都没有，B，VDM和Z都已经有了国际标准，RSL到目前为止还没有国际标。4种语言的特点比较如表1所示。

表1 4种形式语言特点的比较Tab.1 Comparison of the four forms of language features

3.3 选择策略

基于以上分析我们可以得出如下的选择策略：对于所要开发的系统具有时间跨度长、经费充足、软件质量要求高而且软件开发小组的人员素质高，对形式化方法比较了解的情况，我们推荐采用形式化的开发方法；具体来讲，当所要开发的系统中带有较多并发操作时选择RSL，VDM形式规格说明过于形式化往往不容易理解，因而VDM适合对本方法特别熟悉的软件开发小组，B语言是一种支持从规格说明到代码生成整个开发过程的形式化方法，因此需要软件自动化程度高的系统开发推荐使用B方法。软件系统的Z模式规格说明可以按一定的层次结构给出。模式的使用为规格说明提供了一种演算，通过这种演算无论多么大型系统的规格说明都可以通过一个个小的部分来构成，因此Z适合于规模较为庞大的巨系统的研发。

4 结束语

本文介绍了解决软件危机的除软件工程外的另一种方法：形式化方法，形式化方法利用了数学的严密性来解决在软件危机中出现的各种歧义性等问题，并给出了几种常用的形式化方法：RSL，B，VDM，Z，然后对它们的特点进行了分析比较，并给出了适合形式化方法的情况和形式化方法选择策略。可以预计，在将来形式化方法可能会融入到信息技术的各个领域并成为一种主流的方法和技术.

[1]李莹，吴江琴.软件工程形式化方法与语言[M].浙江：浙江大学出版社，2010.

[2]焦蕾.Agent结构的形式化描述及研究 [J].电子设计工程，2012，16（4）：51-55.JIAO Lei.Description and study of Agent structure[J].Electronic Design Engineering，2012，16 （4）:51-55.

[3]Milner R.A complete inference system for a class of regular behaviors[J].Journal of Computer and System Sciences，2009，28（3）:439-466.

[4]Hoare C A R.Communicating Sequential Processes[M].New York:Prentice Hall，2010.

[5]塔维娜，何积丰.基于形式化方法的需求分析[J].计算机工程，2010，26（18）:107-113.TA Jina，He Jifeng.Requirement analysis based on formal method[J].Computer Engineering，2010，26（18）:107-113.

[6]Brookes S D，Hoare C A R，Roscoe A W.A theory of communicating processes[J].Journal of the ACM，2009，31（3）:560-599.

[7]陈怡海，缪淮扣.两种形式语言:RSL与Z的分析比较[J].计算机应用与软件，2002，18（4）:56-60.CHEN Yi-hai，MIAO Huai-kou.Two kinds of language:the analysisof RSLand Zin comparison[J].Computer Applications and Software，2002，18（4）:56-60.

[8]Hennessy M，Milner R.Algebraic laws for nondeterminism and concurrency[J].Journal of the ACM，2009，32（1）:137-161.