利用支持体系结构动态变化的图文法验证体系结构的方法

技术领域

本发明属于软件体系结构领域，具体涉及利用支持体系结构动态变化的图文法验证 体系结构的方法，尤其涉及图文法理论、软件体系结构动态演化理论。

背景技术

在图形化技术中，Le Métayer使用了图文法来形式化的定义软件体系结构，将图中 的节点映射成体系结构中的构件/连接子，边映射成构件间的交互关系，此外，他还采 用了类似通信顺序进程的标注来对支持体系结构风格和实例的定义。Hirsch等人则采用 超图的方式来定义软件体系结构，他们利用图重写规则来表达体系结构的动态演化过 程。Le Métayer和Hirsch的方法都不支持对软件体系结构模型中，接口的规约。Rekers 和Schürr则基于对象之间的空间关系，提出了一种上下文敏感的图文法Layered图文 法，它允许左图和右图中含有任意节点的节点和边，并给出了一种高效的图解析算法。 虽然layered图文法作为一种形式化的图语言比较容易理解，但是其语法的解析较为复 杂并且实现的效率较低。Zhang等人在此基础上，提出了另一个上下敏感的图文法 Reserved图文法。Reserved图文法使用标记图的方式来改进算法的实现效率并降低了 图解析的复杂度，同时结合UML来定义、验证及转换软件系统，但未说明如何来实现软 件体系结构的刻画。柏林工业大学的图文法研究小组也开发了一个基于规则的可视化语 言Attributed图文法，用来规约复杂的图形化数据结构。一些自适应系统也是使用了 Attributed图文法实现了系统自动分析和验证，并且可对系统的类型和约束进行建模。 然而，Attributed图文法的开发和设计并不是针对软件体系结构的设计和规约。

发明内容

本发明的目的在于对通用图文法进行扩展，引入接口、接口标签集、状态及附加属 性的信息，从而能够高层抽象软件系统的组成结构、连接方式以及系统结构配置及属性 等要素，完整地支持软件体系结构的建模、分析和动态演化。同时，通过给出Breeze 图文法中的产生式规则，能够描述软件体系结构的动态重配置(增、删操作)，满足开 放的网络环境和变化的用户需求。此外，通过Breeze图文法在对软件体系结构进行规 约的同时还可以捕获在软件开发初期和后期演化过程中动态变换，基于Breeze图文法的 形式化基础，通过推导验证，保证演化后的一致性和完整性。

根据本发明提供的一种利用支持体系结构动态变化的图文法验证体系结构的方法， 包括如下步骤：

步骤1，定义Breeze图文法

将Breeze图文法定义为六元组(G,P,TL,NL,TA,NA)，其中：

-G表示Breeze图；

-P表示可应用于G的产生式规则集；

-TL表示终端标签集；

-NL表示非终端标签集；

-TA表示终端属性集；

-NA表示非终端属性集；

Breeze图G定义为一个七元组(N,E,l_N,l_E,s,t，a_N)，其中：

-Breeze图G七元组中的N记为N(G)，N(G)是一个有限的节点集；

-Breeze图G七元组中的E记为E(G)，E(G)是一个有限的边集；E(G)定义为 {(n.CN_i,m.CN_j)∈N.CN×N.CN},n,m∈N并且i,j∈I；其中，n表示复合节点n， m表示复合节点m，CN_i表示子节点i，CN_j表示子节点j，n.CN_i表示复合节点n上的接口 子节点CN_i，m.CN_j表示复合节点m上的接口子节点CN_j，N表示通用节点集，CN表示接 口子节点集，N.CN表示节点集中的接口集，下标i表示节点索引号，即第i个节点，下 标j表示表示节点索引号，即第j个节点；I表示索引集；

