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

　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)]<50
　　
　　计数规则
　　True
　　
　　在前置条件中，在括号中定义了五个表达式分组。分别编号从1到5。组1匹配浮点时间。组2匹配序号。它们组成时间元组。组3匹配以整数标记的发送者的客户ID。组4匹配消息，它可以是任意的字符串。组5匹配发送者所在的聊天室。
　　
　　在后置条件中，[(…)]包含一个表达式，分组值可以在 “\”后使用索引号来引用。这样，[(\1+1)]是第一个组的值加一。[(\3)]等于组3。关于正则表达式的更多内容可以在[5]中找到。
　　
　　假定执行过程停止在仿真时刻50那里，检查就不应该超过时刻50。在没有额外条件的情况下，如果在时刻49.5一条消息发送到聊天室，检查程序会希望在时刻50.5时见到相应的广播。为了实现这项功能，引入了一个监视哨[(\1+1)]<50。它会告知检查程序这条规则仅在分组1的值加一小于50时可用。
　　
　　客户不应该接收到它自己的消息，这就是一条计数规则。
　　
　　6.3 与协议的一致性
　　
　　验证模型与协议完全一致如果说是并非不可能的话，至少也是极为困难的。协议，也可以看成需求集合，是使用自然语言描述的。准确解释它是自动检查程序开发的主要障碍。
　　
　　你可能会争辩说协议可以转换为一套规则。使用上面描述的基于规则的方法，协议一致性就可以检查。但是，把协议的完整含义转化为程序易于处理的形式化表达是非常困难的。协议中含有的明显事实和常识常常会丢失。作为人与程序之间的接口，自然语言处理技术是有必要的。
　　
　　在这个案例中，采用了一系列步骤来达成最终的可执行设计。在把协议转换为另一种不同的形式化表达体系时，信息就会丢失。中间步骤检查并不能保证最终产品的正确性。
　　
　　另一方面，检查中间步骤并不足够有效。再者说，根据初始协议直接检查模型是极端困难的事情。在这个案例中，“如何验证最终设计的正确性”是最后的，同时也是最大的公开问题。