黎 明 唐朝霞

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

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

黎 明 唐朝霞

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

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

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

0 引 言

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

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