-Breeze图G七元组中的l_N记为l_N(G)，l_N(G)是给定的节点标签函数，表示在 Breeze图G中，将通用节点集N与节点标签集L_N相关联；其中，Breeze图G中的L_N记 为L_N(G)，L_N(G)定义为{(T_i,S_j)∈T×S}，i,j∈I；其中，T_i表示节点类型集T中的第 i种节点类型，S_j表示节点状态集S中的第j个状态类型；T定义为{component, connector,X}，component表示构件，connector表示连接子，X表示节点初始化时的 类型；S定义为{Waiting,Active,Temporary Failure,Fatal Failure}，Waiting表 示构件或连接子创建后的初始状态，Active表示构件或连接子正常工作状态，Temporary  Failure表示构件或连接子临时失效状态，Fatal Failure表示构件或连接子致命失效 状态；

-Breeze图G七元组中的l_E记为l_E(G)，l_E(G)是给定的边标签函数，表示在 Breeze图G中，将通用边集E与边标签集L_E相关联；

-Breeze图G七元组中的a_N记为a_N(G)，a_N(G)是节点属性标记函数，表示在 Breeze图G中，将通用边集E与构件或连接子属性集A_N相关联；

-Breeze图G七元组中的s,t记为s(G),t(G)，s(G),t(G)是函数，表示在Breeze 图G中，将每条边与该边对应的源节点和目标节点的接口相关联；

l(G):＝l_CN(n)∪l_N(G)∪l_E(G)代表Breeze图G中所有接口、节点和边的标签集；

产生式规则集P由左手边规则图LHS、右手边规则图RHS构成；LHS与RHS拥有一 个公共子图CG，其中，公共子图CG需满足如下条件：

-任何一个属于CG的节点也一定属于LHS和RHS；

-任何一个属于CG的边也一定属于LHS和RHS；

-CG的标签集是LHS的标签集和RHS的标签集的公共部分；

-CG的属性集是LHS的属性集和RHS的属性集的公共部分；

对于产生式规则集P中的任意一个产生式规则实例p，定义为一个二元组(L，R)， 其中：

-L表示左手边规则；

-R表示右手边规则；

R是一个非空的连通图，L和R都是基于相同的标签集L_G和属性集A_G，L_G由TL和NL 构成，A_G由TL和NL构成；

Breeze图文法中的节点为复合节点，即将接口作为子节点引入到构件节点中；

复合节点定义为一个四元组(pn,CN,l_CN,a_CN)，其中：

-复合节点四元组中的pn是一个父节点，即构件或连接子的主体部分；

-复合节点四元组中的CN是一个子节点集，即构件或连接子的接口；

-复合节点四元组中的l_CN是作用在子节点上的标记函数，表示将复合节点上 的子节点集CN与标签集L_CN相关联，其中，L_CN定义为{T_i'∈T'},i∈I；T_i'表示第i个复 合节点的接口类型，接口类型集T'定义为{I,O,I/O,X}，其中，I、O、I/O分别代表接 口是服务请求者、服务提供者、服务请求/提供者，X表示处于初始化期间的接口还未指 派接口类型；

-复合节点四元组中的a_CN是作用在子节点上的接口属性标签函数,表示将复合 节点上的子节点集CN与接口属性集A_CN相关联；其中，A_CN是构件或连接子的接口属性集；

步骤2，定义Breeze图文法重配置操作；

步骤3，利用Breeze图文法推导验软件证体系结构的一致性或完整性。

优选地，所述步骤2包括：重配置添加构件和连接子，具体为：

假定当前Breeze图为CS，CS中含有构件类型为S的构件s，若需要引入与构件s 通讯且构件类型为C的构件c，则令该构件c通过其接口Req发送请求，同时引入连接 子类型为CON的连接子con，该连接子con通过其接口Res接收来自构件c的请求，构 件s通过其接口Res接收来自连接子con的接口Req发来的请求。

优选地，所述步骤2包括：删除构件和连接子，具体为：

假定当前Breeze图为CS，需要删除与构件类型为S的构件s相连接的构件类型为 C的构件c，则删除构件c，同时移除负责构件s与构件c之间通讯的连接子类型为CON 的连接子con。

优选地，所述步骤3包括步骤：

