《软件架构理论与实践》 —3.3　软件架构的形式化建模方法

3.3　软件架构的形式化建模方法

软件架构建模通常采用非形式化方法，然而这种非形式化方法并不能很好地描述不同系统组成部分之间的一些特性，已经难以适应软件架构建模的进一步发展。同时形式化方法作为一种严格以数学为基础的方法，能够清晰、精确、抽象、简明地规范和验证软件系统及其性质，帮助发现其他方法不容易发现的系统描述的不一致、不明确或不完整，有助于增强软件开发人员对系统的理解。总之，形式化的建模方法能够极大地提高软件的非功能属性。

目前，在软件架构建模中，包含基于形式化规格说明语言的建模和基于UML形式化的建模两种软件架构形式化建模方法[47]。

1）基于形式化规格说明语言的建模：其基本思想是利用一些已知特性的数学抽象来为目标软件系统的状态特征和行为特征构造模型，如Z语言、B语言、VDM、Petri网等都是面向模型的方法。或者，它为目标软件系统的规格说明提供了一些特殊的机制，包括描述抽象概念并进行进程间连接和推理的方法，如CSP、CCS、CLEAR等都是代数方法。

2）基于UML形式化的建模：其基本思想是利用形式化与UML结合的建模方法研究成果，对UML图形赋予形式化语义，然后就可以利用已有的形式化语言和工具对UML模型进行推理验证。我们可以将UML相关图形转换成Z语言、B语言、XYZ/E、Petri网等不同的形式化语言，这提高了UML的准确性，为精确建模奠定了良好的基础。

3.3.1　基于形式化规格说明语言的建模方法

软件开发中的形式化建模方法主要是使用形式化规格说明语言来展示系统的架构，解析系统的特性。目前广泛应用的一些形式化描述方法有Z语言、Petri网、B语言、VDM、CSP等，这些形式化方法在功能上各有侧重，可以互补。

1. Z语言

Z语言是迄今为止应用最为广泛的形式化语言之一，软件企业在软件特别是大型软件的开发中经常采用Z语言进行需求分析、软件架构建模。Z语言是由英国牛津大学程序研究组（PRG）的Jean Raymond Abrial、Bernard Sufrin等人设计的一种基于一阶谓词逻辑和集合论的形式化规格说明语言，它采用了严格的数学理论，将函数、映射、关系等数学方法用于规格说明，具有精确、简洁、无二义性且可证明等优点。Z语言是一种功能很强的形式化规格说明语言，可以保证其书写的规格说明文档的正确性，同时还能保证有很好的可读性和可理解性。Z语言借助于模式（schema）来表达系统结构。模式有水平和垂直两种形式。一个模式由变量声明和谓词约束两部分组成，可用来描述系统的状态和操作，即“模式=声明+谓词”。声明部分引入变量，谓词部分表示了关于变量值的要求。

Z语言规范一般由四个部分组成：给定的集合、数据类型和常数；状态定义；初始状态；操作。在实际应用中，Z语言的一个规范（即语言文档）由形式化的数学描述和非形式化的文字解释或说明组成。形式化的数学描述由段落构成，这些段落按顺序给出各种构造类型描述、全局变量定义以及基本类型描述。具体描述时，一个段落可以给出一个或多个构造类型描述。根据段落的含义不同，段落的种类有基本类型、公理、约束条件、构造类型、缩写、通用构造类型、通用常量和自由类型。

Z语言作为一种广泛应用的形式化规格说明语言，在软件架构建模方面也得到了广泛关注。通过使用Z语言对软件架构进行形式化建模，软件开发者可以得到精确、严谨的架构描述。文献[48]中运用Z语言给出了管道–过滤器结构详尽的形式化描述的实例。该结构包括过程抽象和操作抽象。其中，过程抽象包括管道模式、过滤器模式、管线模式，用于描述管道–过滤器这一软件架构风格的静态性质；而操作抽象包括管道操作模式、过滤器操作模式、管线操作模式，详细地描述了管道–过滤器的动态行为。文献[49]以Z语言的形式化描述为基础，使用数据抽象和过程抽象，利用关系、函数、集合、序列、包等将数据从数据结构的表示细节中抽象出来，通过组件、连接件的添加及删除来实现准确描述软件架构的建模过程。

2. Petri网

Petri网是一种系统的数学和图形的建模和分析工具，适用于对具有并发、同步、冲突等特点的系统进行模拟和分析，并被广泛应用于复杂系统的设计与分析中[50]。 Petri网是用于表述分布式系统的众多数学方法之一，作为一种建模语言，它采用图形化方法将一个分布式系统结构表述为带标签的有向双边图。

Petri网的元素包括库所（place）、变迁（transition）、有向弧（arc）和令牌（token），其中有向弧存在于库所和变迁之间，令牌是库所中的动态对象，可以从一个库所移动到另一个库所。Petri网的规则是：有向弧是有方向的，两个库所或变迁之间不允许有弧，库所可以拥有任意数量的令牌[51]。

