计算机系统时间特性与消息序列图的时间属性正式验证

理论计算机科学电子笔记130（2005）211-233www.elsevier.com/locate/entcs计算机系统时间特性PauloS'ergioM unizSilva1DepartamentodeEngenhariadeComputacampaignoeSistemasDigitaisEcolaPolit′ecnicadaUniversidadeSapaulo loAv. Prof. LucianoGualberto，trav. 3，n. 15805508-900SaoPauloSPBrazil摘要在计算机系统开发的早期阶段，计算机工程师通常绘制交互图，偶尔用时序约束进行注释，以推理系统行为的规范。这些图表中最流行的一种是消息序列图（MSC）。然而，MSC所描述的预期行为并不总是与其实际行为相对应。为了帮助正式验证他们的实际行为，即他们的时间属性，本文描述了一个时间框架中的基本定时MSC的解释，正式表示，在一个统一的模型中，在这些直观的图表中传达的定性和度量时间信息。该框架在多项式时间内解决了验证问题，并为自动化工具奠定了基础。保留字：系统行为验证，消息序列图，时间推理。1介绍通常，在计算机系统开发的早期，计算机工程师绘制图表来推理他们将构建的计算机系统的行为。例如，当使用用例模型时，从需求的角度来看，软件工程师通常绘制序列图[27]来描述用例事件流的实现，这些事件流显示了域对象之间的交互。序列图基于基本的消息序列图（MSC）工件，MSC工件是一种众所周知的可视化工具，主要用于对系统的行为进行建模，表示1 电子邮件：paulo. poli.usp.br1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.03.012212P.S. Muniz Silva/Electronic Notes in Theoretical Computer Science 130（2005）211事件在系统抽象之间交换，并在[13]2中正式定义。除了实时计算机工程师之外，大多数计算机工程师都没有完成对这些图的时间属性的验证造成这种情况的一个重要事实是，传统的验证和确认工具在面对早期阶段可用的部分信息时没有多大帮助[11]。如何严格验证这些直观图的时间属性？MSC是基于规范的规范，即描述系统组件、用户和环境如何同时工作和交互以提供系统功能，并提供系统预期行为和主要异常的示例[29]。虽然场景规范导致系统行为的部分描述，但当前广泛的实践将其用作行为规范。在MSC的情况下，预期的行为被表达为相互作用的序列场景规范语义有两种基本方法：场景描述作为设计文档，场景描述作为规范[29]。后一种方法在需求的早期阶段更合适，引入了为规范找到适当设计并证明设计满足规范要求的问题[2]。我们感兴趣的是作为规范方法的场景描述，以及基本MSC属性的特定子集，其允许通常表达消息的直观时间顺序-定性观点-并在消息流上显示简单的时间约束[3][13]-定量观点。我们提出了MSC的形式语义，允许在统一的时间视角中验证场景的预期行为和实际行为之间的冲突，它结合了定性和定量的时间观点。本文的主要贡献是对MSC语义的整合定性的时间观点源于这样一个事实，即当直观地陈述和描述问题域事件的行为时，我们通常说：同样重要的是，这类事件持续一定的时间，允许我们说：首先，直观地说，我们将系统行为抽象到这个定性框架中，只有在此之后，我们才尝试分配定量（度量）时间信息，希望不会违反2ITU标准还定义了由基本MSC组成的高级消息序列图（HMSC）。P.S. Muniz Silva/Electronic Notes in Theoretical Computer Science 130（2005）211213定性的时间陈述。直接支持这些定性时间概念的适当时间本体论是Allen艾伦的理论是在所谓的“朴素物理学”及其常识表示的背景下发展起来的，把时间间隔的概念作为一个原始的概念。它在自然语言理解、规划、知识表示和其他人工智能研究领域很受欢迎。Allen的理论是区间上的二元关系的代数，携带定性的时间信息，并允许对这些信息进行形式化的推理。MSC的定性解释是在这样的时间框架内定义的，其中定性时间约束指定配对事件的相对位置。另一方面，MSC的定量解释在成对事件之间放置度量时间界限，表示时间的定量持续时间。我们的解释是基于一个集成模型，该模型将Allen即它们的相互依赖性，这与MSC的大多数语义模型相反，该模型将没有定时分配的MSC的语义与具有定时分配的语义分开。MSC的拟议解释支持其定性和定量时间属性的结果的生成，以这种方式，我们可以正式检查图表中指定的预期行为和实际行为之间的潜在冲突。如果在开发过程的早期执行验证任务（例如，从需求或分析视图），它可以帮助计算机工程师在考虑设计决策之前发现重要的规范错误。最后也是重要的一点是，验证任务是在多项式时间内完成的，所提出的形式化模型为验证工具奠定了基础。相关工作。MSC在过去几年中得到了广泛的研究。目前，MSC的分析趋势采用各种方法：进程代数[20]和各种模型检查[28][2][4][3][5]，仅举几例。研究源自MSC的部分有序事件结构[28] [24]特别感兴趣。然而，这些部分有序的结构不处理度量信息。[5][3]中专门研究了度量信息。[3]定义了基本MSC的扩展以指定时序约束，但是MSC中的竞争条件的分析，即由于其实际语义而违反MSC中事件的预期顺序-定性分析-独立于时序冲突的分析来实现。该模型起源于工具分析器的版本，最终形成了UBET工具[18]，它实现了符合ITU规范的基本MSC的丰富功能[12]。 不幸的是，UBET和其他流行的工具，214P.S. Muniz Silva/Electronic Notes in Theoretical Computer Science 130（2005）211随后的研究（例如MESA [6]，LTSA-MSC [19]，EventStudio [10]等），虽然为MSC和高级MSC的分析提供了复杂的功能，但没有进行竞争条件和时序分析的实际集成分析。3[22]中出现了本提案的基本思想的初步版本在[23]中，我们完全重新制定了这种初步方法，简化了解释，最重要的是，为验证问题提出了一种易于处理的解决方案，克服了前一个模型的复杂性限制。然而，这两个模型都是以Allen的理论为基础的排他性在第2节中，我们给出了基本MSC的适当形式定义。第3、4和5节分别介绍了对定义的MSC的定性、度量和综合解释。第6节描述了两个简单的实验，展示了集成模型的应用，第7节给出了一些结论和我们目前的相关研究。2MSC的定义首先，我们将简要介绍MSC的概述，引用[3]。MSC是一种图形表示，它显示了系统内并发进程抽象之间的消息交换图1（a）示出了对交换的消息扩展了简单度量定时约束的基本MSC每条垂直线都有一个开始和一个结束符号，代表进程或自治代理（P1， P2和P3）。每个水平箭头描述从一个进程发送到另一个进程的消息（a、b和c）。箭头的尾部对应于发送消息的事件，而箭头的头部对应于消息的接收。通信是一对一和异步的，并且控制流在每个进程内从开始符号独立地流到结束符号。在每个过程中，事件在时间上从上到下排序。当所有进程都终止时，系统终止。MSC的行为是发送和接收消息的序列的集合，即，MSC通过进程之间交换消息的顺序来表示预期的行为预期的顺序不一定代表MSC的实际语义。冲突很可能发生。比如说，3事实上，时间分析功能被排除在后来更复杂的UBET版本之外。我们无法使用昂贵的商业工具来分析它们的功能。P.S. Muniz Silva/Electronic Notes in Theoretical Computer Science 130（2005）211215C[1，1]x在yXx后的yP1和P2a [4，5]b [1，2]P3[1，1]Xx与y相遇Xx重叠yy xx在yy期间Xx开始yyy满足−by xy重叠−by x y包含xy由x（一）x完成y x等于yyxXy（b）第（1）款y完成−由xFig. 1. 一个基本的定时MSC和Allen如果我们暂时忽略度量定时约束，则不难看出，对于图1（a）的MSC存在这样的情形，其中在处理P1处，消息c比消息a更早到达，这与预期的顺序相冲突。在图1（a）的MSC中，消息a上的标签[4，5]指定消息交换持续时间的下限和上限。消息a的发送和消息b的发送之间的标签[1，1]指定了这些事件之间的持续时间，模拟了关于进程P2的计算的假设。我们称这种扩展MSC为基本定时MSC，如[12]。另一方面，定性时间直觉可以用Allen的时间结构[ 1 ]来建模以及关于两个事件在时间上的关系的信息的不确定性。时间结构是时间的简单线性模型。原始理论以时间间隔为代表。时间结构的五个公理和一套完整的13个直观的二元关系之间的间隔-艾伦的基本关系-被定义。图1（b）描述了这些关系。我们将定义一个正式的结构，标记为MSC的基本时间，它捕获了基本计时MSC的基本属性我们扩展[23]，[2]4适当地，对于MSC的定时属性的定义和其他细节。定义2.1设P={P1，. ，Pn}是进程的集合，并且M是消息的集合。让标签！（i，j，a）表示事件“进程P i将消息a发送给进程P j“。让标签？（i，j，a）表示事件“进程P j从进程P i接收消息a“。 让标签#（i）表示4在[23]中，我们只考虑了MSC的非定时属性，并基于[2]的定义。y216P.S. Muniz Silva/Electronic Notes in Theoretical Computer Science 130（2005）211=事件 令标签[i，j]、[i，j）、（i，j]和（i，j），其中i，j ∈ {0，1，. ，∞}分别表示可以是关闭、半关闭或打开的MSC事件对之间的度量时间间隔的下限和上限。定义集合L S={！（i，j，a）|i，j∈ {1，. ，n}<$a∈M}的发送标签集L C={？（i，j，a）|i，j∈{1，. ，n}<$a∈M}的接收标签，集合L B={#（i）|i∈ {1，. ，n}}作为事件标签的集合，集合L=LS<$LC<$LBLT的度量时间标签，以及下一个过程事件标签的集合LN（定义如下）。进程P上的基本时间标记MSC定义为：• 事件集合E被划分为发送事件集合S、接收事件集合C和底部事件集合B。• 映射p：E> → {1，...，n}，将每个事件映射到发生该事件的进程。• 发送事件和接收事件之间的双射映射f：S<$→C，将每个发送事件与其对应的接收事件相匹配。• 一种双射映射ne：E<$→E，它将一个过程中的每个事件映射到同一过程中的连续事件。每个流程事件都连接到同一流程中的唯一连续事件这个映射称为下一个进程事件。• 一种映射l：E<$→L，它标记每个事件，使得l（S）<$LS，l（C）<$LC，l（B）<$LB。对于标号的相容性，对所有s∈S，若l（s）=！（i，j，a）则p（s）=i和l（f（s））=？（i，j，a）和p（f（s））=j。同样，对所有b∈B，如果l（b）= #（i），则p（b）=i。• 一个映射h：E×E<$→LN，它标记了每个过程Pi上的每个下一个过程事件。• 映射t：E×E−→LT，它标记映射f和ne，并表示事件之间的度量时间约束请注意，此映射是可选的。对于每个i ∈ {1，. ，n}，则过程的事件存在全序≤iPi，也就是p−1（i）的元素上，使得关系≤。 i∈{1，.，n}≤i <${（s，f（s））|s∈S}是E的偏序。这是偏序称为视觉序。全序≤i表示过程派岛 偏序≤表示MSC的视觉顺序，强制执行“消息不能及时返回”的概念对应于图1的MSC的部分顺序在图1中示出。P.S. Muniz Silva/Electronic Notes in Theoretical Computer Science 130（2005）211217a [4，5]第21页[1，1]？（2，1，a）！（2、1、a）P11图二、图1的MSC的部分顺序图2中，节点是发送、接收和底部事件，边是消息和下一个进程事件。所提出的基本时间标记MSC的解释是在经典的时间模型中实现的，其中时间是线性的，并且时间点以实线解释 时间间隔X被表示为一对时间点（x-，x+），使得x− y−，x+0，3≤！c≤4，3？

下载后可阅读完整内容，剩余1页未读，立即下载