6 模型执行进行的一致性检查
SVM解释器可以仿真或实时(循环中有人参与的情况下需要)执行Chat模型。执行后的输出结果被转储显示并拷贝一份到文本文件。正如上面说的那样，如果所有的用户交互都明确建模的话，根本就不需要干预。输出迹是我们验证执行结果的惟一方法。必须检查所有设计制品与输出迹之间的一致性。
类图一致性在前面一节中已经研究过。检查器形式化地检查状态图设计。不需要模型执行。时序图一致性可以通过验证实验输出迹来检查。尽管许多情况下正确性仍然不能得到验证(搜索较大范围或者有可能无限状态空间的可能行为)，但对最终产品的信心还是大大增加了。
状态图一致性含有假定SVM执行环境正确的意思。
使用最初的协议验证一致性并不容易，因为它比时序图包含更多的信息。检查程序处理起来会非常困难。
图四 Chat模型
图五 Client组件
图六 聊天室组件
图七 管理器组件
