摘要
本文从初始需求开始构建聊天室模型，以及对个案进行研究。在不同的开发阶段，分别要用到UML类图、时序图和状态图。这样，难免需要确定一致性问题，现在已经提出了许多仿真和方法，用来确保模型各个方面的一致性。我们关注内部一致性，即给定模型内部制品之间的一致性问题。
1 简介
软件系统的开发过程通常会被划分成一些步骤，每个步骤会用到不同的UML图。由于建模系统变得越来越复杂，一致性问题就越发突出起来。而在其中，有两种类型或问题更为显著。第一，内部一致性问题，涉及给定模型内部制品之间的一致性。第二，系统之间一致性问题，涉及软件开发过程中不同演化模型之间的一致性。我们主要关注于内部一致性问题。
不同的文献提出了不同的形式化方法，用来自动检查一致性，发现设计当中存在的问题。在下面几节里，我们分步研究了一个聊天室的开发过程。本文的灵感来源于Agder大学Geir Melby完成的一次项目报告（http://fag.grm.hia.no/ikt2340/year2002/）。这个模型提出了一些潜在的一致性问题。对于它们当中的部分内容，也给出了自动化的一致性检查方法。
在这份案例研究中，我们从需求开始开发了一个聊天室模型。第二节给出了客户、治理器对象以及聊天室之间的通信协议，作为初始需求。第三节研究了一个可能的类的设计，它定义了符合协议的接口。第四节中给出的时序图进一步定义和描述了组件之间的通信，并保持与类设计之间的一致性。第五节使用状态图更进一步地确定应用程序的行为。这份规程可以在我们的SVM（状态图虚拟机）环境中实时地进行仿真或执行。在第六节中，讨论了协议规程与仿真迹的一致性。第七节进行总结。
2 通信协议
我们将要创建的聊天室程序是按照客户机/服务器范型来架构的。客户会随机连接聊天室。假如某个聊天室接收了客户，客户就会发送消息给这个聊天室。然后聊天室广播每条消息，除了发送者以外，每个与聊天室建立连接的客户都会收到一份拷贝。
下面将要描述一个特定的简化了的用例：
X系统包括五个客户和两个聊天室。客户端最初没有连接。每隔一到三秒（非均匀分布），它们都会随机连接一个聊天室。被请求的聊天室同时收到请求（假定没有网络延时，并且通信可靠）。
X一个聊天室至多接收三个客户。当且仅当容量没有超标时聊天室才会接收连接。
X 发出请求的客户会马上收到接收或拒绝通知。
X在客户可以发送聊天信息之前必须被一个聊天室接收。
X连接建立之后，客户会每隔一到五秒（非均匀分布）给它所连接的聊天室发送随机消息。聊天室会立即接收消息，它将耗时一秒钟来处理接收到的消息，并把它广播给除发送者之外的所有连接客户。
X客户会同时收到广播。为了简化起见，我们不讨论没有连接的情况。
3 类的设计
根据上面的规定，显然我们需要两个类：Client和ChatRoom。在开发过程早期阶段，对于仿真来说无需用户干预，我们明确地按照随机过程对用户行为（连接请求和聊天信息）进行建模。以后，客户模型将会被与软件打交道的真实客户所代替。仿真开始时，会初始化五个Client实例和两个ChatRoom实例。
我们还加入了一个singleton类：Manager。Manager以仲裁者的身份中继组件之间的所有通信。这种中心控制措施将会帮助截取系统传递的所有消息，使用它们就可以检查模型的正确性。
图一描述了由这三个类组成的UML类图。
X ChatRoom提供两个方法处理到达的事件。request处理来到的请求，每个请求都有参数clientID和roomID。ChatRoom把接收或拒绝通知发回拥有全局ID标识clientID的发送者。它也使用参数roomID来决定请求是发给它自己还是发给另外一个聊天室了1。send方法接收由客户clientID发送的消息msg。这条msg将会在一秒钟之后被广播出去。
X Client的方法accept和reject处理到达的接收和拒绝通知。参数clientID用来确定目标客户。当一个Client接收到一个broadcast事件，它会检查自己是否在clients集合中。假如情况确实如此，消息msg就会在输出中被打印出来。
X Manager中继连接请求、接收和拒绝通知、来自客户的消息以及聊天室的广播。例如，假如它收到来自聊天室的广播，有三个参数会告诉它消息最初的发送者（客户），广播者（聊天室）以及消息字符串。然后它把消息发给所有连接在聊天室中的，除了最初发送者以外的客户。
图一 类的设计
尽管这种API定义不是形式化的，但接口背后的行为还是很轻易理解的。但是，检查协议的一致性会有些困难，甚至是不可能的，原因如下：
X 行为隐藏在接口背后，它只能在理解的基础上进行解释。
X 协议是用自然语言表达的，程序不可能很轻易地处理。
X 对于一个定义完好的系统来说，会有许多接口设计。它们可能有相当大的不同。例如，本设计中用Manager类来拦截通信。另一项设计可能会使用RequestManager来拦截请求、接收和拒绝，用MessageManager来拦截消息和发送广播。更有另外一种设计可能根本就不会使用任何治理器。
4 时序图
本节讨论的时序图把设计带入比类图更低的抽象层次（更高层次的细节）。时序图必须清楚反映组件之间的交互。
图二 请求模式的时序图
图三 消息模式的时序图
4.1 定时
定时问题使得协议转化为时序图和之后转化为状态图的过程变得困难。在协议描述中，同一时刻会发生一个或多个动作，即使这些动作在某种原因下相关也是如此。例如，聊天室不应该在收到请求之前发送接收或拒绝消息。这样的话，输出迹中出现“在时刻1请求；在时刻1接收”就是正确的，假如出现“在时刻1接收；在时刻1请请求”，那就是不正确的。
一种可能的解决方案是使用tuple(t, s)表示时间，t是以秒计数的浮点时间，s是整数序号。以这种方式，正确的输出可以写成“在时刻(1.0s, 0)请求；在时刻(1.0s, 1)接收”。序列“在时刻(1.0s, 0)接收；在时刻(1.0s, 1)请求”则是不正确的。
4.2 请求和消息模式
请求模式如图二所示。Client首先会调用Manager的方法mrequest。然后Manager通过调用ChatRoom的方法request中继这个调用。ChatRoom马上响应，回调Manager的方法maccept或mreject。然后请求Client会接收到由Manager中继的响应。
图三是消息模式，在系统中随机产生消息，进行传递。注重ChatRoom在收到一次请求后故意延时一秒钟。在这两个时序图中，没有其它延时存在。
4.3 类图和协议之间的一致性问题
与类图之间的一致性是轻易检查的，可以通过收集组件接收到的所有方法调用来达成。例如，在请求模式中，Manager接收mrequest、maccept和mreject。在消息模式中，它接收msend和mbroadcast。这五个方法在类图中都有定义，但没有定义其它的公有方法。由于时序图中并没有给出参数，那样就没有检查参数的必要。检查过程可以自动化。可以部分检查协议的一致性。从请求时序图中很轻易就能看出，聊天室在时刻0收到一个请求，在时刻0接收或拒绝这个客户。这两个时刻的绝对值并不重要。重要的是，回复确实会在同一时间发回。这样设计者就可以手工检查“某个时间应该会发生什么”。假如用到后面讨论的基于规则的方法，有限的自动检查也是可以做到的。
注重基本的时序图无法表达某个时间或某个阶段不应该发生的事情。比方说，协议中会含有这样的意思，聊天室在没有收到请求时不会接收或拒绝客户。时序图中不会包含这样的信息。这会在模型中带来设计错误，影响后续开发步骤的正确性。另一种可能的设计错误是时序图的语义。例如，在请求模式中，时序图描述：假如客户发送mrequest，治理器没有时间前置地发送request，聊天室发送maccept或mreject，也没有时间前置，然后治理器发送accept或reject。不幸地是，迟钝的客户不会发送任何请求，这显然是系统当中的一个问题，不能通过检查时序图检测出来。最坏的情况是根本没有客户连接，这样系统就会永远停机。为了补偿信息丢失，需要UML形式化体系中的其它设计，它们并不完全依靠时序图，或者就要对时序图进行扩展。一个极好的使用时序图并引入扩展的例子是Live Sequence Charts，参见Harel的文章[1]。
5 状态图
状态图用来实现类定义背后的行为。它们可以在我们的SVM（状态虚拟机）[2][3]中执行，用于扩展状态图形式化的解释器是用Python编写的。
5.1 SVM约定
假如想要轻松理解状态图设计，就必须先了解SVM的一些约定。
SVM用扩展状态图形式化体系解释模型。加入了一些新的功能，尽管表现力没有加强2，但易用性却大大改进了。
尽管最初的状态图并不是模块化的，但仍然可以使用SVM实现基于组件的设计。对于聊天室模型来说这是必需的，象客户和聊天室这样的组件可以独立进行设计，但最终在系统中还是要一起工作的。组件通过导入可以进行复用。较大的组件导入一些小的组件（实例），作为它的一个状态。结果是，就象被导入组件的所有状态（分层的）和转换都是直接在这个状态当中编写一样。
SVM模型用文本文件编写。宏是在SVM中引入的一个概念。宏在SVM源文件里的MACRO节中定义。一旦定义后，在整个文本文件中就可以括在括号中使用。例如，定义PREFIX=state，[PREFIX]就可以用来代替字符串“state”，这样[PREFIX]1就等于state1。
后面就会用到其中的一些预定义宏。[EVENT(event, param)]会触发一次事件。它的参数是字符串event和可选列表param。[PARAM]用来检索在处理的事件的参数。它通常在监视哨单元或转换的输出中使用。[DUMP(msg)]打印调试信息或在文本文件中记录这些信息。
组件被导入的时候宏也可以充当参数。进行导入的组件要重新定义一部分或所有最初在被导入组件中定义的宏，也包括预定义宏。继续前面的例子，假如进行导入的组件确定PREFIX=mystate作为导入参数，被导入组件中的[PREFIX]1将会译为mystate1。
很轻易就可以看出，这些扩展并没有增加状态图的表现力。
5.2 扩展状态图形式体系中的聊天室模型
Client、ChatRoom和Manager组件分别在独立的状态图中设计。如图四所示，Chat模型导入了五个Client实例，两个ChatRoom实例和一个Manager实例。同一类型的每个实例都有一个惟一的ID参数。由于可接收的事件集合是不相交的，因此不同类型的实例就可以拥有相同的ID。这个模型可以在SVM环境中仿真或执行。
Client组件如图五所示。最初，它处在nochat状态。每隔一到三秒（非均匀分布）会触发一次mrequest事件，通过治理器来重复连接聊天室，直到请求被接收为止（accept事件被接收）。uniform是一个Python函数，它返回某个区间内的随机实数值，randint返回随机整数值。事件的第一个参数给出客户的惟一ID。第二个参数给出目的聊天室（随机从1或2中选取）。然后，客户转移到状态connected，开始发送消息和接收广播。事件参数是作为列表发送的，[PARAM][0]访问第一个参数，依次类推。注重，当方括号之间的内容不是宏的名字或Python下标时，那它就是监视哨，遵循最初状态图形式化体系中的定义[4]。
用户定义的宏[ID]为每个客户指定一个惟一ID。定义ID=0的意思是缺省值为0。它可以由导入组件（在这里是Chat模型）变为一个惟一数。组件的ID很重要。既然整个系统在导入后可以被看作一幅大的状态图，每一个正交组件都能接收到所有的广播事件。这样，给特定客户发送事件的惟一方法是在参数列表中给出接收者的ID。每一个客户都要检查在处理事件之前，它的ID是否匹配。
与Client组件相比，ChatRoom要更复杂。它使用列表messages[ID]把到来的消息进行排队。这就意味着每一个有着惟一ID的聊天室都会有其自己的队列（假如ID=0，messages[ID]与message0相等）。假如当它正在处理前面的消息时（要耗时一秒钟），一条消息到达，新到达的消息就会加入列表之中。收到消息时的时间也被记录下来，这样即使消息进行排队，它的处理时间自到达时开始计算仍为一秒钟。
Manager组件仅仅只是中继消息。在聊天室接收客户时，函数rec_comm(client, room)在一个列表中记录连接信息。get_clients(room, client)查询列表并返回聊天室room中除了client以外的所有客户。get_room(client)返回client的房间ID号。
聊天室消息队列和治理器连接列表是变量使用示例。它们帮助记录模型的状态。严格地说，这仍然是对最初状态图的扩展，状态必须明确地确定下来。讨论变量已经超出了本次个案研究的范围。
5.3 与类图之间的一致性
基于组件的设计应该严格符合图一中的类设计。再者，组件可以发送事件给接收者，但接收者却不能处理它。或者，发送者提供的参数可能会比需要的要少。这可能会造成严重的运行时错误。
自动检查所有方法调用的发送者-接收者之间的一致性，这样的程序可以写出来。而不是要编写如何在代码级由类型检查器和/或链接器来检查一致性。譬如，Manager接收事件maccept。这意味着它在类定义中提供方法maccept。在处理事件的状态转换输出和监视哨中，要用到[PARAMS][0]和[PARAMS][1]，这样它就至少需要两个参数。检查器遍历整个Chat模型，找出仅由ChatRoom组件调用（异步地）的方法。调用[EVENT("maccept",[[PARAMS][0], [ID]])]提供了两个参数（[PARAMS][0]3和[ID]）。检查这条调用是成功的。
同样地，在模型中所有方法调用的一致性可以由状态图来检查。
6 模型执行进行的一致性检查
SVM解释器可以仿真或实时（循环中有人参与的情况下需要）执行Chat模型。执行后的输出结果被转储显示并拷贝一份到文本文件。正如上面说的那样，假如所有的用户交互都明确建模的话，根本就不需要干预。输出迹是我们验证执行结果的惟一方法。必须检查所有设计制品与输出迹之间的一致性。
类图一致性在前面一节中已经研究过。检查器形式化地检查状态图设计。不需要模型执行。时序图一致性可以通过验证实验输出迹来检查。尽管许多情况下正确性仍然不能得到验证（搜索较大范围或者有可能无限状态空间的可能行为），但对最终产品的信心还是大大增加了。
状态图一致性含有假定SVM执行环境正确的意思。
使用最初的协议验证一致性并不轻易，因为它比时序图包含更多的信息。检查程序处理起来会非常困难。
图四 Chat模型
图五 Client组件
图六 聊天室组件
图七 治理器组件
6.1 输出迹
宏[DUMP(msg)]用来在文件中记录消息msg，一直到执行结束为止（或者自动，或者由调试器手动控制）。每条消息包括三个部分：时间tuple(t, s)，有着惟一ID的发送者或接收者，和消息体。下面是从输出中截取的一部分内容：
. . . . . .
CLOCK: (10.5s,0)
Client 0
Says "Hello!" to ChatRoom 1
. . . . . .
CLOCK: (11.5s,0)
ChatRoom 1
Broadcasts "Hello!" to all clients except
Client 0
. . . . . .
CLOCK: (11.5s,2)
Client 1
Receives "Hello!" from Client 0
. . . . . .
治理器产生输出，它可以访问通信过程中的所有信息。ID为0的客户在时刻10.5发送了一条消息。根据协议，1号聊天室在一秒钟后把该消息广播出去。另一个连接在1号聊天室的客户1在同一时刻收到消息。这里也可以看出消息的最初发送者。
6.2 与时序图的一致性
与时序图的一致性可以通过一套基于规则的方法检查。这些规则在文本文件中定义。检查程序读取文件，检查输出迹是否可以满足所有的规则。正则表达式被扩展之后用以描述规则。规则由四部分组成：前置条件、后置条件、监视哨（任选）和计数规则属性（任选）。前置条件是正则表达式，用来匹配部分输出迹。它与监视哨（一个布尔表达式）结合，定义何时可以使用规则。当规则可用，并且计数规则属性为false时，后置条件（另一个正则表达式）必须要在输出迹中找到；假如计数规则属性为true，后置条件一定不可满足。
例如，下面的规则就说明了消息的发送者并没有在一秒钟后收到广播。
前置条件
CLOCK: \((\d+\.{0,1}\d*)s,(\d+\.{0,1}\d*)\)\n\Client (\d+)\nSays "(.*?)" to ChatRoom (\d+)\n
后置条件
CLOCK: \([(\1+1)]s,(\d+\.{0,1}\d*)\)\nClient [(\3)]\n Receives"[(\4)]" from Client [(\3)]\n
监视哨
[(\1+1)]
计数规则
True
在前置条件中，在括号中定义了五个表达式分组。分别编号从1到5。组1匹配浮点时间。组2匹配序号。它们组成时间元组。组3匹配以整数标记的发送者的客户ID。组4匹配消息，它可以是任意的字符串。组5匹配发送者所在的聊天室。
在后置条件中，[(…)]包含一个表达式，分组值可以在 “\”后使用索引号来引用。这样，[(\1+1)]是第一个组的值加一。[(\3)]等于组3。关于正则表达式的更多内容可以在[5]中找到。
假定执行过程停止在仿真时刻50那里，检查就不应该超过时刻50。在没有额外条件的情况下，假如在时刻49.5一条消息发送到聊天室，检查程序会希望在时刻50.5时见到相应的广播。为了实现这项功能，引入了一个监视哨[(\1+1)]
客户不应该接收到它自己的消息，这就是一条计数规则。
6.3 与协议的一致性
验证模型与协议完全一致假如说是并非不可能的话，至少也是极为困难的。协议，也可以看成需求集合，是使用自然语言描述的。准确解释它是自动检查程序开发的主要障碍。
你可能会争辩说协议可以转换为一套规则。使用上面描述的基于规则的方法，协议一致性就可以检查。但是，把协议的完整含义转化为程序易于处理的形式化表达是非常困难的。协议中含有的明显事实和常识经常会丢失。作为人与程序之间的接口，自然语言处理技术是有必要的。
在这个案例中，采用了一系列步骤来达成最终的可执行设计。在把协议转换为另一种不同的形式化表达体系时，信息就会丢失。中间步骤检查并不能保证最终产品的正确性。
另一方面，检查中间步骤并不足够有效。再者说，根据初始协议直接检查模型是极端困难的事情。在这个案例中，“如何验证最终设计的正确性”是最后的，同时也是最大的公开问题。
7 结论
在这个案例研究中，我们对一个具体的例子进行了讨论。从初始需求开始，我们开发了一个可执行程序。此间经历一些步骤，在不同的抽象层次上进行设计。我们挑选了一种基于组件的方法来把模型模块化，并使模型可以治理。类图定义了组件的接口。尽管只是部分阐述了需求，时序图形式化通信，使得自动检查变为可能。在扩展状态图形式化体系中，我们建模了基于组件的模型，这个模型由SVM执行环境直接转换。开发聊天室模型会引起一系列一致性问题。对于其中一部分内容，可以成功运用自动检查功能。
1．时序图与类图间的一致性得到了检查。检查程序验证所有的必需方法在接口中都已正确地确定下来。
2．状态图与类图间的一致性也可按照同样的方法检查。事件的发送者总能为接收者提供足够的参数。
3．状态图与时序图间的一致性使用基于规则的检查程序来检查。正则表达式被扩展用来确定前置条件、后置条件、监视哨和计数规则属性。
然而，还有一些一致性问题仍然没有解决。
1．类图与协议（初始需求）之间的一致性没有检查。在后续步骤中会发现设计缺陷，或者缺陷也可能会隐藏在最终产品里面。
2．时序图与协议之间的一致性仅仅做了手工检查。尽管时序图只是协议的形式化方法，编写一个程序检查它的正确性也并不轻易。
3．检查扩展状态图中的最终设计和协议之间的一致性，要更为困难。这种检查是必要的，但信息在中间步骤有丢失现象。
应该把注重力放在这些开放问题上，它们大多与系统之间的一致性有关。一致性检查应该是开发过程中和软件开发工具的一个完整的组成部分。
参考文献
[1] D. Harel and R. Marelly. Specifying and executing behavioral requirements: The play-in/play-out approach. Technical Report MSC01-15, The Weizmann Institute of Science, 2001.
[2] Thomas Feng. An extended semantics for a Statechart Virtual Machine. In A. Bruzzone and hamed Itmi, editors, Summer Computer Simulation Conference. Student Workshop, pages S147 ? S166. The Society for Computer Modelling and Simulation, July 2003. Montr′eal, Canada.
[3] Thomas Feng. Statechart Virtual Machine (SVM), 2003. MSDL, McGill University, http://moncs.cs.mcgill.ca/people/tfeng/?research=svm.
[4] David Harel and Amnon Naamad. The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology, 5(4):293?333, 1996.
[5] Python 2.2.3 documentation, May 2003. http://www.python.org/doc/2.2.3/.
[6] David Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3):231?274, June 1987.
[7] Michael von der Beeck. A strUCtured Operational semantics for UML statecharts. Software and Systems Modeling, 1(2), 2002.
[8] Jim Rumbaugh, Ivar Jacobson, and Grady Booch. The Unified Modeling Language Reference Manual. Addison-Wesley, 1998.
1UML状态图（UML 2.0以前的版本）在后面步骤中会用到，它不答应确定事件的接收者，即使只有一个聊天室会处理事件，所有的聊天室也同样都会收到相同的请求。
2为了增强表达能力，可以引入某些扩展，但这样的话检查模型的正确性将变得更加困难。
3这里[PARAM][0]的指的是事件请求的第一个参数，它可以由ChatRoom组件来处理。这个参数会进一步在事件maccept中传递，它是后者的第一个参数。