利用Breeze图文法推导验证体系结构的一致性，包括：

假设通过重配置添加操作给体系结构SA增加了一个新的构件Com_s，并通过连接子 Conn_z进行交互，K、T分别是构件Com_s和连接子Conn_z对外隐藏的操作，则一致性保障 验证条件为如下形式：

若满足一致性保障验证条件，则一致性验证通过，否则不通过；

其中：

表示：A所指代对象与B所指代对象的行为一致；

A||B表示：体系结构在运行过程中，A所指代对象和B所指代对象的交互行为是并 发的；

A\B表示：B所指代对象是A所指代对象对外隐藏的操作。

优选地，所述步骤3包括步骤：

利用Breeze图文法推导验证体系结构的一致性，包括：

假设通过重配置替换操作将体系结构SA中的构件Com_i、连接子Conn_j分别替换为 构件Com_s、连接子Conn_z，C是构件Com_s对外隐藏的操作，则一致性保障验证条件为 如下形式：

若满足一致性保障验证条件，则一致性验证通过，否则不通过；

其中：

f:A→B表示：B所指代对象能够模拟实现A所指代对象的行为；

A||B表示：体系结构在运行过程中，A所指代对象和B所指代对象的交互行为是并 发的；

表示：非；

A||B表示：将A所指代对象替换为B所指代对象；

A\B表示：B所指代对象是A所指代对象对外隐藏的操作；

A|B表示：在体系结构中，可能发生A所指代对象的行为或者B所指代对象的行为；

A＞＞B表示：A所指代对象与B所指代对象之间的交互行为保持平滑一致。

优选地，所述步骤3包括步骤：

利用Breeze图文法推导验证体系结构的完整性，包括：

假设，SA、SA’分别为重配置操作前、后的体系结构，ARM为体系结构参考模型， AddR^*、RemR^*、RepR^*分别表示可能需要执行多次的添加、删除、替换重配置操作；则 完整性验证条件为如下形式：

$f:\left(\mathrm{SA}\right|\left|\left({\mathrm{AddR}}^{*}\right|{\mathrm{RemR}}^{*}\left|{\mathrm{RepR}}^{*}\right)\right)\to \mathrm{ARM}\Rightarrow f:{\mathrm{SA}}^{\prime }\to \mathrm{ARM}$

若满足完整性保障验证条件，则完整性验证通过，否则不通过；

其中：

f:A→B表示：B所指代对象能够模拟实现A所指代对象的行为；

A||B表示：体系结构在运行过程中，A所指代对象和B所指代对象的交互行为是并 发的；

A|B表示：在体系结构中，可能发生A所指代对象的行为或者B所指代对象的行为；

表示：A所指代对象能够推演为B所指代对象。

与现有技术相比，本发明具有如下有益效果：

1、本发明在图文法的基础上结合Attributed图文法、Layered图文法和Reserved 图文法的部分思想，提出一种支持体系结构动态变化的图文法(简称为Breeze图文法 (Breeze Graph Grammars,BGG))，可对具有高分布性、高自治性、高可扩展性和动态 性的网络软件系进行建模，并准确刻画软件体系结构的静态结构和动态交互行为；本发 明利用图转换的思想，将体系结构的变化映射成对应的图重写规则，从而支持软件体系 结构的重配置规则定义，实现体系结构的动态演化，并保障了演化前后体系结构的一致 性和完整性。

2、通过采用本发明所提出的Breeze图文法方法，在实现对软件体系结构建模的同 时能够在软件开发初期和随后的演化过程中支持对动态变化的捕获，与其他体系结构图 技术相比，Breeze图文法建模的软件体系结构更加精准全面，可实现长生命周期的软件 体系结构动态演化。

3、本发明与传统方法的区别：传统的图文法方法常用于程序源代码一级，研究者采 用传统的图文法来抽象程序的语法结构，从而发现其中的语法错误。然后随着软件技术 的发展，现有的软件系统越来越庞大，规模也更加复杂，需要一种建模机制从高层抽象 软件系统的组成结构、连接方式以及系统结构配置及属性等要素。然而，传统的图文法 方法无法满足上述需求。

