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

3.3.2　基于UML的形式化建模方法

由于软件架构建模的本质在于预先给出待建系统的模型并分析其各种行为和特征，因此如何精确地描述模型显然是非常重要的。尽管UML可以用于描述软件架构，对各种软件系统或离散型系统进行建模，并且通过相应支持工具的配合可进行架构的文档化和部分目标语言代码的生成，然而UML不是一种形式化的语言，不能精确地描述系统的运行语义。因此，非形式化描述方法不能支持在软件架构的抽象模型层面进行相关分析和测试，需要进一步采用形式化建模方法及其支持语言和工具。

形式化方法和UML存在很大的互补性，二者的结合研究对提高软件架构的建模质量有着非常重要的意义。形式化与UML结合的建模过程和UML统一建模过程有明显的不同，它的目标是直接构造出尽可能正确的系统。图3-2是形式化与UML结合的开发过程图。因为形式化与UML结合的建模过程和UML统一建模过程的目标不同，所以它们的开发模式也不一样。形式化与UML结合的建模过程的需求分析和设计阶段需要投入大量工作量，通常占到全部工作量的60%～70%，编码和测试工作则只占30%～40%。而UML统一建模过程的编码和测试所需工作量非常大，一般要占到60%～70%[63]。从这里可以看出形式化与UML结合的建模过程在需求分析和设计阶段所投入的工作量要远远大于UML统一建模过程，这主要是因为其在设计阶段使用了形式化描述与验证，保证了软件架构设计的一致性和可靠性，从而使得后期的编码和测试工作变得相对简单。

下面我们来看看如何将形式化方法与UML结合在一起，其中使用的形式化方法以Z语言为例，而UML中以常用的类图、用例图、状态图和顺序图为例。

图3-2　形式化与UML结合的建模过程

1. UML类图的形式化

UML类图是由类、泛化和关联组成的。类包括属性和操作，其中操作包含一组有序的参数。泛化表示了子类和超类的关系。关联一般有两个关联端，每个关联端具有若干属性。UML类图的形式化可以转化为对类、关联、泛化的形式化描述[64]。

（1）类的形式化

在UML中，类是一组具有公共特性的对象的抽象。类有名称、属性和操作。其中，属性有名称、可见性、类型和多重性；操作有名称、可见性和参数，操作的每个参数有名称和类型。在定义图形元素之前，先定义几个集合：Name、Type和Expression。用Z语言表示为[Name, Type, Expression]。在属性中多重性表示属性数据取值的可能数目。在UML中可见性可以是私有的、公共的和保护的。如图3-3所示为类的属性和参数的形式化表示。

VisibilityKind::=private丨public丨protected

图3-3　类的属性和参数的形式化表示

操作中的参数是一个序列，而且参数名必须唯一。如图3-4所示。

图3-4　类的操作的形式化表示

在类中定义的属性名应该不同，并且操作应该带有不同的参数。如图3-5所示。

图3-5　类的形式化表示

（2）关联的形式化

在UML中，类之间的关系用关联来表示。在大多数情况下，类图中两个类之间的关联是二元的，而且聚集和组合总是二元关联。因此，我们只考虑二元关联。二元关联有一个关联名和两个关联端。每个关联端有一个角色名和一个多重性约束、一个描述导航性的属性和一个描述关系类型（聚集、组合）的属性。多重性约束描述的非负整数的范围表示该位置上可以有多少个对象，并且限制了一端的一个对象可以与另一端的多少个对象有关联。谓词部分的约束表示多重性不能为0，对组合而言，组合端的多重性至多为1。如图3-6所示为关联端的形式化表示。

AggregationKind::=none丨aggregate丨composite

二元关联有一个名称并且恰好有两个关联端。谓词部分的属性表示了关联的特性：每个角色名必须不同。对聚集和组合关联来说，应该只有一个聚集或组合端并且另一端是部分或者聚集值为none。假定e1是聚集或组合端，则关联的另一端的聚集值为none，并且属性名和角色名不重叠。如图3-7所示。

      图3-6　关联端的形式化表示     图3-7　关联的形式化表示

（3）泛化的形式化

在UML中，泛化描述了对象之间的分类关系，其中超类对象描述了通用的信息，子类对象描述了特定的信息。如图3-8所示约束表达式表示不允许循环继承。

（4）类图的形式化

UML类图是由类、关联和泛化组成的。约束表达式表示在类图中，类的名称是唯一的，并且关联和泛化涉及的类应该在同一个类图中。如图3-9所示。

      图3-8　泛化的形式化表示  图3-9　类图的形式化表示

2. UML用例图的形式化

用例图由角色、用例和系统三个部分组成，所以对用例图的形式化工作可转化为对这三种元素的形式化描述[64]。

（1）角色的形式化描述

