|
摘要 本文从初始需求开始构建聊天室模型以及对个案进行研究在不同的开发阶段分别要用到UML类图时序图和状态图这样难免需要确定一致性问题现在已经提出了许多仿真和方法用来确保模型各个方面的一致性我们关注内部一致性即给定模型内部制品之间的一致性问题 简介 软件系统的开发过程通常会被划分成一些步骤每个步骤会用到不同的UML图由于建模系统变得越来越复杂一致性问题就越发突出起来而在其中有两种类型或问题更为显着第一内部一致性问题涉及给定模型内部制品之间的一致性第二系统之间一致性问题涉及软件开发过程中不同演化模型之间的一致性我们主要关注于内部一致性问题 不同的文献提出了不同的形式化方法用来自动检查一致性发现设计当中存在的问题在下面几节里我们分步研究了一个聊天室的开发过程本文的灵感来源于Agder大学Geir Melby完成的一次项目报告（）这个模型提出了一些潜在的一致性问题对于它们当中的部分内容也给出了自动化的一致性检查方法 在这份案例研究中我们从需求开始开发了一个聊天室模型第二节给出了客户管理器对象以及聊天室之间的通信协议作为初始需求第三节研究了一个可能的类的设计它定义了符合协议的接口第四节中给出的时序图进一步定义和描述了组件之间的通信并保持与类设计之间的一致性第五节使用状态图更进一步地确定应用程序的行为这份规程可以在我们的SVM（状态图虚拟机）环境中实时地进行仿真或执行在第六节中讨论了协议规程与仿真迹的一致性第七节进行总结 通信协议 我们将要创建的聊天室程序是按照客户机/服务器范型来架构的客户会随机连接聊天室如果某个聊天室接收了客户客户就会发送消息给这个聊天室然后聊天室广播每条消息除了发送者以外每个与聊天室建立连接的客户都会收到一份拷贝 下面将要描述一个特定的简化了的用例 X系统包括五个客户和两个聊天室客户端最初没有连接每隔一到三秒（非均匀分布）它们都会随机连接一个聊天室被请求的聊天室同时收到请求（假定没有网络延时并且通信可靠） X一个聊天室至多接收三个客户当且仅当容量没有超标时聊天室才会接收连接 X 发出请求的客户会立刻收到接收或拒绝通知 X在客户可以发送聊天信息之前必须被一个聊天室接收 X连接建立之后客户会每隔一到五秒（非均匀分布）给它所连接的聊天室发送随机消息聊天室会立即接收消息它将耗时一秒钟来处理接收到的消息并把它广播给除发送者之外的所有连接客户 X客户会同时收到广播为了简化起见我们不讨论没有连接的情况 类的设计 根据上面的规定显然我们需要两个类Client和ChatRoom在开发过程早期阶段对于仿真来说无需用户干预我们明确地按照随机过程对用户行为（连接请求和聊天信息）进行建模以后客户模型将会被与软件打交道的真实客户所代替仿真开始时会初始化五个Client实例和两个ChatRoom实例 我们还加入了一个singleton类ManagerManager以仲裁者的身份中继组件之间的所有通信这种中央控制措施将会帮助截取系统传递的所有消息使用它们就可以检查模型的正确性 图一描述了由这三个类组成的UML类图 X ChatRoom提供两个方法处理到达的事件request处理来到的请求每个请求都有参数clientID和roomIDChatRoom把接收或拒绝通知发回拥有全局ID标识clientID的发送者它也使用参数roomID来决定请求是发给它自己还是发给另外一个聊天室了send方法接收由客户clientID发送的消息msg这条msg将会在一秒钟之后被广播出去 X Client的方法accept和reject处理到达的接收和拒绝通知参数clientID用来确定目标客户当一个Client接收到一个broadcast事件它会检查自己是否在clients集合中如果情况确实如此消息msg就会在输出中被打印出来 X Manager中继连接请求接收和拒绝通知来自客户的消息以及聊天室的广播例如如果它收到来自聊天室的广播有三个参数会告诉它消息最初的发送者（客户）广播者（聊天室）以及消息字符串然后它把消息发给所有连接在聊天室中的除了最初发送者以外的客户 图一 类的设计 尽管这种API定义不是形式化的但接口背后的行为还是很容易理解的但是检查协议的一致性会有些困难甚至是不可能的原因如下 X 行为隐藏在接口背后它只能在理解的基础上进行解释 X 协议是用自然语言表达的程序不可能很容易地处理 X 对于一个定义完好的系统来说会有许多接口设计它们可能有相当大的不同例如本设计中用Manager类来拦截通信另一项设计可能会使用RequestManager来拦截请求接收和拒绝用MessageManager来拦截消息和发送广播更有另外一种设计可能根本就不会使用任何管理器 时序图 本节讨论的时序图把设计带入比类图更低的抽象层次（更高层次的细节）时序图必须清晰反映组件之间的交互 图二 请求模式的时序图 图三 消息模式的时序图 定时 定时问题使得协议转化为时序图和之后转化为状态图的过程变得困难在协议描述中同一时刻会发生一个或多个动作即使这些动作在某种原因下相关也是如此例如聊天室不应该在收到请求之前发送接收或拒绝消息这样的话输出迹中出现在时刻请求在时刻接收就是正确的如果出现在时刻接收在时刻请请求那就是不正确的 一种可能的解决方案是使用tuple(t s)表示时间t是以秒计数的浮点时间s是整数序号以这种方式正确的输出可以写成在时刻(s )请求在时刻(s )接收序列在时刻(s )接收在时刻(s )请求则是不正确的 请求和消息模式 请求模式如图二所示Client首先会调用Manager的方法mrequest然后Manager通过调用ChatRoom的方法request中继这个调用ChatRoom立刻响应回调Manager的方法maccept或mreject然后请求Client会接收到由Manager中继的响应 图三是消息模式在系统中随机产生消息进行传递注意ChatRoom在收到一次请求后故意延时一秒钟在这两个时序图中没有其它延时存在 类图和协议之间的一致性问题 与类图之间的一致性是容易检查的可以通过收集组件接收到的所有方法调用来达成例如在请求模式中Manager接收mrequestmaccept和mreject在消息模式中它接收msend和mbroadcast这五个方法在类图中都有定义但没有定义其它的公有方法由于时序图中并没有给出参数那样就没有检查参数的必要检查过程可以自动化可以部分检查协议的一致性从请求时序图中很容易就能看出聊天室在时刻收到一个请求在时刻接收或拒绝这个客户这两个时刻的绝对值并不重要重要的是回复确实会在同一时间发回这样设计者就可以手工检查某个时间应该会发生什么如果用到后面讨论的基于规则的方法有限的自动检查也是可以做到的 注意基本的时序图无法表达某个时间或某个阶段不应该发生的事情比方说协议中会含有这样的意思聊天室在没有收到请求时不会接收或拒绝客户时序图中不会包含这样的信息这会在模型中带来设计错误影响后续开发步骤的正确性另一种可能的设计错误是时序图的语义例如在请求模式中时序图描述如果客户发送mrequest管理器没有时间前置地发送request聊天室发送maccept或mreject也没有时间前置然后管理器发送accept或reject不幸地是迟钝的客户不会发送任何请求这显然是系统当中的一个问题不能通过检查时序图检测出来最坏的情况是根本没有客户连接这样系统就会永远停机为了补偿信息丢失需要UML形式化体系中的其它设计它们并不完全依赖时序图或者就要对时序图进行扩展一个极好的使用时序图并引入扩展的例子是Live Sequence Charts参见Harel的文章[] 状态图 状态图用来实现类定义背后的行为它们可以在我们的SVM（状态虚拟机）[][]中执行用于扩展状态图形式化的解释器是用Python编写的 SVM约定 如果想要轻松理解状态图设计就必须先了解SVM的一些约定 SVM用扩展状态图形式化体系解释模型加入了一些新的功能尽管表现力没有加强但易用性却大大改进了 尽管最初的状态图并不是模块化的但仍然可以使用SVM实现基于组件的设计对于聊天室模型来说这是必需的象客户和聊天室这样的组件可以独立进行设计但最终在系统中还是要一起工作的组件通过导入可以进行复用较大的组件导入一些小的组件（实例）作为它的一个状态结果是就象被导入组件的所有状态（分层的）和转换都是直接在这个状态当中编写一样 SVM模型用文本文件编写宏是在SVM中引入的一个概念宏在SVM源文件里的MACRO节中定义一旦定义后在整个文本文件中就可以括在括号中使用例如定义PREFIX=state[PREFIX]就可以用来代替字符串state这样[PREFIX]就等于state 后面就会用到其中的一些预定义宏[EVENT(event param)]会触发一次事件它的参数是字符串event和可选列表param[PARAM]用来检索在处理的事件的参数它通常在监视哨单元或转换的输出中使用[DUMP(msg)]打印调试信息或在文本文件中记录这些信息 组件被导入的时候宏也可以充当参数进行导入的组件要重新定义一部分或所有最初在被导入组件中定义的宏也包括预定义宏继续前面的例子如果进行导入的组件确定PREFIX=mystate作为导入参数被导入组件中的[PREFIX]将会译为mystate 很容易就可以看出这些扩展并没有增加状态图的表现力 扩展状态图形式体系中的聊天室模型 ClientChatRoom和Manager组件分别在独立的状态图中设计如图四所示Chat模型导入了五个Client实例两个ChatRoom实例和一个Manager实例同一类型的每个实例都有一个惟一的ID参数由于可接收的事件集合是不相交的因此不同类型的实例就可以拥有相同的ID这个模型可以在SVM环境中仿真或执行 Client组件如图五所示最初它处在nochat状态每隔一到三秒（非均匀分布）会触发一次mrequest事件通过管理器来重复连接聊天室直到请求被接收为止（accept事件被接收）uniform是一个Python函数它返回某个区间内的随机实数值randint返回随机整数值事件的第一个参数给出客户的惟一ID第二个参数给出目的聊天室（随机从或中选取）然后客户转移到状态connected开始发送消息和接收广播事件参数是作为列表发送的[PARAM][]访问第一个参数依次类推注意当方括号之间的内容不是宏的名字或Python下标时那它就是监视哨遵循最初状态图形式化体系中的定义[] 用户定义的宏[ID]为每个客户指定一个惟一ID定义ID=的意思是缺省值为它可以由导入组件（在这里是Chat模型）变为一个惟一数组件的ID很重要既然整个系统在导入后可以被看作一幅大的状态图每一个正交组件都能接收到所有的广播事件这样给特定客户发送事件的惟一方法是在参数列表中给出接收者的ID每一个客户都要检查在处理事件之前它的ID是否匹配 与Client组件相比ChatRoom要更复杂它使用列表messages[ID]把到来的消息进行排队这就意味着每一个有着惟一ID的聊天室都会有其自己的队列（如果ID=messages[ID]与message相等）如果当它正在处理前面的消息时（要耗时一秒钟）一条消息到达新到达的消息就会加入列表之中收到消息时的时间也被记录下来这样即使消息进行排队它的处理时间自到达时开始计算仍为一秒钟 Manager组件仅仅只是中继消息在聊天室接收客户时函数rec_comm(client room)在一个列表中记录连接信息get_clients(room client)查询列表并返回聊天室room中除了client以外的所有客户get_room(client)返回client的房间ID号 聊天室消息队列和管理器连接列表是变量使用示例它们帮助记录模型的状态严格地说这仍旧是对最初状态图的扩展状态必须明确地确定下来讨论变量已经超出了本次个案研究的范围 与类图之间的一致性 基于组件的设计应该严格符合图一中的类设计再者组件可以发送事件给接收者但接收者却不能处理它或者发送者提供的参数可能会比需要的要少这可能会造成严重的运行时错误 自动检查所有方法调用的发送者接收者之间的一致性这样的程序可以写出来而不是要编写如何在代码级由类型检查器和/或链接器来检查一致性譬如Manager接收事件maccept这意味着它在类定义中提供方法maccept在处理事件的状态转换输出和监视哨中要用到[PARAMS][]和[PARAMS][]这样它就至少需要两个参数检查器遍历整个Chat模型找出仅由ChatRoom组件调用（异步地）的方法调用[EVENT(maccept[[PARAMS][] [ID]])]提供了两个参数（[PARAMS][]和[ID]）检查这条调用是成功的 同样地在模型中所有方法调用的一致性可以由状态图来检查 模型执行进行的一致性检查 SVM解释器可以仿真或实时（循环中有人参与的情况下需要）执行Chat模型执行后的输出结果被转储显示并拷贝一份到文本文件正如上面说的那样如果所有的用户交互都明确建模的话根本就不需要干预输出迹是我们验证执行结果的惟一方法必须检查所有设计制品与输出迹之间的一致性 类图一致性在前面一节中已经研究过检查器形式化地检查状态图设计不需要模型执行时序图一致性可以通过验证实验输出迹来检查尽管许多情况下正确性仍然不能得到验证（搜索较大范围或者有可能无限状态空间的可能行为）但对最终产品的信心还是大大增加了 状态图一致性含有假定SVM执行环境正确的意思 使用最初的协议验证一致性并不容易因为它比时序图包含更多的信息检查程序处理起来会非常困难 图四 Chat模型 图五 Client组件 图六 聊天室组件 图七 管理器组件 输出迹 宏[DUMP(msg)]用来在文件中记录消息msg一直到执行结束为止（或者自动或者由调试器手动控制）每条消息包括三个部分时间tuple(t s)有着惟一ID的发送者或接收者和消息体下面是从输出中截取的一部分内容 CLOCK: (s) Client Says Hello! to ChatRoom CLOCK: (s) ChatRoom Broadcasts Hello! to all clients except Client CLOCK: (s) Client Receives Hello! from Client 管理器产生输出它可以访问通信过程中的所有信息ID为的客户在时刻发送了一条消息根据协议号聊天室在一秒钟后把该消息广播出去另一个连接在号聊天室的客户在同一时刻收到消息这里也可以看出消息的最初发送者 与时序图的一致性 与时序图的一致性可以通过一套基于规则的方法检查这些规则在文本文件中定义检查程序读取文件检查输出迹是否可以满足所有的规则正则表达式被扩展之后用以描述规则规则由四部分组成前置条件后置条件监视哨（任选）和计数规则属性（任选）前置条件是正则表达式用来匹配部分输出迹它与监视哨（一个布尔表达式）结合定义何时可以使用规则当规则可用并且计数规则属性为false时后置条件（另一个正则表达式）必须要在输出迹中找到如果计数规则属性为true后置条件一定不可满足 例如下面的规则就说明了消息的发送者并没有在一秒钟后收到广播 前置条件 CLOCK: \((\d+\{}\d*)s(\d+\{}\d*)\)\n\Client (\d+)\nSays (*?) to ChatRoom (\d+)\n 后置条件 CLOCK: \([(\+)]s(\d+\{}\d*)\)\nClient [(\)]\n Receives[(\)] from Client [(\)]\n 监视哨 [(\+)]<50 计数规则 True 在前置条件中，在括号中定义了五个表达式分组。TW.WinGwIT.Com分别编号从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 与协议的一致性 验证模型与协议完全一致如果说是并非不可能的话，至少也是极为困难的。协议，也可以看成需求集合，是使用自然语言描述的。准确解释它是自动检查程序开发的主要障碍。 你可能会争辩说协议可以转换为一套规则。使用上面描述的基于规则的方法，协议一致性就可以检查。但是，把协议的完整含义转化为程序易于处理的形式化表达是非常困难的。协议中含有的明显事实和常识常常会丢失。作为人与程序之间的接口，自然语言处理技术是有必要的。 在这个案例中，采用了一系列步骤来达成最终的可执行设计。在把协议转换为另一种不同的形式化表达体系时，信息就会丢失。中间步骤检查并不能保证最终产品的正确性。 另一方面，检查中间步骤并不足够有效。再者说，根据初始协议直接检查模型是极端困难的事情。在这个案例中，“如何验证最终设计的正确性”是最后的，同时也是最大的公开问题。 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, [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. [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中传递，它是后者的第一个参数。 |