4、本发明解决的技术问题是：本发明通过对传统图文法中图的形式化定义进行扩展， 引入了接口、接口标签集、状态及附加属性，能够支持从高层抽象软件系统的组成结构、 连接方式以及系统结构配置及属性等相关要素，可以进行推导验证软件体系结构重配置 前后的一致性和完整性。

5、本发明获得的技术效果是：采用本发明所提出的Breeze图文法，可将软件系统的 组成结构，如构件和连接，可映射成为图中的节点和边，从而可以描述系统结构配置及 属性。Breeze图文法提供图重写规则，能够描述软件体系结构的动态重配置，从而更完 整地支持了软件体系结构的建模、分析和动态演化，应对开放的网络环境和变化的用户 需求对软件系统提出的挑战。

附图说明

通过阅读参照以下附图对非限制性实施例所作的详细描述，本发明的其它特征、目 的和优点将会变得更明显：

图1为图形化标注：Breeze图文法中的节点。

图2为综合医疗分析系统示意图。

图3为通用图形化标注：综合医疗分析系统。

图4为Breeze图形化标注：综合医疗分析系统。

图5为重配置中的添加操作。

图6为重配置：删除操作。

具体实施方式

下面结合具体实施例对本发明进行详细说明。以下实施例将有助于本领域的技术人 员进一步理解本发明，但不以任何形式限制本发明。应当指出的是，对本领域的普通技 术人员来说，在不脱离本发明构思的前提下，还可以做出若干变形和改进。这些都属于 本发明的保护范围。

本发明的目的是通过以下技术方案来实现的：

1、首先给出通用图文法的定义，在通用图文法中，通常图中一个节点用来表示一 个实体，图中的一条边代表图中节点间的一个连接通道或一种关系。

定义1，通用图形式化描述：

用G:＝(N,E,l_N,l_E,s,t)表示一个定义在给定的两个标签集(节点标签集L_N和边标签 集L_E)上的图G，且图G为一个六元组，符号:＝表示“定义为”，其中：

图G六元组中的N记为N(G)，N(G)是一个有限的节点集，代表在图G中所定义的节 点集；

图G六元组中的E记为E(G)，E(G)是一个有限的边集，代表在图G中所定义的边集；

图G六元组中的l_N记为l_N(G)，l_N(G):＝N→L_N是给定的节点标签函数，表示在图G中， 将通用节点集N与节点标签集L_N相关联；

图G六元组中的l_E记为l_E(G)，l_E(G):＝E→L_E是给定的边标签函数，表示在图G中， 将通用边集E与边标签集L_E相关联；

图G六元组中的s,t记为s(G),t(G)，s(G),t(G):＝E→N将图G中每条边与它对应的 源节点和目标节点相关联；

l(G):＝l_N(G)∪l_E(G)代表图G中所有节点标签函数和边标签函数。

符号→表示关联关系。

2、对通用图文法进行扩展，将其中的普通节点扩展为一个复合节点，即将接口作 为子节点引入到构件节点中。因此，一个构件或连接子则主要是由一个父节点(parent  node,pn)和子节点(children node,cn)构成的，pn是构件或连接子，而cn则代表接 口，从而引入了接口、接口标签集、状态及附加属性。

(1)定义2，Breeze图文法中图节点形式化描述：n:＝(pn,CN,l_CN,a_CN)是一个定义在 给定标签集l_CN上的具有属性的复合节点n(包括接口)，且复合节点n为一个四元组：

复合节点四元组中的pn是一个父节点，即构件或连接子的主体部分；

复合节点四元组中的CN是一个子节点集，即构件或连接子的接口；

复合节点n四元组中的l_CN记为l_CN(n)，l_CN(n):＝CN→L_CN是子节点n标记函数(即作 用在复合节点n上的标记函数)，表示将复合节点n上的子节点集CN与标签集L_CN相关 联，L_CN:＝{T_i'∈T'},i∈I(索引集)；I表示索引标号集，总共有I个复合节点，i表示 第i个复合节点；

