6.3 与协议的一致性

    验证模型与协议完全一致如果说是并非不可能的话，至少也是极为困难的。协议，也可以看成需求集合，是使用自然语言描述的。准确解释它是自动检查程序开发的主要障碍。

    你可能会争辩说协议可以转换为一套规则。使用上面描述的基于规则的方法，协议一致性就可以检查。但是，把协议的完整含义转化为程序易于处理的形式化表达是非常困难的。协议中含有的明显事实和常识常常会丢失。作为人与程序之间的接口，自然语言处理技术是有必要的。

    在这个案例中，采用了一系列步骤来达成最终的可执行设计。在把协议转换为另一种不同的形式化表达体系时，信息就会丢失。中间步骤检查并不能保证最终产品的正确性。

    另一方面，检查中间步骤并不足够有效。再者说，根据初始协议直接检查模型是极端困难的事情。在这个案例中，“如何验证最终设计的正确性”是最后的，同时也是最大的公开问题。

    7 结论

    在这个案例研究中，我们对一个具体的例子进行了讨论。从初始需求开始，我们开发了一个可执行程序。此间经历一些步骤，在不同的抽象层次上进行设计。我们挑选了一种基于组件的方法来把模型模块化，并使模型可以管理。类图定义了组件的接口。尽管只是部分阐述了需求，时序图形式化通信，使得自动检查变为可能。在扩展状态图形式化体系中，我们建模了基于组件的模型，这个模型由SVM执行环境直接转换。开发聊天室模型会引起一系列一致性问题。对于其中一部分内容，可以成功运用自动检查功能。

    1.时序图与类图间的一致性得到了检查。检查程序验证所有的必需方法在接口中都已正确地确定下来。

    2.状态图与类图间的一致性也可按照同样的方法检查。事件的发送者总能为接收者提供足够的参数。

    3.状态图与时序图间的一致性使用基于规则的检查程序来检查。正则表达式被扩展用来确定前置条件、后置条件、监视哨和计数规则属性。

    然而，还有一些一致性问题仍然没有解决。

    1.类图与协议(初始需求)之间的一致性没有检查。在后续步骤中会发现设计缺陷，或者缺陷也可能会隐藏在最终产品里面。

    2.时序图与协议之间的一致性仅仅做了手工检查。尽管时序图只是协议的形式化方法，编写一个程序检查它的正确性也并不容易。

    3.检查扩展状态图中的最终设计和协议之间的一致性，要更为困难。这种检查是必要的，但信息在中间步骤有丢失现象。

    应该把注意力放在这些开放问题上，它们大多与系统之间的一致性有关。一致性检查应该是开发过程中和软件开发工具的一个完整的组成部分。