软件体系结构形式化方法的适用性考察

黎 明 唐朝霞

（湖南科技学院，湖南 永州 425199）

软件体系结构形式化方法的适用性考察

黎 明 唐朝霞

（湖南科技学院，湖南 永州 425199）

论文以一个销售管理系统形式化建模为例，考察了采用形式化方法的适用性原则并探讨了存在的问题。通过遵循试验证明，所提议的规则可以促进模型的简化、强化抽象概念的提取和明确抽象模型与具体模型的区别。在下一步工作中，需要讨论开发过程多阶段的形式化描述以及如何关联多阶段模型。

VDM-SL；需求定义；形式化方法；软件体系结构；形式化描述

0 引 言

为了解决软件危机、减少软件开发的成本费用，人们提出了两类解决方法：一类是采用工程化方法来组织管理软件开发过程，即软件工程方法。其中面向对象技术以及基于面向对象技术的软件架构开发流程是能较好控制成本的手段之一。一类是深入研究软件开发过程的规律，建立严密的数学理论，以指导软件开发实践。第一类方法中面向对象方法的软件架构能够描述出需求、设计以及实现等不同抽象水平的软件构造，但是，在现阶段还不能够很好地表达抽象水平不同的构造层次以及不同构造元素之间的关系。

A.Hall提出了使用基于形式化方法的软件体系结构的描述方法，可以准确地确定软件的构造元素间关系[1]。使用形式化方法进行软件开发的有用性，在 A.Hall的文献中详细地进行了说明。但是为了在实际的软件开发项目中使用形式化方法，还有必要讨论形式化方法时要注意的策略与基本原则。

本论文通过一个商品销售管理系统的实例，考察了基于形式化描述方法的描述模型和形式化方法的适用规则。

1 VDM-SL简介

形式化系统中最具有代表性的方法是 VDM(Vienna Development Method)方法，基本思想是运用抽象数据类型、数学概念和符号来定义软件开发中的运算和函数功能。在高层次的抽象模型上进行功能描述，能够让开发者获得对系统的深刻理解并能早期发现和避免实现细节错误的传递[2]。

VDM抽象层次高、语法严格，文法数学逻辑性强，它的核心元素为其标准化语言 VDM-SL。VDM-SL由一套数学表示系统和基于谓词逻辑、集合理论的推理规则组成，基于抽象数据建模，用抽象模型描述计算功能；并且可以采用Hoare风格断言描述推理规则。具有最少知识和简单准确的特点。已被广泛用于语言定义、需求分析和体系结构模型定义等领域[3]。

2 基于VDM-SL的描述模型和原则

由于上述VDM-SL的优点并且在国内有过较多的实际软件开发事例，本文决定采用VDM进行形式化描述，所预想的模型如图1所示。形式化模型需要描述需求定义、设计、实现的各层次；需要描述逻辑模型和物理模型之间存在关系；并且需求与设计、设计和实现等不同开发过程之间的关联关系也需要在模型中得到体现[4]。

以下论述主要聚焦于软件体系结构的输入部分：需求的描述，按照以下的原则使用VDM-SL来进行构建。

(1) 抽象模型 VDM-SL中使用类型（types）和函数（functions）进行描述。

(2) 具体模型 在抽象模型的基础上追加值的方式进行描述。

在抽象模型的描述中，只抽取了类型和函数对系统进行描述，这样做的目的是能使开发者在描述需求时不用考虑物理系统结构，促进系统的抽象化过程，可以不用纠结于过多的描述方法。另外，具体模型采用在抽象模型的基础上，将具体的数据作为值来进行定义。

图1 体系结构的形式化描述模型

3 基于形式化方法的销售管理系统的描述

销售管理系统管理包含销售商品的信息以及销售金额等销售数据，为了方便信息传递，对销售数据的格式进行了规定。在本部分的内容中，使用形式化方法，针对销售数据中的部分记录的需求进行了定义。

3.1 抽象模型

销售管理系统所涉及的抽象概念使用抽象模型进行描述，相关记录中的详细信息使用具体模型来进行描述。通过分析需求对象，以商品、分类、单价、销售记录、销售数量统计、销售金额统计的概念来表示需求内容。为了能描述这些概念，我们定义了以下的类型。

单价概念中，又分为现金销售的单价和会员卡销售的单价两种。 本文在具体模型中使用如下的方式进行定义。values

销售数额统计和销售金额统计概念也会有相同的问题，单价的定义同样也作为相关统计定义的对象。由于销售数额统计中有多个统计对象，因此将统计对象作为参数定义为相应的统计函数。