复合节点n四元组中的a_CN记为a_CN(n)，a_CN(n):＝CN→A_CN是作用在子节点n上的接口 属性标签函数,表示将复合节点n上的子节点集CN与接口属性集A_CN相关联，A_CN是构件 或连接子的接口属性集。

其中，T_i'表示第i个复合节点的接口类型，T’:＝{I,O,I/O,X}表示接口类型集， I,O,I/O分别代表接口是服务请求者、服务提供者及服务请求/提供者，X是一个特殊的 接口类型，代表接口处于初始化期间，还未指派接口类型。图2给出了一个Breeze图 文法中节点图形化标注方式(状态S将在下面图的定义中给出)。

(2)定义3(Breeze图形式化描述)：G:＝(N,E,l_N,l_E,s,t，a_N)是一个定义在给定的 两个标签集l_N和l_E上的Breeze图G，且G为一个七元组：

Breeze图G七元组中的N记为N(G)，N(G)是一个有限的节点集；

Breeze图G七元组中的E记为E(G)，E(G)是一个有限的边集,E(G):＝{(n.CN_i,m.CN_j) ∈N.CN×N.CN},n,m∈N并且i,j∈I(索引集)；n表示复合节点n(包含接口)， m表示复合节点m(包含接口)，CN_i表示子节点i，CN_j表示子节点j，n.CN_i表示复合节 点n上的接口子节点CN_i，m.CN_j表示复合节点m上的接口子节点CN_j，N表示节点集，CN 表示接口子节点集，N.CN表示节点集中的接口集，i表示节点索引号，即第i个节点， j表示表示节点索引号，即第j个节点；

Breeze图G七元组中的a_N记为a_N(G)，a_N(G):＝N→A_N是节点属性标记函数，A_N表示构 件或连接子的属性集；

Breeze图G七元组中的l_N记为l_N(G)，l_N(G):＝N→L_N是给定的节点标签函数，表示在 图G中，将通用节点集N与节点标签集L_N相关联；Breeze图G中的L_N记为L_N(G)， L_N(G):＝{(T_i,S_j)∈T×S}，i,j∈I(索引)；T_i表示节点类型集T中的第i种节点类型， S_j表示节点状态集S中的第j个状态类型；

Breeze图G七元组中的l_E记为l_E(G)，l_E(G):＝E→L_E是给定的边标签函数；表示在图 G中，将通用边集E与边标签集L_E相关联；

Breeze图G七元组中的s,t记为s(G),t(G)，其中，s(G),t(G):＝E→N.CN将每条边 与它对应的源节点和和目标节点的接口相关联；

l(G):＝l_CN(n)∪l_N(G)∪l_E(G)代表图G中所有接口、节点和边的标签集。

其中，T:＝{component,connector,X}，S:＝{Waiting,Active,Temporary Failure, Fatal Failure}；component表示构件，connector表示连接子。T代表节点类型集，可 为构件或连接子，在节点初始化时，其类型为X。S表示节点状态集，构件或连接子的 状态说明如下：

●Waiting：构件或连接子创建后的初始状态；

●Active：构件或连接子正常工作状态；

●Temporary Failure：构件或连接子临时失效状态；

●Fatal Failure：构件或连接子致命失效状态。

3、定义Breeze图产生式规则。图文法中一个重要的特性就是图重写规则(Graph  rewriting rule)或产生式(production)。通常情况下，一条产生式由两个子图构成， 分别称为左手边(Left-Hand Side,LHS)和右手边(Right-Hand Side,RHS)。在Breeze 图文法中，体系结构的建模结果通过执行相应的产生式来实现体系结构的重配置。

定义4，Breeze图产生式形式化描述：Breeze图文法产生式P:＝(L,R)是由一个定 义在给定的节点和边的标签集和属性集上的两个图(L和R)构成，即LHS和RHS。LHS 与RHS可拥有一个公共的子图(Common Graph，CG)。公共子图CG需满足如下条件：

