个案研究：聊天室UML模型一致性问题

　　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在同一时刻收到消息。这里也可以看出消息的最初发送者。