《[2017年整理]软件体系结构形式化方法》由会员分享，可在线阅读，更多相关《[2017年整理]软件体系结构形式化方法（47页珍藏版）》请在金锄头文库上搜索。
1、 软件体系结构形式化方法软件体系结构形式化方法是指在严格的数学基础（逻辑、代数、自动机、图论等）之上建立的软件开发方法，它是数学上的综合、分析技术的应用，用于开发计算机控制的系统。它可提供一个用于模型设计和分析的严格而有效的途径。其主要目的是克服自然语言、图表等非形式化方法描述体系结构存在的不足。由于形式化方法能在早起发现系统中的不一致、歧义、不完全和错误，目前己被证明是一种行之有效的减少设计错误的方法，是提高软件系统可信度的重要途径。开始的时候，研究人员运用形式化方法描述单个软件系统的体系结构或者体系结构风格。然后，逐步提出运用形式化方法描述和分析体系结构的通用模型。根据对目标软件系统进行说
2、明的方式，形式化方法可以分为如下两种：1、面向模型的方法。在面向模型的方法中，对目标软件系统的说明是为其构造一个模型，该模型的构成成分是一些具有特性的数据抽象，如域、元组、集合、序列、包、映射等。2、面向性质的方法。这种方法通过直接给出目标软件系统的一组特性来描述目标软件系统，通常是一组目标软件系统必须满足的形式公理。在面向性质的方法中，其形式规格说明仅描述目标软件系统的性质，而不涉及实现方法。根据表达能力，形式化方法大致可分为五类：1、基于模型的方法。给出系统（程序）状态和状态变换与操作的显式但亦是抽象的定义，但对于并发没有显式的表示，如基于模型的形式规约语言 Z 和VDM。2、代数方法。通
3、过联系不同操作间的行为关系而给出操作的隐式定义，而不定义状态，同样它亦未给出并发的显式的表示，如基于性质的代数规约语言OBJ， LARCH， CLEAR。3、过程代数方法。给出并发过程的一个显式模型，并通过过程间允许的可观察的通讯上的限制（约束）来表示行为，如 CSP， CCP。4、基于逻辑的方法。有很多方法采用逻辑来描述系统的特性，包括程序允许的低级规范和系统时间行为的规范，如时态逻辑。5、基于网络的方法。根据网络中数据流显式地给出系统的并发模型，包括数据在网中从一个结点流向另一个结点的条件。如 Petri 网、谓词变换网。形式化方法的研究和应用己有 30 多年的历史。最初的产生是由 Dik
4、stra 和Hoare 在程序难验证方面的工作中和 Scott，Strachey 以及其他学者在程序语义方面的工作基础上发展起来的。在软件开发过程中，用户需求的规格说明（体系结构描述）非常重要，其使用者包括用户、系统分析员、设计与编程人员、测试人员和验收人员。规格说明对这些人员来说是一个可靠的参照点；系统分析员接受用户的需求，产生目标软件系统的规格说明；设计与编程人员根据规格说明，进行模块设计并产生最终程序代码；测试人员和验收人员验证最终程序代码是否满足规格说明。非形式规格说明具有易读、易理解的优点，但是它通常具有歧义性，这往往引起规格说明使用者对同一规格具有不同的理解，最终导致用户对已完成的
5、系统产生不满。为了克服这些缺陷，人们提出了一种新的软件开发范型，即通过严格的、规范化的数学理论描述，这就是形式化方法分析与规格说明方法。形式化方法是基于数学的方法来描述目标软件系统性质的一门技术，用严格的数学符号和数学方法则对目标软件系统的结构与行为进行有效的综合、分析和推理，它为系统的说明、开发和验证提供了一个框架，利于发现目标软件系统需求中的不一致性、不完整性等方面。1 基于粒度计算的形式化方法信息粒度是粒度计算的基本处理对象，是由相似的、功能接近或空间相邻的元素集合。定义.信息粒度是包含了多个属性信息的信息实体，用三元组(P，V ，F) 表示，其中 P 表示属性集合， ， ， 是 x 属
6、性的值域， 是信xVPVPF:息函数，反映了信息粒度的全部信息。构件是软件系统的结构块单元，是软件功能设计和实现的承载体。不管是功能构件还是数据存储构件，从计算观点看，构件是具有计算特性的逻辑对象或实现单元，同时构件还包括其它的一些约束特性信息：可靠性、效率、接口特性、可维护性等。定义.软件构件是至少具有计算属性的信息粒度，是可重用的、相对独立的、具有不同的软件抽象层次的软件计算单位，表示了系统中主要的计算元素和数据存储。构件有两种：复合构件和原子构件。构件和构件之间通过连接件建立和维持行为关联和信息传递，连接件定义了构件之间交互的规则并且给出了一些实现的机制。连接件并不一定对应具体的软件实现
7、体，但一定规定了消息交换协议，如参数传递方式等。除此之外，连接件还可能具有方向性、响应度、角色等其它属性。定义.连接件是规定了构件之间消息交换协议的信息粒度，是应用于构件间进行连接通信的设计单元。在目前工程实践中，自然语言是最方便使用的描述语言，但自然语言具有歧义性、不一致性、不准确性等缺陷。为克服这些缺陷又不失自然语言的易理解、方便性，使用模糊理论来规范、模型化自然语言。模糊集合论的目的之一就是给自然语言的语义分析建立一个数学模型，概念用某论域上的模糊集表示，同时定义语气算子和模糊算子、模糊集上的各种运算、模糊句型、模糊推理。由于软件体系结构设计是软件设计的早期决策，存在许多的模糊信息和不完
8、全知识，可以规定，信息粒度中属性值以模糊集合表示。设信息粒度具有某属性P，建立关于 P 的论域 Up，p 的属性值就可用 Up 上的模糊集表达，Up 的建立上下文相关。例如构件的可靠性，假设分为 7 个等级，其论域可设计为-3，-2， -1，0，1， 2，3，则可靠性的值“好、一般”等语言值是其论域上的模糊集。一般的可划分等级的属性都可依此定义论域。这种建立在模糊理论基础上的信息描述，近似于自然语言，又具有形式语言的严密性、可推理性。构件和连接件的设计就是尽量实现其所有属性满足要求值的过程。Bass 等人认为，软件体系结构包括构件、构件的外部可见性以及相互的关系。可见性是指构件提供的服务、性能
9、、特性等。EGSA-ADL19也总结软件体系结构是：“在软件密集的大规模系统或具有类似需求和结构的软件产品线的开发中，必须从一个较高的层次来考虑组成系统的构件、构件之间的交互，以及由构件与构件交互形成的拓扑结构，这些要素应该满足一定的限制，遵循一定的设计规则，能够在一定的环境下进行演化。而且，软件体系结构应能反映系统开发中具有重要影响的设计决策，便于各种人员的交流，反映多种关注，据此开发的系统能完成系统既定的功能和性能需求” 。据此，可以定义：定义.软件体系结构是一个由构件、连接件及其形成的拓扑结构构成的粒度空间。设构件集合为 C，连接件集合为 A，拓扑结构关系为 S，软件体系结构SA=(C，
10、A ， S)。传统的粒度空间定义为信息粒度的集合，信息粒度间不包括结构关系，我们的粒度空间处理信息粒度之间的结构信息，是传统粒度空间的拓展。我们以图表示 SA，构件和连接件为节点，构件之间仅通过连接件建立关联，则 S 是构件和连接件之间的边集。每个连接件至少邻接两个构件，连接件相邻没有意义。规定一个软件体系结构中不允许存在孤立的构件或构件子集，不允许存在并行边。这是符合现实的，构件总是互相交互的，体系结构的一个部分总是和其它部分有着某种形式的联系。几个构件之间如果彼此有多种形式的交互，在语义上可以合并成更高抽象的一种交互形式。因此有：定义.在构件和连接件是否关联的语义下，软件体系结构 SA=(
11、C， A，S)是一个连通的简单二部图，其中 C， A 为节点集，S 是构件和连接件之间的边集。且具有以下约束：(1).对于 ， x 的度数至少为 2。(2).不存在这样的集合 ， 的元素个数大于 1，对于 ，存在A11 1Ax某一非空子集 ， 且 。C1 Syx),( SzCz),(图 2.1 显示了三个结构图， （1）图是合法的软件体系结构图， （2）图不符合上面的定义， （3 ）图 a4 是（2）图 al 和 a2 合并而成，在语义上等价（ 2）图，为表示、处理的归一化、简单化，按上面的定义规定（2）图是不合法的软件体系结构图， （3 ）图是合法的软件体系结构图。（1） （2 ） （3）图
12、 2.1 软件体系结构图用邻接矩阵 X 表示 SA，设 C 的基数为 m， A 的基数为 n， ，由二部图性质，当(im 且 jm)时，)(nmijxX=0，同时邻接矩阵是对称矩阵，单纯从连接语义看，X 可以压缩成 mn 矩ij阵 X，称为简化矩阵。图 2.1(1)的 ，010100X。10XS 的边如果赋以权值，表示交互强度、频度等语义，S 图成为模糊图，X 和X可解释为 C 和 A 上的模糊关系。这种加权的结构邻接矩阵可以表达多维语义。不同的属性，赋以不同的权值，表示在此属性维度上 C 和 A 中元素之间的模糊关系，得到此属性维度上矩阵 Xp 和 Xp ，pP。结构图右上部分(im)还可表
13、达连接件角色语义，左下部分 (im 且 jSA2。SA1 可经由 1 个编码过程转化成 SA2，称 SA2 是 SA1 的直接细化，记为 SA1SA2 。显然， 是自反的、可传递的。定义 7.如果 SA1SA2， SA1=(C1，A1，S1) ，SA2=(C2，A2 ，S2)，则SA1 可由 SA2 经如下规定的解码过程形成：(1).对集合 C2 进行某关系 R 划分得商集 C2/R，对于 ，有集合RCc/2Aca1|a1A2， ，设)1,(2()1,( SayCySaxCc 且c1（Cc，Ac，Sc） ，Sc (c，a)|cCc，aAc 有（c，a ）S2 且 (C2-cCc)， ，c1 叫
14、做复合构件，C1=c1 ， A1= A2 -Ac。2),(Sac(2 ).设以 C1 和 A1的元素为点集形成结构 SA1=(C1，A1，S1)，S1=( ，y)bc| C1 ，设 （Cc，Ac，Sc） ，yA1， 。SA1 不一定是bcbc 2),(SyxCc合法的体系结构。(3).如果有元素个数大于 1 的集合 ， 存在非空集合11,AaA有 且 ， 则设,3,13Cx,S)x,a2(),2(3(SyCy。 叫做复合连接件。(A1(4).以 C1 和 A1 的元素为点形成软件体系结构 SA1， S1=(x，y)|xC1，yA1， a3y 有（x，a3）S1。划分关系 R 可以依据构件功能相
15、似性、耦合紧密度等。图 2.2 展现了一个软件体系结构解码过程例子，SA2 中部件划分为Cl，C2，C3，C4 ，C5，经解码 1， 2 步骤得 SA1， SA1经 3，4 步骤得 SAl。图 2.2 软件体系结构的结构演化显然，上述定义说明了软件体系结构演化中结构的分解和合成所应遵守的约束，可以清楚地跟踪构件和连接件的变化轨迹。从形式上看，复合构件(Cc， Ac， Sc)与体系结构相似，但复合构件并不等同软件体系结构。定理 2. 设所有软件体系结构的集合为SA，所有复合构件的集合为c1 ，则SA c1，即所有的软件体系结构都是复合构件，但存在不是软件体系结构的复合构件。证明：设有任意软件体系结构(C， A， S)，把 C 中所有元素作为一个划分解码，由定义 7 得整个软件体系结构为一个复合构件，因此SA cl。又图 2.2 中 SA2 中 c4， c5 是一划分，解码后得复合构件(c4+c5)， (c4+c5)内部没有连接件，显然 c4， c5 不相邻，(c4+c5)部件的结构拓扑是零图，不连通，由定义 5 知体系结构的结构拓扑为连通图，所以(c4+c5)构件不是软件体系结构，由此SA c1 ，(证毕)。一般认为，复合构件是由多个构件组成，我们的模型反映复合构件是由多个构件及这多个构件内部交
