软件体系结构形式化方法

《软件体系结构形式化方法》由会员上传分享，免费在线阅读，更多相关内容在应用文档-天天文库。

1、五、软件体系结构形式化方法软件体系结构形式化方法是指在严格的数学基础（逻辑、代数、自动机、图论等）之上建立的软件开发方法，它是数学上的综合、分析技术的应用，用于开发计算机控制的系统。它可提供一个用于模型设计和分析的严格而有效的途径。其主要目的是克服自然语言、图表等非形式化方法描述体系结构存在的不足。由于形式化方法能在早起发现系统中的不一致、歧义、不完全和错误，目前己被证明是一种行之有效的减少设计错误的方法，是提高软件系统可信度的重要途径。开始的时候，研究人员运用形式化方法描述单个软件系统的体系结构或者体系结构风格。然后，逐步提出运用形式化方法描述和分析体系结构的通用模型

2、。根据对目标软件系统进行说明的方式，形式化方法可以分为如下两种：1、面向模型的方法。在面向模型的方法中，对目标软件系统的说明是为其构造一个模型，该模型的构成成分是一些具有特性的数据抽象，如域、元组、集合、序列、包、映射等。2、面向性质的方法。这种方法通过直接给出目标软件系统的一组特性来描述目标软件系统，通常是一组目标软件系统必须满足的形式公理。在面向性质的方法中，其形式规格说明仅描述目标软件系统的性质，而不涉及实现方法。根据表达能力，形式化方法大致可分为五类：1、基于模型的方法。给出系统（程序）状态和状态变换与操作的显式但亦是抽象的定义，但对于并发没有显式的表示，如基于

3、模型的形式规约语言Z和VDM。2、代数方法。通过联系不同操作间的行为关系而给出操作的隐式定义，而不定义状态，同样它亦未给出并发的显式的表示，如基于性质的代数规约语言OBJ，LARCH，CLEAR。3、过程代数方法。给出并发过程的一个显式模型，并通过过程间允许的可观察的通讯上的限制（约束）来表示行为，如CSP，CCP。4、基于逻辑的方法。有很多方法采用逻辑来描述系统的特性，包括程序允许的低级规范和系统时间行为的规范，如时态逻辑。5、基于网络的方法。根据网络中数据流显式地给出系统的并发模型，包括数据在网中从一个结点流向另一个结点的条件。如Petri网、谓词变换网。形式化方法

4、的研究和应用己有30多年的历史。最初的产生是由Dikstra和Hoare在程序难验证方面的工作中和Scott，Strachey以及其他学者在程序语义方面的工作基础上发展起来的。在软件开发过程中，用户需求的规格说明（体系结构描述）非常重要，其使用者包括用户、系统分析员、设计与编程人员、测试人员和验收人员。规格说明对这些人员来说是一个可靠的参照点；系统分析员接受用户的需求，产生目标软件系统的规格说明；设计与编程人员根据规格说明，进行模块设计并产生最终程序代码；测试人员和验收人员验证最终程序代码是否满足规格说明。非形式规格说明具有易读、易理解的优点，但是它通常具有歧义性，这往

5、往引起规格说明使用者对同一规格具有不同的理解，最终导致用户对已完成的系统产生不满。为了克服这些缺陷，人们提出了一种新的软件开发范型，即通过严格的、规范化的数学理论描述，这就是形式化方法分析与规格说明方法。形式化方法是基于数学的方法来描述目标软件系统性质的一门技术，用严格的数学符号和数学方法则对目标软件系统的结构与行为进行有效的综合、分析和推理，它为系统的说明、开发和验证提供了一个框架，利于发现目标软件系统需求中的不一致性、不完整性等方面。1基于粒度计算的形式化方法信息粒度是粒度计算的基本处理对象，是由相似的、功能接近或空间相邻的元素集合。定义.信息粒度是包含了多个属性信

6、息的信息实体，用三元组(P，V，F)表示，其中P表示属性集合，，，是x属性的值域，是信息函数，反映了信息粒度的全部信息。构件是软件系统的结构块单元，是软件功能设计和实现的承载体。不管是功能构件还是数据存储构件，从计算观点看，构件是具有计算特性的逻辑对象或实现单元，同时构件还包括其它的一些约束特性信息：可靠性、效率、接口特性、可维护性等。定义.软件构件是至少具有计算属性的信息粒度，是可重用的、相对独立的、具有不同的软件抽象层次的软件计算单位，表示了系统中主要的计算元素和数据存储。构件有两种：复合构件和原子构件。构件和构件之间通过连接件建立和维持行为关联和信息传递，连接件定

7、义了构件之间交互的规则并且给出了一些实现的机制。连接件并不一定对应具体的软件实现体，但一定规定了消息交换协议，如参数传递方式等。除此之外，连接件还可能具有方向性、响应度、角色等其它属性。定义.连接件是规定了构件之间消息交换协议的信息粒度，是应用于构件间进行连接通信的设计单元。在目前工程实践中，自然语言是最方便使用的描述语言，但自然语言具有歧义性、不一致性、不准确性等缺陷。为克服这些缺陷又不失自然语言的易理解、方便性，使用模糊理论来规范、模型化自然语言。模糊集合论的目的之一就是给自然语言的语义分析建立一个数学模型，概念用某论域上的模糊集表示