●表示任何一个属于CG节点也一定属于 LHS和RHS；

●表示任何一个属于CG的边也一定属于 LHS和RHS；

●表示公共子图CG的标签集是左手边和右手边标签 集的公共部分；

●表示公共子图CG的属性集是左手边和右 手边属性集的公共部分。

4、定义Breeze图文法，从而刻画软件体系结构模型。

定义5(Breeze图文法)：Breeze图文法是一个六元组(G，P，TL，NL，TA，NA）,其中G 是一个初始状态Breeze图，P是一系列可应用于G的产生式规则集，TL是终端标签集， NL是非终端标签集，TA终端属性集，NA是非终端属性集。对于即对 于产生式规则集P中的任意一个实例产生式规则p，可定义为一个二元组，包括左手边 规则(Left Hand Side，LHS)L和右手边规则(Right Hand Side,RHS)R，其中：

R是一个非空的连通图；

L和R都是基于相同的标签集L_G:＝TL∪NL和属性集A_G:＝TA∪NA；L_G表示图G上的所 有标签集(包括终端标签集和非终端标签集)，A_G表示图G上的所有属性集(包括终端 属性集和非终端属性集)。

5、定义Breeze图文法重配置操作，支持软件体系结构动态演化。软件体系结构作 为软件系统的高层抽象，需支持软件系统在的设计阶段粗粒度的重配置操作，如构件或 连接子的添加、删除、替换等操作，从而将软件系统的变化映射到软件体系结构层次。 根据体系结构重配置的特点，本发明关注重配置原子操作，包括构件的添加、构件的删 除、连接子的添加、连接子的删除。

(1)重配置添加构件/连接子

假定当前Breeze图为CS，需要引入新的类型为C的构件c，其通过接口Req发送 请求，同时引入连接子类型为CON的连接子con通过接口Res接收来自构件c的请求， 类型为S的构件s通过接口Res接收来自con接口Req发来的请求。

(2)删除构件和连接子

假定当前Breeze图为CS，需要删除与类型为S的构件s相连接的类型为C的构件 c，同时移除负责它们之间通讯的类型为CON的连接子con。

接下来对利用Breeze图文法推导验证软件体系结构的一致性和完整性进行说明。 通过顺序通讯进程CSP(Communication Sequential Process)对基于Breeze图文法模型 进行描述、推导，从而验证一致性和完整性。

(1)一致性

在体系结构重配置后，如果新的软件体系结构能模拟实现体系结构重配置前的行为 或至少与之前体系结构行为等同，则认为体系结构行为满足一致性条件。

定义设SA和SA’分别对应重配置前后的两个体系结构，并设ARM是体系结构参考 模型。若SA和SA’满足如下任何一个条件：

-(SA＝ARM)^(SA'＝ARM)，即：SA和SA'的体系结构参考模型都是ARM

-(f:SA→ARM)^(f:SA'→ARM)，即：ARM能够模拟实现SA和SA’的行为

则认为SA’可以模拟实现SA的行为，可写为f:SA→SA'。

定义设SA和SA’分别对应重配置前后的两个体系结构，若SA’至少能模拟实现 SA的行为，则认为SA’与SA的行为一致，并可写为

若新的体系结构与旧的体系结构时一致的，则组成它们的构件和连接子也应当是一 致的。

根据图文法定义，采用顺序通讯进程CSP进行抽象描述，设有两个构件分别是Com_i和Com_j，一个连接子Conn_k，则Com_i、Com_j、Conn_k三者之间的交互行为可写成 (Com_i||Conn_k||Com_j)。Com_i、Com_j和Conn_k是一致的，当且仅当它们满足如下的条 件：

f:(Com_i||Conn_k||Com_j)→(Com_i\C||Conn_k\T||Com_j\S)，即：若将构件或连接子 内部的行为隐藏，则其对外表现的行为不会影响系统的行为或违反系统约束

$\left({\mathrm{Com}}_i\right|\left|{\mathrm{Conn}}_k\right|\left|{\mathrm{Com}}_j\right)\Rightarrow ({\mathrm{Com}}_i>>{\mathrm{Com}}_j)$

其中，C、T和S分别表示构件Com_i、连接子Conn_k和构件Com_j内部的行为，“\” 表示隐藏操作，Com_i＞＞Com_j表示构件Com_i和构件Com_j是平滑连接，连接子Conn_k的 行为与构件的相兼容。

假设，通过重配置添加操作给体系结构SA增加了一个新的构件Com_s，并通过连接 子Conn_z与系统交互，则一致性保障验证条件可写成如下形式：

验证条件：满足

其中，“Com_s\K”和“Conn_z\T”表示“K”和“T”是一系列构件Com_s和连接子 Conn_z对外隐藏的操作，系统外部无法观察到。

其中：

表示：A所指代对象与B所指代对象的行为一致；

A||B表示：体系结构在运行过程中，A所指代对象和B所指代对象的交互行为是并 发的；

A\B表示：B所指代对象是A所指代对象对外隐藏的操作。

而针对替换构件/连接子的重配置操作，一致性验证条件可写成如下形式：

验证条件：满足

其中，“Com_s\C”表示“C”是一系列内部操作，被构件Com_s隐藏且不能被外部系 统所观测到，即在体系结构重配置后，Com_s只暴露它的公共行为给SA。Com_s＞＞Com_k代表经过替换连接子Conn_j后，构件Com_s和构件Com_k通过新的连接子Conn_z连接后， 交互行为仍保持平滑一致；构件Com_i是被构件Com_s替换的构件，连接子Conn_j是被连 接子Conn_z替换的连接子。

其中：

f:A→B表示：B所指代对象能够模拟实现A所指代对象的行为；

A||B表示：体系结构在运行过程中，A所指代对象和B所指代对象的交互行为是并 发的；

表示：非；

A||B表示：将A所指代对象替换为B所指代对象；

A\B表示：B所指代对象是A所指代对象对外隐藏的操作；

A|B表示：在体系结构中，发生A所指代对象的行为或者B所指代对象的行为；

A＞＞B表示：A所指代对象与B所指代对象之间的交互行为保持平滑一致。

(2)完整性

上述的分析和验证保证了体系结构重配置后的一致性，此外，另一个需要保证的属 性就是完整性，即系统重配置不会违反系统约束或需求。

设SA和SA’分别对应重配置前后的两个体系结构。若SA的重配置操作满足系统约 束，并且在执行重配置操作后，SA’能模拟体系结构参考模型ARM的行为，则称新的系 统满足于完整性约束，可写为SA'satTr(Integrity)。

其中，Tr(Integrity)表示完整性需求。完整性验证条件可写成如下形式：

验证条件：$f:\left(\mathrm{SA}\right|\left|\left({\mathrm{AddR}}^{*}\right|{\mathrm{RemR}}^{*}\left|{\mathrm{RepR}}^{*}\right)\right)\to \mathrm{ARM}\Rightarrow f:{\mathrm{SA}}^{\prime }\to \mathrm{ARM}$

其中，AddR^*、RemR^*、RepR^*表示可能需要执行多次的添加、删除、替换重配置操 作，根据条件要求，重配置操作需要满足系统约束。

其中：

f:A→B表示：B所指代对象能够模拟实现A所指代对象的行为；

A||B表示：体系结构在运行过程中，A所指代对象和B所指代对象的交互行为是并 发的；

A|B表示：在体系结构中，可能发生A所指代对象的行为或者B所指代对象的行为；

表示：A所指代对象能够推演为B所指代对象；

以综合医疗分析系统为例，则需要满足客户/服务器风格约束CS，则AddR^*sat CS、 RemR^*sat CS和RepR^*sat CS，A sat B表示：A所指代对象的规约满足B所指代对 象的规约。因此可得如下另一个验证条件：

验证条件：