角色是与系统交互的外部实体（人或事），代表的是一类能使用某个功能的人或事，所以它的形式化描述比较简单。假设类A和类B使用系统的功能时具有角色C，则角色C可以表示成“Actor C==AVB”。

（2）用例的形式化描述

利用Z语言可以将用例形式化为如图3-10所示格式。

其中，Use Case Name是模式名，Declarations是声明部分，Predicates是谓词不变式部分。对用例模式而言，声明部分是状态变量和输入/输出声明，谓词不变式是执行用例的功能时应满足的条件和执行用例的功能后引起的变化。用例模式的谓词不变式可以表示如下：

Predicates = Pre-Pred ∩ Post-Pred

不变式中的“∩”表示“并且”的关系，意思是Predicates由Pre-Pred和Post-Pred两部分组成。Pre-Pred表示执行用例的功能前状态变量和输入应满足的条件，即用例的前置条件；Post-Pred表示执行用例的功能后状态变量和输出应满足的条件，即用例的后置条件。

1）独立用例的形式化描述：这里的独立用例是指该用例与其他用例之间不存在use或extend关系。前面所介绍的用例模式可以用来表示独立用例的形式化，为了更清晰地描述用例模式的前置条件和后置条件，将其用例模式的谓词不变式部分分成两部分表示，表示方法如图3-11所示。

2）有关系的用例的形式化描述：这里有关系的用例指的是与其他用例之间存在扩展或使用关系的用例的形式化。图3-12是扩展关系和使用关系的用例图。由于在这两种关系的用例中，Use Case A均继承了Use Case B中的一些行为，因此把Use Case B看作父用例，Use Case A看作子用例。形式化描述具有扩展和使用关系的用例时，对于父用例（即Use Case B）将按照独立用例的形式化方法进行描述；而对于子用例（也就是Use Case A），则将其描述成包含父用例的模式，如图3-13所示。

      图3-12　具有扩展关系和使用关系的用例图       图3-13　有关系的用例图的形式化表示

相对于独立用例的形式化，具有扩展和使用关系的用例（子用例）的描述只需要在Declarations部分增加其所继承的用例的声明即可。

（3）系统的形式化描述

系统是用例图的另一个组成部分，它的形式化描述同样可以按照图3-13的格式给出，只不过将Use Case Name用System Name代替，如图3-14所示，图中System Name是系统的名称，Declarations是系统所提供的功能（即用例）的声明，Predicates是对用例的约束，主要用来表示各个用例之间的关系。

（4）用例图的形式化描述

用例图是由角色、用例和系统组成的，所以只要将角色、用例和系统的形式化描述组织起来，就可得到用例图的形式化描述。用例图的形式化描述如图3-15所示。图中，Declarations部分是角色、用例和系统的说明，Predicates部分用于表示角色和用例之间的关系，也就是说用来表示某个角色与哪些用例之间有关系，即使用了用例的功能。

3. UML状态图的形式化

UML状态图由状态和迁移组成，对应地，在形式化过程中我们分别定义了迁移模式和状态模式，状态模式之间的层次化结构机制用Z语言的模式运算来表示[65]。

（1）迁移模式

迁移模式表征一个迁移所引起的状态变化，关联迁移前的变量值与迁移后的变量值。迁移具有触发事件、迁移条件、动作、源状态和目标状态，在定义Z语言的模式之前，先定义几个集合：事件集EE、迁移条件集CE、动作集AE。

EE::={Request_Event, Transform_Event, Signal_Event, Time_Event}

CE::={Boolean_Expression}

AE::={Assignment,Call,Create,Destory,Rerurn,Send,Terminate,Uninterpreted}

EE中的事件是具有时间和空间位置的显著发生的某件事。事件带有参数，参数可用于迁移中的动作。事件可以划分为请求事件（Request_Event）、变更事件（Transform_Event）、信号事件（Signal_Event）和时间事件（Time_Event）[66]，如表3-2所示。

表3-2　事件的种类和对应描述

EE中的迁移条件是布尔条件表达式，它可能引用附属于该状态的对象的属性以及触发事件的参数。迁移条件在触发事件发生时被求值，如果表达式为真，则迁移被激发。AE中的动作在迁移被激发时执行，动作通常是赋值语句或单个的计算，还包括调用操作、设置返回值、创建和销毁对象以及其他指定的控制动作。迁移模式定义如图3-16所示，其中Name是标识符集合，name指迁移名，Source_state指迁移模式连接的源状态模式，TriggerEE指触发事件集，Object_state指迁移的目标状态模式。

（2）状态模式

状态模式包含变量声明和使用声明变量的谓词集，其动态属性由迁移模式描述，静态属性则由状态模式和操作模式来描述，定义如图3-17所示。

（3）层次化结构机制表示