上述的单价的描述中，将现金销售单价和会员卡销售单价两个概念统一定义为单价表，使得现金销售单价和会员卡销售单价中的相同概念可以提取并抽象化。另外，含有多个统计对象的销售数额的统计，定义为销售数统计表函数，捕捉了其中的参数化概念并进行了抽象化。通过使用数据和操作的抽象化，将10个记录中含有的概念抽象为6个概念，实现了简单、明确的表达。

3.2 具体模型

具体模型阶段，明确从抽象模型中生成记录的基本概念。本文案例中的具体模型的描述规则如下：

（1）所有的记录当中，所含有的构成记录商品的序列号都是相同的。

（2）在具体模型中定义商品和分类等编码化的相关信息。

如下定义，采用商品列表来描述商品序列，用记录生成函数来构造商品记录。

通过定义记录生成函数，明确了具体模型生成记录的接口。记录生成函数明确了抽象模型中必要信息的构造，对抽象模型的进一步细化工作有较大的影响。另外，在具体模型的描述中，将与抽象模型中共有的类型、值、函数等概念进行细化和具体化，让两种模型得到连接，也可以在具体模型中找到对应的抽象模型，尽量避免需求过度或者需求误解。

4 形式化方法适用的效果和课题

4.1 形式化方法适用的效果

在上述构建需求的过程中，本文认为采用形式化方法可以得到以下的效果。

(1)使用VDM-SL的类型和函数定义所有的概念，这是进行概念整理的一种有效的手段。

(2)使用形式化方法手段可以在一定程度上避免因为个人理解差异，而造成需求定义的偏差。

(3)使用形式化描述方法，不能指望能将所需要表述的需求进行完全详尽的描述。

(4)通过摸索更加通用的类型和函数，在抽象化过程中进一步发现可以合并的抽象级别较高的概念。

(5)使用形式化方法进行定义模型时，我们必须对系统的全局概念比较清楚，可以促进开发者把握系统需求的整体概念。

4.2 抽象化方法的方针

通过上述的事例，我们可以得到以下抽象化方法的方针：

(1)省略非重要概念的具体描述：在抽象化过程中，概念过多会让模型复杂化，因此可以使用token,undefined字段简化模型。

(2)同一概念用一个类型来定义：如在单价概念定义的例子中，找出可以通用的类型来进行描述，促进模型的互操作性，避免相同概念的不同描述产生的歧义。

(3)抽象出可以参数化的函数：如记录生成函数的例子中，将记录生成概念中的相关处理模块化，将个数参数化，定义出参数化函数。

(4)抽取通用化的函数：如销售数统计表函数的例子中，根据功能的共同部分抽选出通用部分，定义为函数，提高抽象化程度。

4.3 形式化方法适用的课题

使用形式化方法描述需求还存在以下的课题：

(1)存在使用自然语言可以很简单地进行描述，但使用形式化会变得复杂的场景。

(2)存在使用形式化的表达使得需求难以理解的场景。

以上的问题，主要是由于缺少在各种场景中的形式化描述实例，因此，能够公开在实际开发现场中使用形式化方法描述需求的案例的相关信息是解决上述问题的重点。

在具体的开发实例中为了描述需求，使用图比较多，而VDM-SL中，虽然可以使用解释器执行已经具体化的形式化描述，但还没有解析和生成图的功能。如果可以将解释器执行时的数据、数学模型图示化，这样就可以做到执行的可视化，对形式化语言的需求描述理解有更好的支援效果。

5 结束语

本文通过以使用形式语言VDM-SL来描述销售管理系统的需求，考察了在开发中采用形式化方法的原则以及还存在的课题。通过遵循形式化方法描述的规则，可以促进模型的简化、强化抽象概念的提取和明确抽象模型和具体模型的区别。在今后的工作中，进一步讨论如何在开发阶段，在将需求模型形式化时给出需遵循规则的提示。 并且关注设计阶段的形式化描述以及如何衔接需求与设计之间的关联。

[1]Jim.Woodcock, Peter.Gorm.Larsen, Juan.Bicarrequi.Formal methods:Practice and experience[J].ACM Computing Surveys, 2009,(10):119-126.

[2]曹重华,白似雪,杨锦云.维也纳分析方法及其应用[J].南昌大学学报(理科版),2005,(2):99-102.

[3]齐学智,陈金水.从形式化式样出发的实时控制软件开发[J].工业控制计算机,2004,(8):28-29.

[4]王昌晶,罗海梅,左正康.基于问题模式的形式化软件规格说明生成方法[J].计算机研究与发展,2013,(2):352-360.

TP311.5

A

1673-2219（2014）05-0122-03

2013－12－17

2013年永州市科技局科技计划项目 “学校信息系统应用集成研究”。

黎明（1974－），男，湖南永州人，硕士，讲师，主要研究领域为分布对象计算，计算机网络，软件工程。

（责任编校：刘志壮）