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

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中传递，它是后者的第一个参数。