为了支持大中型软件开发，Z语言引入了层次化结构机制，允许用成组框将相关的图元结合在一起，成组框可以嵌套，从而支持对目标软件系统功能的逐级分解。下面我们利用Z语言的模式运算来定义组合状态的状态模式，从而表示层次化结构机制。

图3-17　操作模式以及状态模式的形式化表示

状态模式之间的OR、AND、SAND三种关系可以分别使用操作符“‖”“&”“#”来定义，其语法为：Schema-Exp::=Schema-Exp op Schema-Exp（其中op为‖、&或#）。

这三个操作符都是二元操作符，操作数为模式表达式。模式运算定义为合并子模式的变量声明和断言以形成一个新的模式。对于‖和&操作符，两个模式必须类型兼容，#操作符用于描述顺序系统，要求两个模式共享的输入、输出变量的类型一致，它的操作效果是对于所有共享变量，第一个模式的输出值将作为第二个模式的输入值。在定义了迁移模式和基本状态模式S2、S3、S4、S5、S7、S8后，图3-18中的UML状态机示例可用模式运算表示为：

sub1::=S2#S3　sub2::=S4#S5　S6::=S7#S8　S1::=sub1&sub2

S::=S1||S6

图3-18　UML状态机示例

另外S2、S3、S4、S5、S7、S8也可以是引用子状态机状态或者占位状态，可以在逐步求精中不断细化，外层的状态细化成多个内部状态，每个子状态继承父状态的迁移。

4. UML顺序图的形式化

UML顺序图用于描述对象间动态的交互关系，着重体现对象间消息传递的时间顺

序[67–68]。顺序图采用两个轴：水平轴表示不同的实例（其实是角色，每个角色代表一个特定的对象或一组对象的集合，以下称之为实例），垂直轴表示时间。两个实例生命线间带有箭头的线表示消息，消息的箭头形状表明了消息的类型是发送还是返回。消息按发生的时间顺序从上到下排列，每个消息旁边标有消息名，也可加上参数。图3-19 给出了顺序图的一个具体实例。

图3-19　用户成功登录到服务器的UML顺序图

（1）实例的形式化描述

顺序图具有一定的抽象句法，也必须满足一些合式规则。这里使用Z 语言严格地对它们进行描述，规格说明使用了以下给定的类型：[INSTANCE, TYPE, NAME] ，其中INSTANCE、TYPE、NAME分别是所有实例、类型和名称的集合。

在顺序图中实例的生命线上发送或接收消息的点称为位置点，每个实例的生命线上存在着有限个离散的位置点。如图3-20所示的全程变量

l _max，表示系统所允许的最大位置点。实例生命线上的位置点用模式ILocation 描述，其中任意一个位置点均不大于l_max。

（2）消息的形式化描述

在每个位置点上可以有一个或多个消息发送给其他实例，或者接收从自身或其他实例发送过来的一个消息。每个消息上标记有消息的名称和对应的参数，其中消息的参数类型应与系统模型中类图给出的操作说明一致。为了区分相同发送实例和接收实例间激活相同操作的两个消息，每个消息还附带一个唯一的标识号。消息标识用模式MsgId描述，其中任意两个消息的标识号均不相同。如图3-21所示。

顺序图中可以使用返回标记，它表示从消息处理中返回，而不是一个新消息，所以返回标记与原来的消息具有相同的消息标识。通常情况下它带有一个返回值，其类型也与类图中的说明相一致。返回标记可以由模式ReturnId定义，如图3-22所示。

用S 和R 分别表示消息的发送和接收，则消息的发送接收标志MSRFlag 定义为：

MSRFlag ::= S丨R

顺序图中的每个消息与实例生命线上的两点相关，即发送消息的位置点和接收消息的位置点，可以用模式Message描述。如图3-23所示。

另外，用映射msg来描述顺序图中位置与消息之间的对应关系，定义函数source、target来描述消息与发送或接收该消息的实例之间的对应关系：

/msg：ILocation        F Message

source,target: Message → F1 INSTANCE

顺序图可用模式WFSequenceDiagram描述，其中至少有一个实例和一个消息，并且对于任意的消息，其发送位置点与接收位置点应不同。如图3-24所示。

图3-24　WFSequenceDiagram的形式化描述

UML与Z结合的建模过程是在目前软件规模和复杂性不断增大的情况下提出的，它对现在工业界软件架构建模过程做了一些改进，并提出了一些新的思路和构想。不只是Z语言，其他形式化方法也可以将非形式化的UML图形转换为具有精确语义的形式化规格说明，在非形式化的图形表示与形式化定义之间建立映射关系。UML中的类图、用例图、状态图以及顺序图较适合形式化描述，用形式化描述方法其他图反而使得描述过程更加复杂，容易降低效率。