基于消息序列图的情景分析形式化技术的轻量级应用——验证和模拟用户需求的形式化方法

1网址：http://www.elsevier.nl/locate/entcs/volume65.html17页基于消息序列图的情景分析形式化技术普兰达尔巴杜里河Venkatesh和Girish K. 帕尔希卡尔印度浦那市哈达萨工业区54 B塔塔咨询服务有限公司，邮编411 013电子邮件：{pbhaduri，rvenky，girishp}@ pune.tcs.co.in摘要本文介绍了轻量级的形式化技术的基础上，消息序列图（MSC）的捕获和验证早期的需求和设计。我们的重点是在指定、模拟和验证场景时的易用性，并有效地检查它们所需的属性。我们讨论了如何的形式主义的高级消息序列图（HMSC或MSC'96），可用于捕获的用例中的场景，从而使工具的使用进行分析。然后，我们提出了两个正式的语义HMSC-一个直观的线性时间语义运行的基础上，和操作语义标记的过渡系统。 接下来，我们提出了一种使用模板描述用例场景的期望属性的方法，用于验证关于非正式需求的场景。然后，可以通过用于在表示MSC的事件上的优先关系的有向图中查找路径的有效算法来建立MSC的集合的正确性属性。我们以模拟和验证工具的形式实现了操作语义和验证算法，用于分析场景。1介绍我们在本文中的目的是应用形式化的方法在捕获和验证用户的需求。其目标是将用例捕获的需求形式化[8]，就像基于UML的面向对象建模中所采用的那样[4]。我们打算使用消息序列图（MSC）的正式符号为UML中的用例提供严格的语义[7，11，12]。这为用例场景的建模带来了几个好处。由于MSC是一种正式的符号，具有正式的语法和语义，因此可以构建工具来分析它们。此外，MSC通过允许在一个模型或图中呈现具有分支和循环的多个场景，以及通过利用层次结构的力量以便于理解和重用，以基本的方式扩展了UML序列图2002年由ElsevierScienceB出版。 诉操作访问根据C CB Y-NC-N D许可证进行。2MSCs通过关注软件系统中通信实体之间的消息交换，提供了一种直观和可视化的需求描述方式最近由ITU [7]对MSC（MSC'96或Z.120）的语法和语义的标准化以及它们用于捕获早期设计要求的流行（参见[1，6]）已经导致用于分析它们的属性的商业工具。MSC的扩展，称为实时序列图（LSC），已被提出作为[5]中用例和场景的语义上合理的基础。本文的目标类似于[2，5]，即开发形式化分析技术和工具，以便在软件工程中有效地使用基于XML的需求然而，我们的重点是在规范和验证方面的易用性，而不是表达能力。由于大多数用户、设计师和开发人员不太可能熟悉正式的规范和验证技术，因此我们试图将尽可能多的形式隐藏在工具背后，并为用户提供一个友好直观的可视化界面来分析场景。特别是，我们使用户能够通过以交互方式模拟用例中的各种场景来验证系统需求为此，我们提出了一个操作语义的HMSC符号，这已在模拟器中实现。作为验证需求的另一种可能的方法，我们提出了一种小型的模板规范语言，用于说明MSC集合的理想属性。这种语言很直观，可以以下拉菜单和列表框的形式呈现给用户。这些属性的验证是通过在表示MSC事件的优先关系的有向图中搜索适当的路径来实现的。 我们的模板规范语言足够强大，可以捕获优先和响应（或结果）属性[9]。 优先属性声明一个状态/事件的发生是另一个状态/事件发生的必要先决条件。优先属性的一个例子是另一方面，响应属性表明，当一个状态发生时，另一个状态的发生必须随之发生。一个例子是虽然在[10]中已经探索了MSC中的模板匹配的思想，但是重点是指定事件的相对顺序的模式和匹配过程的有效算法。作者将模板指定为MSC，匹配被定义为优先关系之间存在同态嵌入。此外，视觉顺序和优先顺序之间的差异增加了模板匹配过程的复杂性相比之下，我们的模板是以事件排序的线性化来表示的，其中事件是发送和接收命名消息。其结果是，我们的算法有多项式复杂性的模板属性，我们已经考虑。这里报告的工作是一个方案的一部分，将行为建模的背景下，基于元模型的案例工具。因为3仅仅呈现系统动态的一个方面，它们必须与其他开发视图集成，无论是静态的（例如，类，对象）和动态（例如，状态机）。我们的目标是达到一个共同的语义域的静态和动态的系统视图每个单独的视图，如MSC或状态机，将映射到这个公共语义域。这种统一的语义建模将确保视图之间的一致性以及从中生成的代码的兼容性在本文中，我们不追求这个一般的框架工作，并集中在正式的软件工程基于MSC的分析技术该文件的主要贡献是双重的。首先，我们以标记转换系统（lts）的形式提出的HMSC的操作语义是新的。我们已经建立了一个模拟器HMSC实现这种语义通过运行对应的LTS的抽象机这允许用户探索HMSC描述的各种场景，包括模拟分支点和迭代循环的行为。其次，我们提出的验证框架，基于使用模式和有效验证算法的属性指定，以前没有被探索这种正式核查办法的主要优点是易于使用和效率高。用户不必熟悉时态逻辑或模型检查技术，就可以执行简单的验证和确认任务。由于性质检测算法的多项式时间复杂度，避免了传统模型检测方法本文的组织结构如下。在第2节中，我们简要地描述了MSC的形式主义，并讨论了它如何在用例场景中正式地捕获流程在第3节中，我们描述了一个线性时间语义的HMSC运行和操作语义的基础上适合作为HMSC的仿真工具第4节描述了MSC特性的具体化和验证技术第5节将我们的工作放在正式软件工程计划的角度。2消息序列图消息序列图（MSC）是一种用于描述实体之间交互的图形语言，由ITU-TS标准化图1是描绘电话呼叫中的典型场景的基本MSC的示例MSC中标记为呼叫方、交换机和被呼叫方的垂直线表示通信实体，也称为实例。MSC中的一个实例显示了从上到下的时间流程实例之间的水平箭头表示消息。箭头从发送实例开始，在接收实例结束。图中标记为空闲、通话和连接的六边形被称为条件。 有关符号的详细信息，请参阅ITU建议Z.120 [7]。4电话呼叫者开关呼叫者O型钩DialTone拨号数字空闲电话铃声O型钩回答说话说话挂机连接断开挂机空闲图1.一、电话呼叫中典型场景的消息序列图ITU建议还定义了高级MSC（HMSC），用于使用迭代和分支来分层构建多个场景HMSC的一个例子是图2左侧所示的电话呼叫场景，其中每个圆形框（称为节点或MSC参考）指的是基本MSC或另一个HMSC。节点之间的边描述了控制流。 分支和循环描述了场景中的可选流程和迭代操作。 在图中，Cancel和Disconnect是MSC引用，指的是基本MSC，如右侧所示。HMSC电话呼叫场景中的所有其他节点指的是未示出的基本MSC图2中的HMSC电话呼叫场景描述了除了图1中描述的正常流程之外，电话呼叫中可能发生的多个场景：(i) 呼叫者可以在被呼叫者应答之前断开连接这种情况由从节点Request到节点Cancel的输出分支捕获。正常的流程对应于从请求到应答的输出分支。(ii) 从Cancel和Disconnect到Request的反向循环捕获重复或迭代操作的可能性。5电话_呼叫_场景请求取消答复连接断开取消主叫方切换被叫方挂机取消断开连接主叫方切换被叫方挂机断开挂机图二. 高级MSC我们基于MSC的用例形式化旨在开发用于描述和分析用例场景的工具。所获得的好处是为模拟、分析、测试用例生成和形式验证提供工具支持。这种分析的先决条件是MSC和HMSC符号的形式语义的存在，这是下一节的主题3HMSC的语义在本节中，我们提出了两个语义的HMSC-线性时间语义的基础上运行的概念和操作语义的标记的转换系统。虽然前者对于理解和推理MSC是有用的，但后者更适合在模拟器中实现HMSC的行为。3.1线性时间语义我们提出了基于运行的MSC语言的线性时间语义，正如Damm和Harel在[5]中所做的那样。对我们来说，HMSC的运行是有限的，6→→在事件的有限序列中。这些事件是从实例i到实例j发送或接收消息msg，或定时器事件（设置、重置和超时）。消息传递可以是同步的，也可以是异步的，我们假设有一种方法可以用这些信息来注释消息我们从基本MSC的抽象语法开始，如[5]。对于MSC m中的每个实例i，我们将有限数量的离散位置l相关联，这些位置从实例i的顶部到底部编号，使用{0， . ，lmax（m，i）}。 在MSCm中的每个实例中的一个会话，表示为i，i，m，用条件或事件来标记换句话说，位置是指MSC实例上的区域，该区域包含条件、消息发送或消息接收或定时器事件（设置、重置、超时）。我们当所引用的MSC从上下文中清除时，将从位置中删除下标m基本MSCm的语义是根据偏序定义的，≤m由m在它的位置集<$i，l<$i上诱导的。偏序由以下优先关系R m获得：• 沿实例线排列i，l<$Rm<$i，l+1 <$，除非两个连续位置在共区域中• 消息发送引起的顺序：如果i，l是发送事件，并且iJ，lJ是消息的对应接收事件，则i，lRmiJ，lJ;• 同步消息阻止发送方，直到接收：如果i，l是发送事件，iJ，lJ是同步消息的相应接收事件，则iJ，ljRm i，l+1;• 共享条件导致同步障碍：如果位置i，l和iJ，lj共享条件c，则i，lR miJ，lJ+1。我们假设MSCm是格式良好的，即，关系式Rm是非循环的。我们称Rm为MSCm的优先关系。则偏序≤m是Rm的自反传递闭包。图3示出了基本MSC及其相关联的部分顺序。定义3.1基本MSC m的语义是与≤m兼容的游程的集合，即，所有偏序线性化的集合≤m。✷请注意，这意味着我们有一个concur的交错语义还要注意，基本MSC的语义是有限序列的有限集合。接下来，我们将MSC-图[2]定义为HMSC的受限形式，其中每个节点都是基本MSC。定义3.2 MSC-图G是一个元组（V，，v I，v T，μ），其中V是顶点的集合，是V上的二元关系，v I是初始顶点，v T是终端顶点，μ是将每个顶点v映射到MSC m的标记函数。✷7∈∪∈∪从这个MSC图中，我们可以得到从初始顶点开始到终端顶点结束的有限路径，代表系统的有限执行。此外，由于MSC图中存在循环，因此存在从表示系统的无限执行的初始顶点开始的无限路径 在定义MSC图的语义时，我们必须定义异步连接两个MSC意味着什么[2]。直观地说，这对应于一个实例接一个实例地连接MSC。定义3.3具有相同实例集的两个MSCm1和m2的异步级联是由以下关系的传递闭包给出的位置（m1）位置（m2）上的偏序≤m1;m2≤m1≤m2<${（i，l<$m1，i，lJ<$m2） | ⟨i, l⟩m1 ∈ locations (m1)∧lJ<$m2∈locations（m2）}其中XY表示集合X和Y的不相交并集。✷定义3.4MSC-图G的语义是通过以下方式获得的所有有限和无限运行的集合(i) 沿每条路径异步连接每个基本MSC，然后(ii) 在第一步中从偏序得到的游程集合的所有路径上取不相交的并集，包括有限和无限✷在上述定义中有一个微妙之处。MSC图中的路径可能涉及循环，其中一些节点重复。在执行异步级联操作时，必须非常小心地重命名同一基本MSC中的位置。这就是使用不相交联合操作的原因。最后，一个HMSC由一个图组成，其节点要么是基本的MSC，要么用另一个HMSC标记，允许图的嵌套。定义3.5HMSC H是一个元组（N，B，vI，vT，μ，E），其中N是节点的有限集合，B是盒子（或超节点）的有限集合，vI N B是初始节点或盒子，vTN B是终端节点或盒子，μ是一个标签函数，将N中的每个节点映射到MSC，B中的每个盒子映射到已经定义的HMSC，E是将节点和盒子彼此连接的边的集合HMSCH的含义是通过递归地将每个框替换为相应的HMSC以获得MSC图来定义的。详细情况见[2]。3.2HMSC的操作语义在最后一节中提出的HMSC的线性时间语义是非构造性的，不适合作为仿真的基础。在这里，我们提出了一个操作语义，它可以直接实现的抽象机器的形式此语义通过带标签的8≤联系我们−→⊆ ××−→C−→ ∈C−→C−→≤≤转移系统（C，i，E，）其中C是配置或状态的集合，i是初始配置，E是事件的集合，C E C是转移关系。与线性时间语义一样，我们从基本的MSC开始。通过使用用于从事件的偏序获得自动机的标准技术，从第3.1节中定义的偏序m直接获得基本MSCm定义3.6事件的偏序（E，≤）中的截集c是E的向下闭子集，即，e∈c和EJ≤e意味着EJ∈c。从E得到的割集记为C（E）。✷直觉上，切割代表一致的全局状态或配置。空切口代表初始配置，此时没有事件发生。定义3.7给定事件的偏序（E，），我们定义一个转移关系（（E），，E，）如下：对于c，d（E），有一个转移cedi d = ce。我们说事件e在MSC的配置c中启用m，表示为enabled（e，c，m）。✷注意enabled（e，n，m）等价于e是偏序中的最小元素（locations（m），≤m）。定义3.8基本MSCm的操作语义由转换系统（（E），，E，）给出，其中E是偏序（事件（m），m），其中events（m）是仅具有发送、接收和定时器事件的m的位置的集合，即，条件被忽略。✷我们现在定义HMSC的操作语义与3.1节一样，我们从MSC图的简单情况开始，其中MSC的嵌套级别为1。与基本MSC相比，MSC图的操作语义呈现出一些复杂性和微妙之处。由于在线性时间解释中使用的异步级联，在任何时候，控制可以驻留在MSC图中的多个顶点中。这些顶点甚至不需要形成连续链或路径-其中可能存在“孔”。此外，由于MSC图中的循环，顶点的多于一个的化身可以是活动的。此外，由于图中的分支，一个顶点的两个不同化身可以选择在分支点处做出不同的选择。以下定义考虑了所有这些并发症。定义3.9 MSC-图G =（V，→，v I，v T，μ）的配置C是对m< p，c>的一对e，其中p=[v1， . ，vn]是G中从v1= v 1开始的有限路，c是基本MSC m = m 1中的一种构型，在定义3.7的意义上，. ..m n，其中μ（v i）= m i。✷请注意，同一个顶点v在路径p中可能出现不止一次。9∈∅−→ {}∈1n1nn+1个我们通过变换系统（C，vI，v>，Eτ，−→）定义了MSC-图G的操作语义，其中C是配置集如上定义，E=V Vm=µ（v）events（m）×N是所有事件中的事件集合，G中的基本MSC由自然数索引，τ是一个特殊事件，称为沉默事件初始构形由从G中的初始顶点vI开始的空路径和空事件集组成定义3.10组态之间的跃迁关系（带有τ标记跃迁）由以下情况定义：(i) < [v1， . ，vn]， c><[v1， . . . ，vn]，ce>ifevents（mi）被启用在配置C中。(ii) < [v，.，v]，c >−τ→<[v，.，v，v]，c >如果配置c配置-在基本MSC m = m1;. ;在我的生活中没有任何实例。在MSC-图G中，向量xvn+1是vn的任意后继.✷上面的定义捕获了这样的直觉：MSC图G的执行的一个步骤或者在路径p=[v1， . . . ，vn]的一个新的顶点v n +1，或者当v n +1中的一个顶点被激活时，在p的末尾增加一个新的顶点v n +1.HMSCH =（N，B，vI，vT，μ，E）的操作语义通过使用上述用于将HMSC简化为MSC图的构造来获得。我们省略了细节，因为没有涉及概念上命题3.11线性时间和上面给出的HMSC的操作语义由线性时间语义定义的游程集合与用于操作语义的标记转移系统的迹集合相同。✷3.3HMSCs的模拟我们已经建立了一个原型工具，用于模拟的HMSC，直接实施的HMSC的操作语义上面提出的。由于空间的限制，我们目前只有一个简短的轮廓的模拟算法。细节可以在[3]中找到。基本MSC的模拟将与第3.1节中定义的MSC m相对应的优先关系R m作为输入。该算法本质上是对这种关系进行拓扑排序，其中每个阶段的最小元素表示启用的事件。只要有多个最小元素，用户就可以选择接下来执行哪个事件当事件被执行时，它将从事件集中删除。当MSC中的所有事件都已执行时，算法停止。用于模拟HMSC的算法进行HMSC的嵌套遍历。10}--对应的有向图，从起始顶点开始它开始模拟图中第一个可到达的基本MSC，并在执行实例上的最大事件时向其添加新MSC。这对应于对应于HMSC的标记跃迁系统中的τ跃迁每当HMSC图中存在分支时，系统都会提示用户选择要考虑执行的下一个HMSC节点到达结束顶点时，模拟结束4基本MSC4.1方法当通过场景捕获需求时，需求工程师通常对验证集合S = M1，.感兴趣，Mn的基础MSC。模拟的一种替代方案是允许用户陈述S中的MSC应该遵守的属性，并自动验证它们，这对于大的n可能是不切实际的问题是定义一个验证算法，该算法将基本MSC的集合S和属性的语句P（在某些定义良好的语法中）作为输入，如果集合S满足属性P，则返回yes，否则返回no（如果需要，还可以提供反例）。在下面的演示中，为了简单起见，我们假设S由单个基本MSCm组成。下面提出的技术可以容易地扩展到处理n个基本MSC的一般情况HMSC的扩展正在研究中。在选择用于指定属性的符号时，需要在易用性和表达能力之间进行权衡。在[9]之后，我们假设属性属于各种类型的预定义模板，因此为了便于使用和验证的效率而牺牲了通用性。这些属性是根据输入MSC的轨迹中事件的相对顺序来陈述的虽然属性模板不能表达实际上可能感兴趣的所有此外，设计有效的算法来验证使用这些模板陈述的属性是可能的我们提出了属性模板的语法和简单的图论算法（基于MSC的偏序语义）来验证这些属性。MSC中的每个事件都有一个由其位置给出的唯一ID，如第3.1节所示。一般来说，用户定义的事件对应于一组内部事件。例如，在图3中，用户定义的事件我们假设属性是根据用户定义的事件及其否定来指定的我们说用户定义的事件e在任何与之对应的内部事件发生时发生。由于用户定义的事件e代表非空集合，S ={e1，...，e k}的内部事件，否定事件not（e）代表事件not（e1）. not（ek）.11≤≤e8 =接收（P2，NA，double）e6 = receive（P2，UR，double）e4 =接收（P1，NA，inc）e3 = send（P1，NA，inc）e7 = send（P2，NA，double）e2 = receive（P1，UR，inc）e1 = send（P1，UR，inc）e5 = send（P2，UR，double）图三. MSC和相关的部分订单4.2属性模板4.2.1追踪跟踪属性断言在输入MSCm的所有或部分跟踪中以指定顺序发生的事件序列。属性的模板如下所示用斜线分隔的粗体术语是选项，用户必须选择其中一个。这里，每个ai，1i n，要么是用户定义的事件（即内部事件的非空集合），要么是它的否定1。子序列/压缩子序列事件[a1，. ，an]发生在开始/在最后/某处曾经/总是/从未这个模板实际上对应于几种可能的模式，具体取决于所选择的选项，如下所述我们还根据与给定MSCm对应的偏序的线性化来定义这些模式中的每一个的语义。例如，在图3中，1为了简单起见，当打包的子序列（即，连续子序列）选项被选择。 同样，当选择开始或结束选项时，序列中的第一个事件不应该是负面事件。核控制P1 UR NAP2IncInc双双12属性声明有可能（在至少一个线性化中）接收由两条inc消息的回执组成的双消息。子序列事件[”NA receives发生某处史以来当引号中的用户定义事件被相关的内部事件集替换时，此属性语句转换为以下模式。事件的子序列[{e2}，{e6}，{e4}]发生在某处史以来显然，这个属性是真的，至少有一个线性化- 例如，，其中事件序列[e2，e 6，e 4]作为子序列出现。作为另一个例子，在图3中，下面的属性声明可以发送两个inc消息，而不需要在其间发送任何double消息。子序列事件[”p1 sends发生某处史以来当引号中的用户定义事件被相关的内部事件集替换时，此属性语句转换为以下模式。子序列事件[{e1，e3}，not（{e5，e7}），{e1，e3}]发生某处史以来4.2.2后果另一种常见且有用的属性，称为consequence，使用以下模板指定。13⊆∈子序列/打包子序列/[每个/所有/一个]事件，X导致子序列/压缩子序列/[an/all]事件，来自Y这里X、Y和E是用户指定的事件集（如果选择了子序列选项，则X和/或Y是该模板对应于几种可能的模式，用于检查某些操作在其优先级发生时是否例如，consequence属性可以用来说明，每当一个进程（UR或NA）收到inc消息时，它随后就会收到一个double消息。有一个相反的优先级属性模板，它断言如果X已经发生，那么Y必须在该运行中先前发生。4.3属性模板每个模板对应于几个模式，这取决于用户选择的这些模式的语义是根据MSC的线性时间语义我们还定义了检查这些属性模式的算法我们举例说明了这个过程的一些跟踪和后果属性模板的pat-schedule回想一下3.1节，Rm是与MSCm相关联的优先关系。我们写当n（ai，aj）时，p=（ai，aj）Rm的过渡闭包. 以下是下面的算法假设传递闭包已经被预先计算。时间复杂度为了简单起见，下面我们假设（i）每个事件ai都是一个内部事件（不是用户定义的事件），（ii）没有一个事件ai是负面事件。 处理用户定义和负面事件的一般算法在全文[3]中描述。(i) 预处理模式：ventsα=[a1，. 永远不会在某个地方发生。意义：是否存在Rm的至少一个线性化σ使得α是σ的子序列？(ii) 预处理模式：ventsα=[a1，. ，一个永远不会发生的地方。意义：α是Rm的每个线性化σ的部分序列吗？(iii) 预处理模式：ventsα=[a1，. 永远不会在某处发生。意义：是否不存在Rm的线性化σ使得α是σ的子序列？以下算法可用于检查属性模式（1）。可以很容易地修改al-xim，以输出包含α作为子序列的实际线性化14∈ ≤≤∈ ≤≤算法跟踪a输入集合E ={e1，...，e n}的MSC m中的所有可能事件，n≥ 1E上的输入二进制优先关系Rm输入α=[α1，. ，ak]agivennon-emptyfinitesequenceofevenets使得对于所有的1i k，ai E，并且在α中没有重复如果至少有一个线性化包含α作为子序列，则输出true;否则为false对于（j=2;j<=k;j++）对于（i= 1;ij;i++）if（precedes（aj，ai））returnfalse;return true;该算法的正确性来自以下观察。命题4.1设E是包含n个元素的有限非空集，R是E上的优先关系。 则E中的两个元素a1，a2在R的某种线性化中出现（按此顺序）当且仅当a2不先于a1。在与（1）相同的假设下，可以使用以下算法来检查属性模式（2）算法跟踪b输入集合E ={e1，...，e n}的所有可能事件的MSC m，n≥ 1E上的输入二进制优先关系Rm输入α=[α1，. ，ak]agivennon-emptyfinitesequenceofevenets使得对于所有的1i k，ai E，并且在α中没有重复如果所有可能的线性化都包含α作为子序列，则输出true;否则输出falsefor（i=1;ik;i++）if（！precedes（ai，ai+1））returnfalse;return true;该算法的正确性来自以下观察。命题4.2设E是包含n个元素的有限非空集，R是E上的优先关系。 则E中的两个元素a1，a2在R的每个线性化中出现（以该顺序）当且仅当a1在a2之前。这两个算法的复杂度都是O（k2）.结果属性模板还代表几个属性模板，这取决于用户选择的选项我们说明了语义的后果模板的模式之一。属性模式：来自X的事件导致来自Y的所有事件。意思是：对于Rm的每个线性化σ，是否存在一些15⊆| |}||| |x∈X和Y的某个有序置换Y1使得序列x·Y1（由x与Y1连接得到）是σ？下面的算法验证了这个模式指定的属性的结果。演算法推论b输入集合E ={e1，...，在MSC m中的所有可能事件中，n≥ 1E上的输入二进制优先关系Rm输入两个非空集合X，Y E如果来自X的事件在所有可能的线性化中导致来自Y的所有事件，则输出true;否则为falsefor（i = 1; i< = |X|; i ++）{x：=X（i）; //X的第个元素//检查x后面是否有Y的所有元素//在所有线性化中对于（j = 1; j <= |Y|; j ++）如果（！precedes（x，Y（j）then//Y的第j个元素break;//x后面不是Y的所有元素}//结束if（j >Y）then//上面的for循环检查了Y返回true; //x是一个//returnfalse该算法的复杂度为O（XY）。请注意，没有一个算法明确检查所有可能的线性化。其他属性模式的其他算法也以类似的方式定义。5结论基于场景的规范（如MSC）提供了一种直观和可视化的方式来描述需求。由于MSC可以提供一个正式的语义，他们可以进行各种分析。在本文中，我们提出了一个形式化的语义HMSC，在此基础上的模拟和验证工具已经设计。我们的重点是应用这个工具集在需求验证的一部分，工业案例工具。为了将基于MSC的工具集集成到软件开发过程中，必须解决几个问题。首先，它们必须与用例模型集成，用例模型是UML用于需求捕获的流行符号。开发人员在维护用例的场景时面临的挑战之一是需求以及因此用例不断变化，并且很难保持相关MSC同步。敬过度-{16针对这个问题，我们提出设计一个通用的元模型，从这个元模型中，用例和MSC的元模型将作为视图导出这将使维护用例和MSC之间的关系成为可能，从而使一个模型中的更改能够自动反映在另一个模型中此外，模拟算法，属性验证和其他分析方法将在通用元模型级别工作，而不是MSC。在软件开发过程中使用场景的另一个挑战是维护它们与其他动态模型的关系，例如用于描述对象行为的状态MSC和状态机可以被理解为系统的局部视图，分别指定对象间协作和对象内反应行为由于这两种观点不是独立的，因此为了使它们描述一个连贯的系统，它们之间必须保持一种形式上的关系我们建议通过将这些动态视图映射到具有状态结构的标记转换系统的公共语义框架来解决这个问题。这个语义域原则上可以解释系统的所有动态视图，可能具有合适的参数化或变化点，例如，关于转换的并发性或粒度在第3节中给出的MSC的语义是一个特例，它可以被认为是特定于某些参数的公共语义域。我们基于情景的分析算法和工具应被视为迈向上述综合行为建模和分析框架的第一步这将把情景与结构模型和行为模型结合起来，并有助于正向工程6确认感谢S教授。拉梅什对他的讨论和反馈的工作。我们感谢Mathai Joseph教授在整个项目中的指导和鼓励。引用[1] R.作者声明：Dr.消息序列图分析器。软件概念和工具，17（2）：70[2] R. Mr.扬纳卡基斯 消息序列图的模型检验。 第十届国际并发理论会议论文集，CONCURSpringer-Verlag，1999.[3] 普兰达尔巴杜里河Venkatesh和Girish Palshikar。使用消息序列图分析场景的形式化技术。内部报告，TRDDC，2001年。17[4] Grady Booch，James Rumbaugh，和Ivar Jacobson. 统一建模语言用户指南。Addison-Wesley，1998年。[5] W. Damm和D.哈雷尔LSC：将生命注入消息序列图。在FMOODS'99：Proc.Third IFIP Intl. Conf. on Formal Methods for Open Object-Based DistributedSystems，1999.[6] G.J. Holzmann，D.A. Peled和M.H.雷德伯格需求工程设计工具。贝尔实验室技术期刊，第86-95页[7] ITU-T。ITU-T建议Z.120：消息序列图（MSC），1996年4月。[8] Ivar Jacobson ， Magnus Christerson ， Patrik Jonsson ， and GunnarOvergaard. 面向对象软件工程Addison-Wesley/ACM出版社，马萨诸塞州雷丁，一九九二年[9] Wil Janssen，Radu Mateescu，Sjouke Mauw，Peter Fennema，and Petravan der Stappen.管理者的模型检查。在第六届国际SPIN研讨会的程序模型检查的实际方面（图卢兹，法国），1999年9月。[10] 弗拉基米尔 莱文 还有多伦·佩利德 通过模板匹配验证消息序列图。在TAPSOFT（FASE斯普林格。[11] E. Rudolph，J. Grabowski，and P. Graubmann.消息序列图。计算机网络和ISDN系统，28（12）：1629[12] E. Rudolph，J.Grabowski，and P. Graubmann. MSC消息序列图（MSC'96）1996年10月，在第一届分布式系统和通信协议的形式描述技术以及协议规范、测试和验证国际会议（FORTE/PSTV'96）上发表