交互扩展状态图——形式规范集成的前沿技术

理论计算机科学电子笔记115（2005）49-57www.elsevier.com/locate/entcs交互扩展状态图GwenSalauêna，1，3 andPascalPoizatb，2aDIS，Universit`adiRomabLaMI，Universit'ed摘要集成形式描述技术是一种很有前途的多方面系统规范化方法。在这种情况下，我们提出了一种形式主义，称为扩展状态图（ESD），结合在一个同构的框架状态图和正式的数据描述语言。我们的目的是在这里，以提高隐式ESD通信机制与通信，这是实现使用同步向量的明确描述。本文还讨论了交互作用图的应用.关键词：形式规范集成，状态图，形式数据类型，同步向量，交互图。1介绍在过去的几年里，系统复杂性的增加使得有必要从不同的方面来描述它们。这种关注点的分离出现在编程（所谓的面向对象的编程）和规范和设计（AOSD）级别。综合形式描述技术的使用和此后的定义是规范这种多方面系统的一种有前途的方法。根据我们在这个问题上所做的几个实验[1]，我们提出了一个综合的形式主义，1电子邮件：salaun@dis.un ir oma 1. It2电子邮件：poizat@lami. uni v-e vr y。fr3这项工作得到意大利研究部在FIRB框架（基础研究基金）下资助的ASTRO项目的部分支助1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.09.02850G. Salaün山口Poizat/Electronic Notes in Theoretical Computer Science 115（2005）49扩展状态图[4]（ESD）。ESD使用形式化和图形化的符号，目的是利用两者的优势：图形符号的用户友好性和可读性，如UML，软件建模的事实标准，以及形式化符号，以实现验证和动画机制[5]。系统的静态和功能方面使用正式的数据描述语言，如代数规范，Z或B.系统的动态方面（事件，行为和通信）使用扩展状态图处理的静态方面的正式datastries描述UML符号在ESD中用于表示事件发送（D2 ^tick（n+1）） 例如，在图1的图D3中），并且ESD集成语义随后建立在此基础上以提出通信约束的灵活机制来表达可能的通信模型。这些约束的表达性已经在[4]中进行了说明，以处理通常的面向对象的异步消息传递通信。然而，这种技术选择并不是理想的。首先，它需要在指定者每次需要特定的通信模型时重新定义通信约束。此外，缺乏使ESD之间的通信模型显式的方法是容易出错的，并且损害了指定模块的重用，因为通信约束将被发现到顺序组件中。为了提高ESD之间的交互手段，我们在这里扩展我们的初步建议与替代和互补的通信机制，nisms，仍然保留了整个综合形式主义的形式一致性：同步向量。还讨论了交互图的使用。两者都以一种简单的方式插入到我们在[4]中给出的ESD语义中。因此，可以直接进行相互作用的说明（无需额外的形式化）。本文的结构如下。在第2节中，我们总结了ESD方法。第3节和第4节讨论我们的扩展建议。最后，我们对这项工作作了总结性评论。2扩展状态图本节提供了对ESD语义的必要了解。我们的方法的更全面的介绍可以在[4]中找到语法. ESD扩展了状态图（如Statecharts或UML）：• 在其中导入正式数据类型模块并声明和键入的数据框G. Salaün山口Poizat/Electronic Notes in Theoretical Computer Science 115（2005）4951在出来D11回来tick（x：2导入LarchSpec NATD31/n：/D1 ^tick（n+1），2导入LarchSpec NATn：天然D21回来tick（x：2导入LarchSpec NATFig. 1. 三个相互作用的ESD• 在转换中，在守卫、接收和动作部分（动作和事件发送）中使用形式数据库（代数术语，Z或B操作）。这在图1中的一个简单示例中进行了说明，其中包含三个交互关系图。从左手边到右手边，粗体标签分别表示：（D1）通过tick事件接收变量x中的自然值，（D2）导入使用Larch规范语言编写的数据描述模块NAT，（D3）在转换的动作部分修改n变量的值及其在数据框中的定义，并通过tick事件将值n+1发送到D2语义 让我们首先注意到，我们的目标不是为状态图的某些特定方言提供形式化的语义（确实存在很多，参见[4]的参考文献）。我们的目标是以一种模块化的方式，用正式的数据库来形式化这种图的扩展，即扩展它们的语义。我们认为，一个假设，这些语义（以下称为基本的）给出了一个操作的方式，使用标记的转换系统（LTS）。我们的语义是使用规则组给出的[4]。前两组（R1和R2）用于类型检查术语，并使用评估机制对其进行解释。R3组用于扩展基本语义，以描述扩展图的各个演化，这是通过使用变量绑定（表示为由E表示）、输入事件队列（Qin，事件到达并存储在其中）和输出事件队列（Qout，表示发送的事件）。 此扩展考虑了可能的值接收和操作。这产生LTS的集合{Di：（S，S0，T）}然后，R4基团用于描述以下化合物中可能的修饰：每个图的队列都是开放系统语义的结果（在输入队列中添加，从输出队列中删除这再次产生集合{Di：（Sopen，S0open，Topen）}，其中，对于每个Di，Topen<$T×E<$×E<$，Ein（resp.Eout）是所有输入事件（分别为输出事件）的Di.作为52G. Salaün山口Poizat/Electronic Notes in Theoretical Computer Science 115（2005）49我接收器我我11nnJ+−开放标签J通常对于LTS，（s，标号，s，E，E）∈ T 表示为s→E+，E− S. 规则给定通信模型约束CC，R5然后构建全局LTS（S，S0，T）由R4的乘积产生，即S=DSopen（Di），S0=<$DS0open（Di），T ={t ∈ <$DTopen（Di）|CC（t）}。例如，CC可以定义为在异步消息传递通信模型中的两个图之间关联合法的开放系统队列修改：l1JlnJCC（s1→E+，E−s1，. ，sn→E+，E−sn）惠sende r∈1.. n，n ∈Dreceivere∈Es−ender，D接收器∈i∈1. nDi∈ E+这种规则（集合）的分离，使人们能够重用特定的规则，并替换或专门化其他规则来处理特定的需求。正是这种模块化使人们能够提出上述规则集的替代方案，并就本文而言，以增强R5。3与同步向量隐式通信策略到组件的替代方案是使用同步向量指定交互，同步向量是表达性的，正式的和可读的（即使只有文本）方式来编写ESD之间的交互。同步向量最初是由Arnold和Nivat提出的[2]并用于例如AltaRica形式主义[3]。Korrigan [7]中定义了这个初始概念的扩展，其中使用时序逻辑公式的高级同步向量使人们能够通过不同的策略来组成自动机语法. 如果在技术上我们使用同步向量，我们的目标是保持良好的可读性，因此在[2，3]基本向量（仅对基本同步通信建模）和Korrigan之间找到一个中间级别，更有表达力，但也更难使用，时间公式。我们vector可以用于对ESD之间的不同同步策略进行建模，例如：• 异步的，面向的，一到n，不同的名称：[a！，ε，b？，ε，c？]• 同步，值传递，one with many：• 同步、值协议、多对多：• 同步，值协商，多对多：<......这是什么？>向量处理同步通信，而[. . [1]处理异步通信。用图表标识预先确定事件-G. Salaün山口Poizat/Electronic Notes in Theoretical Computer Science 115（2005）4953→n⎪⎨n我我限制器（例如，D1.a！，D2.b？D3.c？> ）不需要。对应是通过向量中事件的顺序来获得的。在向量中，关于事件的唯一信息是它们是否被输入（例如e！）或输出（例如，e？） 事件 关于绑定到事件的变量或值的信息由ESD语义的规则R3处理。ε通常与同步向量一起使用，以表示相应的ESD不做任何事情（这将匹配其异步向量只包含一个输出事件。语义通过同步向量的交互的形式化是以这样一种方式进行的，其规则可以取代我们ESD语义中的R5规则。抽搐首先，请记住，全局转换t=（s1L1E+、E−sJ1，.，1 1lnJsn→E+，E−sn）只有在CC为真时才有效（R5）。用向量集V表示。 一个转换对于一组向量是有效的，如果对1成立：CC（t，V）惠函v∈V，t| = v.设type是定义的函数，例如对于任何输入事件e？在向量中，键入（e？）对于任何输出事件e ！，类型（e！）=Eout. 此外，type（ε）=Eε。同步通信的规则是：l1JlnJ（s1→E+，E−s1，.，sn→E+，E− sn）|= 优惠11岁nv，nli=ei（v）iftype（ei）=Ein（a）Qout（si）−Qout（sJi）={ei（v）}iftype（ei）=Eout（b）⎪⎩li=ε∧Qout(si)=Qout(siJ)iftype(ei)=Eε(c)该规则同时处理事件名称和类型，这些类型必须在向量和转换之间匹配，以及值传递。输入事件和ε位于ESD LTS的转换标签中。输出事件则不然，它们被放入队列的输出队列（R3规则），并在通信时被提取（R4规则）。因此，它们对应于对应ESD输出队列Q_out中的源转换状态和目标转换状态之间的差异。 所有输出事件必须在相同的值（v）上达成一致，而输入事件将接收它。这里介绍的规则处理单个值传递，但可以像LOTOS [6]中那样一般化为n个异步通信使用全局转换的E+和E−元素然后获得异步通信的规则，（a）其中ei（v）∈E+和（b）其中ei（v）∈E−。同步的不太严格的版本可以用向量的不太严格的版本来表达。例如，广播通信（即，仅54G. Salaün山口Poizat/Electronic Notes in Theoretical Computer Science 115（2005）49发送者/send（n）tick/n：=n+1tick/n：=n−1tick/n：=n+1IMPORT LarchSpec NATn：天然加法器rec（x：Nat）/resA（x+y）rec（y：Nat）导入LarchSpec NATEvenComput/resE（evenrec（x：导入LarchSpec NAT图二. 三个相互作用的ESD，无隐式通信与所有注册的接收机必须同步的多播通信相反，某些所需的接收机可以真正同步）。应用程序. 我们的例子（图2）是由三个相互作用的diagram组成的：一个发送器发送自然数，一个偶数计算机测试数字是否是偶数，一个加法器添加两个自然数。一个值由发送者同步广播到偶数计算机，然后另一个值被送到加法器。最后，加法的结果被传送到偶数计算机。对应于该示例的 通 信 的 矢 量 ， 其 中 ESD 参 考 顺 序 是 EQUIPMENT 、 EvenComput 、Adder，是：<发！，rec？，rec？>，发送！，ε，rec？>，ε，rec？，resA！>}请注意，这些向量并不意味着交互触发中的任何顺序，只有合法的同步。同步向量的这个缺点可以使用交互图来为了结束本节，让我们强调xCLAP [5]可以计算同步乘积（使用我们的transition相关向量，也可以使用状态相关向量），这是从其前身CLAP [8]恢复的技能。这些表达方式也可以应用于ESD，整个规范（一些扩展状态图和同步向量）可以使用xCLAP模拟功能进行动画化。4使用交互图交互ESD我们在本节中的目标是提供这样的见解，即ESD交互也可以使用交互图来描述（这个术语考虑了它们的方言，如MSC或UML序列图）。我们在图3中描述了我们的三个示例组件（图2）之间可能的相互作用。由于MSC不允许组件同步，G. Salaün山口Poizat/Electronic Notes in Theoretical Computer Science 115（2005）4955--阿鲁内偶数运算加法器CommCommComm图三. MSC与三个ESD的S ={S D1，...，S Dn}S D1S D2 DeSD1−→ SD′1SD2−→ SD′2适用（e）−−−−−→S[SD′1 /SD1，SD′2/SD2]见图4。MSC交互语义对于具有不同名称的事件（这是一个缺点，因为这损害了组件的可重用性级别），图2ESD同步转换应该在XML中重命名。然而，可以表达同步的时间排序（这不是同步向量的情况）。语义 MSC产生不同的CC规则，处理它们定义的不同类型的相互作用。以事件e上的任意两个图D1和D2之间的交互为例（例如事件e上的图D1和D2之间的交互）。CC规则为：CC（（SDi−→SDJi ）i∈1.. n，M）优惠M|={（SDi适用（e））i∈1..n}−→（SDi）i∈1.. n[（SDJi/SDi）i∈1.. 2]，记作E[x/y]，表示一个共同的集合EJ，它等于E用x代替y。CC使用标记为从演绎规则获得的应用的转换。这里的规则如图4所示。至于状态图[4]，我们的目标不是形式化交互图，而是能够在我们的通信约束语义规则的定义中以通用的方式重用它们的不同语义。假设D是所选择的MSC语义的函数，其产生MSC模型的合法转换。在这里，它指出，在分别处于状态SD1和SD2的D1和D2之间，在e上的相互作用是可能的。就通信方案的图形表示和时间排序而言，交互图与同步向量是互补的。然而，不同的相互作用的缺点不同，eeM |= SLi56G. Salaün山口Poizat/Electronic Notes in Theoretical Computer Science 115（2005）49语法语义的问题在于，它们中没有一个处理我们使用同步向量处理的所有不同类型的UML 2.0中提出的序列图在表达性方面更令人满意，但它们还没有完全形式化。5总结发言明确的通信策略提高了集成规范的可重用性水平，因为在顺序组件中不存在特定的通信信息。在本文中，我们提出了扩展机制，明确指定ESD之间的相互作用。我们的同步向量可以表达非常不同的同步策略。交互图的使用表达性较低，但受益于其特定友好的图形表示。相关的工作包括第一过程代数（主要是LOTOS [6]，就集成规范而言）。然而，它们的隐式同步策略通常很难理解（例如进程结束时的隐式同步，δ）。此外，由于我们的同步向量插在我们现有的ESD语义之上，我们可以表达同步和异步通信，或者m个进程中n个进程的同步，这不是LOTOS的情况。更接近我们的方法是ISM [9]。ISM是高级输入/输出自动机，具有与ESD相同的表现力，但结构有显著改进。然而，ISM之间的通信比我们的通信更受限制，因为只有异步总线通信可用。这项工作的前景是双重的。第一个方向是将我们的方法推广到一个框架，该框架支持一般（和通用）方法来指定动态规范模块之间的从某种意义上说，这需要我们的第二个观点是使用这里开发的思想扩展xCLAP工具包[5]动画和验证方法（xCLAP本身是CLAP [8]工具的扩展，该工具处理更简单的规范语言）。引用[1] Allemand，M. 、C. Attlogb'e，P. Poizat，J. -C. 罗伊和G。Salaun？n，SHE29比36[2] Arnold，A.，“Finite Transition Systems,” Prentice-Hall,G. Salaün山口Poizat/Electronic Notes in Theoretical Computer Science 115（2005）4957[3] Arnold ， A. ， G. Point ， A. Gri Pastaault 和 A. Rauzy ， The AltaRica Formalism forDescribing Concurrent Systems，Fundamenta Informatica40（1999），pp. 109-124[4] Att iogb'e，C. ，P. 波伊扎塔和G。 S alau？n，InegrationofForm alDatatatypesinStateDiagrams，in： M.Pezz`e ， editor ， InternationalConferenceonFundamentalApproachestoSoftwareEngineering，LNCS2621（2003），pp.341-355[5] Auverlot，A. 、C. Cailler，M. Coriton，V. 我是Gruet和M。 No？el，xCLAP：一种基于形式数据的结构图的方法，硕士学位项目，南特大学。可查阅http：//www. 迪斯 uniroma1.it/salaun/xCLAP/（2003），由C. Attlogb'eanddG. 我来了[6] Bolognesi，T.和E. Brinksma，ISO规范语言LOTOS，在：P. H. J. van Eijk，C. A. Vissers和M. Diaz，editors，The Formal Description Technique LOTOS，Elsevier Science Publishers North-Holland，1989 pp. 23比73[7] Choppy ， C. ， P. Poizat 和 J.- C. Royer ， A Global Semantics for Views ， in ： T. Rus ，editor，International Conference on Algebras Methodology And Software Technology，LNCS1816（2000），pp.165-180[8] Choppy，C.，P. Poizat和J.- C. Royer，The Korrigan Environment，Journal of UniversalComputer Science7（2001），pp. 十九比三十六[9] Oheimb，D. v.的， 交互状态机：一种有状态的方法来证明安全性，在：A. Abdallah，P. Ryan和S. Schneider，editors，International Conference on Formal Aspects ofSecurity，LNCS2629（2002），pp. 15比32