在软件架构领域，为了应对软件动态演化面临的挑战，应提高所建立的软件架构的动态演化性。利用Petri网及其扩展，对面向动态演化的软件架构进行建模能够有效提高所建立软件架构模型的动态演化性。因此，关于利用Petri网对软件架构建模的研究主要集中在描述软件架构的动态演化性方面。

经典的软件架构的Petri网描述是一个四元组，其形式化定义为L=（Cm，Ce，Rr，Ca），其中Cm为软件架构中的组件，Ce为软件架构中的连接件，Rr为软件架构中的角色，Ca为软件架构中的约束。Petri网形象地描述了软件架构的动态语义，通过变迁的发射Token从一个库所分配到另外一个库所，表明了资源或消息的传递，较好地说明了整个软件系统的流程。Petri网还可以用形式化的分析方法对软件系统的死锁和活性进行动态分析和验证，以进行早期的预防和检测，避免建模时的人为错误，同时可以利用相应的Petri网支持工具对软件架构模型进行模拟。

文献[52]提出了一种基于Petri网的软件架构—PSA（Petri-Software-Architecture）。PSA着眼于有关系统架构全局特性方面的问题，利用Petri网对系统元素间输入/输出以及系统静态、动态特性的描述能力，使用Petri网的可达标识图给出了一种计算组件贡献大小的方法，同时还给出了架构演化中组件删除、增加、修改以及合并与分解等各种变化引起的波及效应分析。通过系统 PSA的可达标识图（RMG）可以很容易界定某一组件变化所影响的其他组件，即组件对 SA 影响的大小（称为贡献或者贡献大小），比传统方法[53]中通过系统可达矩阵计算更加直观，而且组件变化后不一定需要每次重新计算，而可达矩阵方法需要在每次更新系统后重新计算其可达矩阵。

运用基于 PSA模型的可达标识图来分析软件架构性能，一方面能给系统架构师提供系统信息参考，如组件贡献大小可以帮助合适地改变系统架构，同时也可适当地更改原有系统可达标识图并快速分析变更后新系统的特性；另一方面，首次用 Petri 技术分析系统架构性能为软件架构研究提供了一个全新的思路。进一步的工作是利用 Petri 网辅助完成软件架构其他方面的设计，如辅助完成系统运行时的故障诊断与自校正设计。

文献[54]设计了一种面向动态演化的软件架构元模型，其选取Petri网作为软件架构建模的主形式化工具，使得模型在具有直观图形表示的同时，又具有精确且严格的语义。该软件架构元模型包括静态和动态两个视图。静态视图表达软件架构的静态结构，动态视图以静态视图为基础，反映系统行为导致的软件架构状态变化。其中，静态视图以Petri网的网结构表示，动态视图以网系统表示，组件之间的交互就相应地以Petri之间的交互和融合展示出来，软件系统的动态行为以Petri网中变迁点火引起的网系统的动态运行来展示。通过变迁的分类来映射稳定和易变需求，通过库所的分类来映射主动和被动需求，通过区分端口和接口来映射计算和交互的相对隔离等机制，在软件架构建模中继承和保持需求建模对动态演化的支持机制。

3. B语言

B方法用一种简单的伪程序语言来描述需求模型、规格说明，并进行中间设计和实现，这个语言就是B语言[55]。B语言支持规格说明的类型检测、动态验证、数学证明等以确保设计过程的正确性，同时分层次开发以降低大型软件开发的复杂性。分层次的方法可以将高层实现表示成低层的规范，一个完整的开发就是逐步实施的规范/实现过程。规范/实现过程在最低级的实现可以从预先实现的可重用的组件库中得到，高级的重用也可通过不断扩展新的组件库从而支持整个开发过程，每一层的实现过程是将规范翻译成可维护的独立编译的源代码和可执行指令的过程。同其他面向对象方法一样，B语言中的结构化机制增强了信息隐藏和数据封装特性，确保了大型开发中各个组件的独立开发。

B语言使用简单熟悉的符号表示法[56]。这种符号表示法用广义替换表示状态转换，从规格说明到编码，这种统一的形式减少了学习的难度和转换中的语法错误，这种“数学程序设计语言”可使人们使用一种非常具体的规格说明形式，而且对软件工程师来说也是极为有益的。B语言采用模块化构造，从规格说明到实现的模块化构造允许将规格说明和验证过程分解为多个子任务进行，相比其他类似的规格说明语言这个优点是非常突出的，而且比ADA和C++中的结构化构造更容易学习。B语言有大量实用的工具支持，它们支持了B方法中软件开发周期的所有阶段，甚至包括动画制作和文档生成等，其他形式化方法似乎还没有如此强大的类似集成工具。

