用例和任务模型：缩小软件工程和用户界面设计概念差距的集成方法

理论计算机科学电子笔记183（2007）73-88www.elsevier.com/locate/entcs面向用例和任务模型Daniel Sinnig，a，1，2Patrice Chalina，3 和FerhatKhendekb，4康考迪亚大学加拿大蒙特利尔b康考迪亚大学加拿大蒙特利尔摘要用例是功能需求文档的选择标记法，而任务模型被用作用户界面设计的起点。在本文中，我们激励需要一个集成的开发方法，以缩小软件工程和用户界面设计之间存在的概念差距。 一个先决条件是定义一个共同的语义框架。 相对为了定义合适的语义域，我们讨论了核心要求并回顾了相关工作。提出了一种基于偏序集的初步方法。提出了从CTT任务模型和用例图到上述形式化的映射保留字：用例、任务模型、场景、语义、偏序集1引言不幸的是，在目前的实践中，功能需求规范和UI设计既不协调也不协调。而不是有一个独特的过程，其中UI设计遵循从功能需求规范的逻辑进展特别是，已经注意到大多数UI设计方法没有很好地与标准软件工程实践相结合[23]。事实上，UI设计和功能需求的工程通常由不同的人按照不同的流程进行1 这项工作得到了加拿大国家科学和工程研究委员会的部分支持。2 电子邮件：d sinnig@encs.concordia.ca3 电子邮件地址：chalin@encs.concordia.ca4 电子邮件地址：khendek@ece.concordia.ca1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.01.06274D. Sinnig等人/理论计算机科学电子笔记183（2007）73软件工程和UI开发之间存在着相对较大的概念鸿沟，这两个学科都有自己的模型、生命周期和理论。以下两个问题直接导致这种缺乏一体化：• 独立开发UI相关模型和软件工程模型忽略了现有的重叠，产生冗余并增加了维护开销。• 在生命周期结束时，从UI相关模型和软件工程模型推导实现是有问题的，因为这两个过程不是从相同的规范开始的，因此可能导致设计不一致在本文中，我们提出了一个正在进行的研究项目，其主要目标是：弥合软件工程和UI设计之间的概念差距正式集成用例和任务模型的初步结果。虽然用例是功能需求文档的首选方法[4]，但UI设计通常从识别用户任务和环境需求开始[20]。尽管如此，用例和任务模型有许多相似之处。我们证明了这一点（部分）由一个共同的语义框架，这两个模型的介绍本文件其余部分的结构如下。第2节对我们的框架进行了在第3节中，我们回顾并比较了用例和任务模型。第4节讨论了与基于符号的语义定义相关的工作。在本节中，我们还将概述通用语义模型的核心需求，并介绍我们的方法。我们在第5节中总结并展望了未来的工作。2总体框架我们的总体研究目标是定义一种集成方法，用于在整个软件工程过程中开发用例和任务模型。该计划的一个关键目标是定义一个正式的框架，用于在需求和设计级别处理用例和任务模型。这样一个正式框架的基石是两种符号的公共语义域。公共语义域是满足关系的形式定义的基本基础。这种关系允许我们在用例和任务模型的连续细化之间建立（形式上的）语义链接。理想情况下，改进和满意度证明将得到支持验证的工具的帮助。这些工具通常遵循两种主要方法：自动验证（即模型检查，自动定理证明）和手动验证（交互式定理证明）。但即使没有工具，满意度关系的非正式应用也可以作为识别工件之间简单可追溯性链接（如软件工程中通常所做的那样）的严格基础图1可视化了我们的想法，即具有一个通用的满意度概念，它同样适用于类似性质的工件（例如两个用例）之间，就像它适用于D. Sinnig等人/理论计算机科学电子笔记183（2007）7375图1.一、在正式框架中关联用例和任务模型用例和任务模型。3背景在本节中，我们提醒读者用例和任务模型的关键特征。对于每一个符号，我们提供定义和一个说明性的例子。最后，这两种符号进行了比较，主要的共性和差异进行了对比。3.1用例模型用例是由Jacobson在大约15年前引入的。他将用例定义为“通过使用某些功能来使用系统的特定方式”[ 8 ]。Cockburn [4]经常将最近的用例普及归因于此。用例建模逐渐进入主流实践，将其视为软件开发过程中的关键活动（例如Rational统一过程），因此，有越来越多的证据表明它对客户和开发人员有显著的好处[14]。用例捕获参与者和开发中的系统之间的交互。它被组织成一个相关的成功和失败场景的集合，这些场景都与主要参与者的同一目标相关联[11]。用例通常被用作捕获功能需求的规范技术。它们记录了大多数软件和系统需求，76D. Sinnig等人/理论计算机科学电子笔记183（2007）73图二. “订购产品”的用例示例利益相关者之间的契约（设想的系统行为）[4]。在当前的实践中，用例被提升为用散文语言编写的结构化文本构造。虽然叙事语言的使用使得用例建模成为促进涉众之间的沟通的吸引人的工具，但散文语言众所周知易于产生歧义，并且几乎没有为高级工具支持留下空间。作为一个用例的具体示例，图2给出了一个详细的用户目标级别的用例，用于一个用例以包含用例的各种属性的“header”部分开始一个用例的核心部分是它的主要成功场景，它紧随在标题之后。主要的成功场景由用户和系统之间的一系列交互步骤组成交互步骤指示主要参与者可以通过使用系统来达到他/她的目标的最常见的方式。通过指定用例扩展来完成用例。这些扩展构成了可能会也可能不会导致用例目标实现的替代场景。它们代表了替代（有时是例外）行为（相对于主要的成功场景），并且对于捕获完整的系统行为是必不可少的每个扩展都以一个条件（相对于D. Sinnig等人/理论计算机科学电子笔记183（2007）7377图三. “Order Product” Task主成功场景），这使得扩展相关，并导致主场景“分支”到备选场景。条件之后是一系列行动步骤，这可能导致用例目标的实现或放弃和/或进一步的扩展。从需求的角度来看，用例扩展的穷举建模是一种有效的需求获取方法。3.2任务模型用户任务建模现在是一个很好理解的技术，支持以用户为中心的UI设计[18]。在大多数UI开发方法中，任务集是UI设计阶段的主要输入用户任务模型描述用户使用应用程序执行的任务大多数任务建模方法的起源可以追溯到活动理论[10]，其中人类操作员执行活动来改变部分环境（工件），以实现特定目标[5]。像用例一样，任务模型描述用户与系统的交互。 任务模型的主要目的是系统地捕捉用户在与系统交互时实现目标的方式[24]。不同的任务模型存在，从叙述性任务描述，工作流程图正式分层任务描述。图3显示了用户任务模型的适配ConcurTaskTreesEnvironment（CTTE）[16]可视化。CTTE是一个图形化建模和分析ConcurTaskTrees（CTT）模型的工具[17]。该图说明了“订购产品”功能中涉及的任务之间的层次分解和时间关系更确切地说，所描绘的任务模型指定用户如何利用系统来实现他/她的目标，但也指示系统如何支持用户任务。任务类型的指示由用于表示任务的符号给出任务模型是有组织的78D. Sinnig等人/理论计算机科学电子笔记183（2007）73有向图。任务被分层分解为子任务和原子操作。叶任务也称为操作，因为它们是由用户或系统实际执行的任务。任务的执行顺序由在对等任务之间定义的时态运算符各种时间操作-有很多的erator，最流行的是：enabling（>>），choice（[]），concurrency（||），禁用（[>]）。CTT算子的完整列表及其解释的定义可以在[17]中找到。我们注意到，在任务“显示购买摘要”和“显示缺货”之间以及在任务“显示确认”和“显示付款错误”之间使用的二元时态运算符不是CTT的一部分。我们已经介绍了运营商作为一个扩展CTT。它被称为中止选择运算符，由符号（[]A）和悬停在其右操作数上的STOP符号表示。Abort Choice操作符的解释与内置的Choice操作符类似，在这个意义上，要么执行第一个操作数指定的任务，要么执行第二个操作数指定的任务。然而，在执行第二个操作符之后，模型的所有任务都被禁用。因此，不能执行更多的任务，场景结束。引入这个时态操作符的主要动机是，如果没有它，我们就无法方便地将“OrderProduct”用例中指定的流程特别有问题的是用例步骤过早地导致终止。在CTT任务模型中模拟这样一个事件的唯一方法是在任务树中创建几个主要的备选分支。一个分支表示“OrderProduct”完全执行的情况，而其他分支表示任务提前终止的情况。然而，这样的建模会产生大量的重复（因为相同的起始任务会在每个品牌中重复），并且不必要地增加了任务树可视化的复杂性。3.3用例与任务模型的比较在前面的两节中，我们讨论了用例和任务模型的主要特征。在本节中，我们将比较这两种方法，并概述值得注意的差异和共性。用例和任务模型都属于基于XML的标记族，因此可以捕获系统的使用场景集。一方面，用例通过主要的成功场景和任何相应的扩展来指定系统行为。另一方面，任务模型在一个单一的“单片”任务树中指定系统交互。理论上，这两种符号都可以用来描述相同的信息。然而，在实践中，用例主要用于记录功能需求，而任务模型用于描述UI需求/设计细节。从这个角度来看，用例在更高的抽象级别上捕获需求，而任务模型则更加详细。因此，任务模型的原子操作通常是较低级别的UI细节，在用例的上下文中是不相关的（实际上是禁忌的[4]）上面提到的区别在用例和任务模型中很明显。D. Sinnig等人/理论计算机科学电子笔记183（2007）7379作为例子。与“订购产品”用例相比，相应的“订购产品”任务模型具有更多的UI细节，因为它包含与图形UI相关的步骤。例如，任务模型包含处理所选择或输入的值的提交的附加任务（例如，“提交搜索参数”或“提交支付信息”）。这些步骤未在相应用例中指定，因为它们适用于需要额外提交步骤作为数据输入确认的UI。此外，一些用例步骤（用例的最小可能单元）已经被拆分为任务模型中更小的操作任务。例如，用例步骤2对应于一个连接的用户活动，但是需要由捕获产品类别、系列和品牌的输入的三个UI元素来支持。然而，在许多情况下，用例将包含任务模型中不存在任务模型集中在与UI设计相关的方面，因此，它们的使用场景被严格描述为用户和系统之间的输入输出关系。与次要参与者（在用例模型中指定）的交互被省略，因为它们与UI设计无关。其示例是图2的“订购产品”用例的用例步骤7（4用例和任务模型在本节中，我们首先回顾了用于基于XML的符号的形式主义接下来是对需求的讨论，这些需求需要由用例和任务模型的公共语义框架来解决最后，我们提出了我们建议的语义域，这是基于偏序集。4.1相关工作在基于XML的符号领域中，系统的行为方面（捕获事件的顺序和进展）起着关键作用。虽然已经提出了几个不同的形式主义的基于代数的符号，在下面我们简要讨论三个突出的方法，即：进程代数，偏序集和图结构。进程代数是一种广泛用于定义基于代数的符号的交织语义的形式。在这种方法中，系统的行为由一组（可能并发运行的）进程建模。形式主义本身是作为一种形式演算（定义代数的术语）与相关的“演绎/变换”规则来推理国际电信联盟（ITU）发布了一份基于通信进程代数（ACP）的基本消息序列图（MSC）的正式语义推荐书[2][6]。这项工作是Mauw et首先建立的初步研究的延续。Reniers [13].在最近的工作中，Rui和Butler还提出了一种过程代数语义，80D. Sinnig等人/理论计算机科学电子笔记183（2007）73用例模型，其总体目标是使用例重构形式化[22][25]。在他们的方法中，情景被表示为基本在Rui的提议中，他通过部分适应ITU MSC语义来为特定用例场景（情节）分配意义。此外，语义被定义为相同用例的相关场景以及相关用例。以下用例关系被正式定义：包含，扩展，泛化，继续，相似和等价。适用于非交错语义定义的形式主义是基于偏序的。例如，Zheng et.等人提出了基于定时标记偏序集（lposets）[26]的定时MSC 2000 [7]的非交织语义。Partialorder semantics for（regular，un-timed）MSC已经由Bennyr提出[1]和Katoen和Lambert [9]。巴特尔等等人提出了MSC子集的语义，其仅允许消息事件作为可能的MSC事件类型。相比之下，Katoen和Lambert的语义更完整。 他们将MSC映射到一组偏序多集（pomsets）。一个pomset是一个对应的lposet的所谓同构类。 一个pomset包含所有可以从一个基本lposet通过双射投影导出的对象。基于pomsets的方法与基于lposets的方法米祖尼等al.提出用例图作为用例的中间符号[15]。用例图是有向的，潜在的循环图，其边表示用例动作，节点表示系统状态。这允许对要执行的动作的顺序的自然表示。为了将多个用例集成到一个规范中，Mizouni et.描述了一种用于将一组（相关的）用例图（每个表示一个用例）转换为扩展有限状态机（EFSM）的算法。图的合并是基于用例规范中的常见状态完成的本文提出的语义定义最初受到Zheng等人提出的lposet方法的启发。此外，类似于Mizouni et.例如，我们采用用例图作为用例的中间符号。在我们介绍我们的方法之前，我们讨论一些核心需求，这些需求需要通过任何形式化来解决，这些形式化将用于对用例和任务模型进行建模。4.2语义框架在第3节中，我们回顾了用例和任务模型的关键特征，并讨论了它们当前（和专门）的应用领域。在本节中，我们将重新考虑这些信息，以便为用例和任务模型编译一组特定于任何公共语义框架的需求。这两种符号都用于指定指示如何使用系统的场景。从技术上讲，一个场景由一系列可能无限的事件组成因此，我们要求用例和任务模型的语义模型正式地捕获使用场景集。应该可以从正式规范中机械地提取有效的使用场景。此外，给定一个规格和一个场景，应该可以明确地决定该场景是否有效，D. Sinnig等人/理论计算机科学电子笔记183（2007）7381相对于给定的规格。在任务建模（例如CTT）中，人们经常区分不同的任务类型。例如：“数据输入”、“数据输出”、“编辑”、“修改”或“提交”。在相应的语义模型中，事件也应该通过它们的类型来区分。基于分型，可以进一步约束事件的排序。这种约束的一个例子是表示信息输入的事件（“数据输入”）必须在提交完全相同的数据的事件（“提交”）之前。在我们在4.1节中调查的形式主义中，基于标记偏序集形式主义的方法也区分了MSC运行期间可能发生的不同类型的事件。(In特别地，标记功能的目的是为每个MSC事件分配类型在用例建模中，状态条件经常约束用例步骤的执行。例如，一个用例的pre-condition属性表示该用例将被执行的一组此外，每个用例扩展都由一个条件触发，该条件必须在扩展中定义的步骤执行之前保持。为了能够评估条件，语义模型必须提供捕获状态概念的方法，并且应该能够将状态条件映射到事件的外观到目前为止，我们已经将语义模型的需求绑定到用例和任务模型的内在特征上。然而，下一个需求与软件开发过程更紧密地相关，用例和任务模型将在该过程中被精心制作。软件开发过程的一种观点是作为一系列的“规程”，在此期间，模型被迭代地转换/细化，直到达到实现级别。用例和任务建模是这样一个生命周期的因此，一个通用的语义模型应该很容易支持细化。最后一个要求与并发模型的选择直接相关。在交错模型中，真正并发的概念被省略，并发系统行为被认为等同于所有可能的（交错的）顺序执行的非确定性选择。事实证明，交织方法通常不支持将事件（或动作）任意细化为子事件（或子动作）。主要原因是，在交错模型中，“交错的确切内容取决于进程中哪些事件是原子的”[ 19 ]。因此，如果一个以前的原子动作被进一步细化，子动作之间的新的交织被引入，这在细化之前没有被考虑。因此，大多数等价关系（例如迹等价和双模拟等价）在任意细化下都不保留[3]。这个问题在非交错并发模型（也称为偏序语义或真并发语义）中不会发生，因为并发的概念系统的行为表示在因果关系相互关联的事件的偏序关系的基础上。没有因果关系的事件被解释为并发事件。82D. Sinnig等人/理论计算机科学电子笔记183（2007）734.3基于偏序集的语义域在本节中，我们将说明一种语义方法，在该方法中，我们将演示CTT任务模型和用例如何映射到偏序集的集合。我们首先重申偏序集（偏序集）的定义，然后定义偏序集上的一些算子。最后，我们将描述定义从用例和任务模型到偏序集集合的映射的4.3.1数学符号（Mathematical Notation）定义4.1就我们的目的而言，偏序集（偏序集）是一个元组（E，≤）得双曲余切值.E：是一组事件，≤E×E：是定义在E上的偏序关系（自反、反对称、传递）。这种关系规定了事件的偶然顺序。为了能够组合偏序集，我们定义了以下操作：定义4.2二元运算：顺序复合（. ）和平行组合（||两个偏序集p和q的）定义为next。注意，R表示R的自反传递闭包。设p=（Ep，≤p）且q=（Eq，≤q），其中Ep<$Eq=<$，则：p. q=（Ep<$Eq，（≤p <$≤q <${（ep，eq）|ep∈Epandeq∈Eq}）<$）p||q =（Ep<$Eq，≤p <$≤q）在我们的方法中，我们使用以下偏序集上的操作来定义4.3对于两组偏序集P和Q，序列复合（. ）、平行组合（||）和替代成分（#）的定义如下：P.Q ={pi.qj|pi∈P和qj∈Q}P||Q={pi||QJ|pi∈Pandqj∈Q}P #Q = P<$Q我们的模型的另一个基础是跟踪的概念。然后我们定义一个给定偏序集和一个给定偏序集的迹定义4.4偏序集p=（E，≤）的迹t被定义为来自E的事件的（可能无限的）序列，使得n（i，j在t的索引集中）。 i >t2）= M <$t1）. M <$t2）//使能Mt1||t2）= M <$t1）||M<$t2）//并发执行M <$t1[]t2）=M <$t1）#M <$t2）//选择Mt1|+的|t2）=（M <$t1）. M <$t2））#（M <$t2）. M<$t1））//阶独立性M<$topt）=M<$t）#（n，n）//optinalexecutionM <$t）={（，），M<$t），（M<$t）. M<$t）），（M<$t）. Mt）。M<$t）），. }//itetion注 意 ， 如 果 CTT 任 务 表 达 式 包 含 时 态 运 算 符 Disabling （ [> ） 、Suspend/Resume（|>）或新引入的操作符Abort Choice（[] A），它需要被转换为不涉及84D. Sinnig等人/理论计算机科学电子笔记183（2007）73见图4。 “Search”这些操作符，在应用映射函数之前。一个简单的示例说明了如何将“搜索”任务的任务模型为了执行搜索，用户首先输入搜索字符串。接下来，用户或者直接提交搜索参数，或者进一步细化搜索标准。“细化”任务由“选择类别”任务和“选择子类别”任务的顺序执行组成，并且可以在任何时候通过执行“提交”任务来中断（和禁用）。我们使用了二进制禁用（[>）操作符来指定所需的行为。运算符的含义定义如下：由其操作数指定的两个任务同时启用。一旦第二个操作数指定的第一个（子）任务（在本例中为从任务模型中，我们可以推导出以下任务表达式：t1>>（（t2>> t3）[> t4）注意，各种任务通过使用标识符（t1，t2，t3，t4）来表示。接下来，我们必须将任务表达式转换为等效的任务表达式，它不使用禁用操作符。这可以通过检查可以从规范中提取的一组可能的场景来完成在我们的示例中，我们可以在以下三种场景中进行选择(i) 用户输入并提交搜索字符串（t1>>t4）。(ii) 用户输入搜索字符串，选择一个类别，然后提交搜索参数（t1>>t2>>t4）。(iii) 用户输入搜索字符串并在提交之前选择一个类别以及一个子类别（t1>> t2>>t3>> t4）。因此，任务表达式可以重写如下：（t1>> t4）[]（t1>> t2>> t4）[]（t1>> t2>> t3>> t4）任务表达式现在是基本形式，因此我们可以应用我们的D. Sinnig等人/理论计算机科学电子笔记183（2007）7385语义功能M.根据其递归定义，应用程序可以分为以下步骤：M <$（t1>>t4）[]（t1>>t2>>t4）[]（t1>>t2>>t3>>t4））=M <$t1>> t4）#M <$t1>> t2>> t4）#M <$t1>> t2>> t3>> t4）= M <$t1）。M<$t1）. Mt2）。M<$t1）. Mt2）。Mt3）。第四阶段）={（{t1，t4}，{（t1，t4）}）}{（{t1，t2，t4}，{（t1，t2），（t2，t4）}）}{（{t1，t2，t3，t4}，{（t1，t2），（t2，t3），（t3，t4）}）}因此，我们得到了一个由三个偏序集组成的集合，其中每个偏序集代表前面讨论过的一个场景。4.3.3将用例转换为偏序集在本节中，我们将讨论如何将用例转换为偏序集的集合转换由两部分组成。首先，文本用例被转换为中间图形式，我们将其称为用例图。接下来，基于用例图迭代地构造对应的偏序集集合定义4.9用例图是一个带标签的迁移系统U=（Q，q0，qf，T）其中，Q是有限状态集q0∈Q是初始状态qf∈Q是最终状态T<$Q×Q是转换关系。类似的工作Mizouni et. al [15]（在4.1节中讨论），标记转换系统的转换表示用例步骤，而节点表示状态。来自实际用例的用例图的组成取决于用例中隐含或显式包含的流程构造。这样的流程构造的示例是：跳转（例如，在步骤X）、排序信息（例如，用例步骤的编号），或者分支到用例扩展。需要注意的是，如果用例是以纯粹的叙述形式捕获的，那么用例图的推导将是一个手动活动。在用例图的基础上构造了一组偏序集。构造可以通过以下两个步骤机械地执行：首先，我们为用例图中的每个转换通常，偏序集的集合由单个偏序集组成，而偏序集又定义了一个表示相应用例步骤执行的单个事件其次，用例图被迭代地转换为仅由初始状态和最终状态组成的标记转换系统。在每次迭代中，用例图的一个节点被删除，并且在其传入节点和传出节点之间定义一个新的转换。与第一步类似，一组偏序集被分配给新插入的变迁。86D. Sinnig等人/理论计算机科学电子笔记183（2007）73这个偏序集集合是附加到传入转换和传出转换的偏序集集合的合成的结果。此时，它不再表示单个用例步骤，而是用例步骤的组合。如果被删除的节点包含一个自循环，或者如果已经存在从传入节点到传出节点的转换，则一旦图仅由初始和最终状态组成，则与两个状态之间的转换相关联的偏序集的集合表示表示原始用例图的偏序集的集合。我们注意到，所提出的算法的主要思想源于众所周知的算法，该算法将确定性有限自动机（DFA）转换为等价的正则表达式。然而，我们不是逐步组合正则表达式，而是组合偏序集的集合。我们建议读者参考[12]以了解更多细节。在下一节和最后一节中，我们总结了本文的主要思想所提出的语义域与我们列举的要求有关，并对未来的途径进行了展望。5结论和今后的工作在本文中，我们强调了开发用例和任务模型的集成方法的必要性这种方法将建立在一个共同的语义框架之上。从理论上讲，这两种符号都可以用来描述相同的信息。然而，在实践中，用例主要用于记录功能需求，而任务模型用于描述UI需求和设计决策。关于语义框架的定义，我们回顾了相关的工作和形式主义。基于用例和任务模型的内在特征，我们编制了一个列表，列出了任何正式框架都应该满足的四个核心需求：（1）捕获使用场景集，（2）区分不同的事件类型，（3）捕获状态的概念，以及（4）支持事件细化。然后，我们介绍了我们的初始方法，该方法将用例和任务模型映射到偏序集。到目前为止，本文所提出的偏序集形式主义只满足第一个和最后一个有效的事件序列通过使用偏序关系关联事件来指定。一个场景被称为是有效的，如果一个迹可以从相应的偏序集中提取类似的事件序列的场景关于支持事件精化的要求，我们使用偏序集形式主义来指定非交织语义，这自然支持精化[3]。作为今后的工作，我们将处理剩下的两个要求。例如，支持不同事件类型的要求可以通过定义一个标签函数来解决，该函数将事件类型映射到偏序集的每个元素此外，需要引入进一步限制有效跟踪定义的规则。这样的规则的示例可以是数据输入类型的事件必须总是由提交类型的对应事件跟随的条件。以与标记函数将类型分配给事件相同的方式，可以使用类似的函数D. Sinnig等人/理论计算机科学电子笔记183（2007）7387定义为将状态条件与事件的发生相关联。例如：事件执行可以以满足前置条件为条件;此外，事件执行可以导致满足某个后置条件的状态另一个未来的途径涉及用例和任务模型规范的满足关系的定义。关于所使用的形式主义的可满足性的自然定义可以通过细化来表述。在本文中，我们正式定义了基于迹包含的两个偏序集之间的加细在这种情况下，一个规范满足另一个规范，如果前一个规范的偏序集的对应集合是表示后一个规范的偏序集的集合的精化我们的持续工作旨在进一步研究合适满意度关系的定义，但亦专注于实际验证过程的工具支持。引用[1] 巴尔河，G. Holzmann和D.Peled，An Analyzer for Message Sequence Charts，in Proc. TACAS'96，（1996）pp. 35-48号。[2] Baeten ， J. ， 和 W.Weijland ， Process Algebra ， Cambridge Tracts in Theoretical ComputerScience18。剑桥大学出版社，剑桥（1990年）。[3] 卡斯特拉诺湖和G. de Michelis，Concurrency vs. interleaving：introductive example. EATCS公报，31，二月，（1987）第12-25页。[4] Cockburn，A.，编写有效的用例，Addison-Wesley，（2001）。[5] Dittmar ， A. P. Forbrig ， Higher-Order Task Models ， Proceedings of Design ， Specification andVerification of Interactive Systems，2003。[6] ITU-T，建议Z.120-信息顺序图，日内瓦，1996年。[7] ITU-T，建议Z.120-信息顺序图，日内瓦，1999年。[8] 雅各布森岛，P. Jonsson，M. Christerson和G.面向对象的软件工程-用例驱动方法，Addison WesleyLongman，Upper Saddle River，N. J.，一九九二年[9] Katoen，J.和L.Lambert，Pomsets for Message Sequence Charts，in Proc. 1998年的SAM'98[10] Kuutti，K.，活动理论作为人机交互研究的潜在框架。《语境与意识：活动理论与人机交互》，麻省理工学院出版社，1996年。[11]Larman，C.，应用UML和模式：面向对象分析和设计以及统一过程介绍，第二版，Prentice-Hall，2002年。[12] Linz，P.，《形式语言与自动机导论》，Jones & Bartlett出版社，第二版，页。83-86，1997年。[13] Mauw，S.，和硕士李文，一种基于代数语义的基本信息序列图，计算机学报，第37卷，第4期，1994年。[14] 梅 里 克 ·P Barrow ， The Rationality for OO Associations in Use Case Modeling ， In Journal of ObjectTechnology，Vol.4，No.9，2005。[15] 米 祖 尼 河 A. 萨 拉 赫 河 Dssouli 和 B. Parreaux ， Integrating Scenarios with Explicit Loops ， inProceedings of NOTERE 2004，Essaidia Morocco，June 2004.[16] Mori ， G. ， F. Paterno 和 C. Santoro ， CTTE ： Support for Developing and Analyzing Task Models forInteractive System Design，IEEE Transactions on Software Engineering，August 2002，pp. 797-813，2002年。[17] Paterno，F.，基于模型的交互式应用程序设计和评估，Springer，2000年。[18] Paterno，F.，Towards a UML for Interactive Systems，in Proceedings of EHCI 2001，Toronto，Canada，pp. 2001年7月18日88D. Sinnig等人/理论计算机科学电子笔记183（2007）73[19] 普拉特副总裁用偏序建模并发，国际并行编程杂志，15（1），页。33-71，1986年2月。[20] 普雷斯曼河，软件工程-实践者的方法，第6版，Mc Graw Hill，2005年[21] Regnell，B.，M.李国雄，一种基于图形表示的层次化用例模型，北京大学计算机工程学院学报[22] Rui，K.，一个重构用例模型的过程代数语义学，博士论文，Concordia大学，2004年。[23] Seealah，A.，M. Metzger和D.软件和可用性工程：流行的神话，障碍和集成途径。以人为中心的软件工程-在软件开发中集成可用性，Springer，2005年。[24] Souchon，N.，Q. Limbourg和J. Vanderdonckt，在多个使用上下文中的任务建模，在交互系统的设计，规范和验证程序中，罗斯托克，德国，第10页。59-73，2002年。[25] 徐，J，W. Yu，K. Rui和G. Butler，用例重构：工具和案例研究，载于2004年APSEC会议记录，韩国釜山，pp. 484-491.[26] Zheng，T.，F. Khendek和B. Parreaux，Refining Timed MSC，SDL 2003：System Design，LectureNotes in Computer Science，Volume 2708/2003，pp. 234-250