作为一种较新的、基于模型范畴的形式化方法，B语言将程序和程序规格说明严格处于统一的数学框架下，采用基于Zermelo-Frankel集合论的符号表示法书写。B语言包含一种结构化机制（从需求规格说明到精化再到实现），以一种伪码语言即抽象机符号表示法（Abstract Machine Notation，AMN）构造需求模型并设计和实现，由于AMN支持规范说明的类型检测、动态验证，所以确保了设计过程的正确性。B语言在软件架构建模领域应用较多，文献[57]通过分析UML和B语言的优缺点，将二者结合，对UML模型图使用B语言进行形式化，定义映射规则，并使用B工具Atelier-B对所建模型进行自动检查与验证。文献[58]通过将UML转换为B AMN，利用Linux下的B语言工具集如BToolKit进行细化、实现及验证。

4. VDM

VDM是在1969年开发PL/1语言时由IBM公司维也纳实验室的研究小组提出的。VDM是一种功能构造性规格说明技术，它通过一阶谓词逻辑和已建立的抽象数据类型来描述每个运算或函数的功能。20世纪90年代初这种方法在欧美许多研究机构或大学得到了广泛的应用[59]。

VDM技术的基本思想是运用抽象数据类型、数学概念和符号来规定运算或函数的功能，而且这种规定的过程是结构化的，其目的是在系统实现之前简短而明确地指出软件系统要完成的功能。由于这种形式化规格说明中采用了数学符号和抽象数据类型，所以可使软件系统的功能描述在抽象级上进行，完全摆脱了实现细节，这样为软件实现者提供了很大的灵活性。此外，这种形式化规格说明还为程序正确性证明提供了依据。应用VDM技术进行系统开发包含了形式化规格说明、程序实现和程序正确性证明三个部分。

使用VDM定义形式化规格说明具有以下三个明显的优点：①只告诉计算机做什么；

②提供了程序正确性证明的依据；③使规格说明描述简练、精确。此外，使用VDM还可以使程序设计者牢固树立先抽象后具体的不断证明其正确性的逐步分解、自顶向下的开发思想，从而在整个程序开发的过程中用系统而严密的方法来保证所开发程序的正确性。文献[60]在VDM的基础上，使用其工具语言Meta-Ⅳ，通过抽象软件系统的语法域、语义域及语义函数来形式化表示软件架构的建模过程。文献[60]利用VDM的扩展语言—面向对象的VDM++，在RUP的分析和设计工作中将UML视图转换为相应的VDM++形式化规格说明，以规范软件架构的建模过程。同时通过VDM++形式化规格说明的每次静态检测与模拟执行，确定本次开发周期中所建模的规格说明满足评价标准的程度，以及在下一次开发周期中可做的改进，通过如此不断迭代的过程使得软件规范逐渐满足评价标准。

5. CSP

CSP即基于进程代数的描述语言，它以进程和进程之间关系的描述为基础，用来描述一个复杂并发系统的动态交互行为特性。CSP进程通过事件的有序序列来定义。在事件中，一个进程与它的环境相交互。一个进程的所有事件集合构成该进程的字母表。例如αP表示进程P的事件集合，即字母表。事件一般用小写字母表示，进程用大写字母表示。对字母表中的不同事件，进程将做出不同的动作，例如x:A→P(x)表示进程P的字母表A中的事件x发生后，进程P以x事件为初始事件继续进行。进程到某一时刻为止所处理的事件序列定义为进程的迹（trace）。针对复杂进程的描述，CSP允许进程的嵌套，一个大的进程可以由许多小的进程组成。CSP进程之间发送消息交互，进程之间的关系（即进程的组合方式）通过一些运算定义，如顺序、并发、选择、分支以及其他非确定性的交织等。另外，CSP定义了两个原语进程—Skip（正常终止）和Stop（死锁），用来终止一个进程。

CSP使用的符号子集包括以下元素[61]：进程和事件，进程描述了交互事件中的一个实体，事件可以是原子的，也可以包含数据，最简单的进程Stop表示没有事件；前缀，如果有e→P，则e为P的前缀；替代（alternative），即确定性选择，一个进程可以表现为P或Q，由它自己决定，表示为PΠQ；决定（decision），非确定性选择，一个进程可以表现为P或Q，且由它所处的环境（与其他过程的交互）决定，表示为P[]Q；命名进程（named process），进程名称可以与进程的表达式相关联。

CSP以事件为核心，通过事件集合实现进程及其关系的描述，并且通过失效/偏差模型对进程行为进行判别。失效由迹和拒绝集成对定义，拒绝集也是一个事件集合，它给出进程在指定迹上面可以拒绝的事件集合。偏差用于描述无法预测的环境。CSP的主要优点在于CSP规范的可执行特性，因此可以检查内在的一致性。此外，CSP还支持从规范验证到设计和实现的一致性，即如果规范是正确的，并且转换也是正确的，那么设计和实现也是正确的。CSP不仅可以用于建立刻画系统行为的模型，还可以用于建立推理的形式演算模型，研究者们发现CSP能够很好地描述软件架构模型的各种语义属性。文献[62]在CSP理论的基础上，对软件架构的形式语义和代数语义进行了分析，并对软件架构的元模型进行了描述，将元模型的每一层都描述为一个进程，然后利用CSP严密的语义特性表达能力和演算推理分析能力对整个模型进行良好的语义描述分析和检测。