软件组件的描述和交互：使用实时序列图和最小的假设

理论计算机科学电子札记108（2004）83-98www.elsevier.com/locate/entcs生成组件设置Sotiris Moschoyiannis1英国萨里大学计算机系GU2 7XH，英格兰摘要软件组件往往被视为灵丹妙药时，面临着越来越多的软件使用在许多不同的计算领域的挑战。然而，在组件之间的接口处的复杂的“调用相互作用”常常导致病态行为并阻碍有效的重用。很明显，需要一种语言来记录和指定组件，使它们与配置的变化隔离开来。在本文中，我们描述了使用实时序列图（LSC）来描述组件的相互作用。然后，我们提倡一种方法来正式化这些交互，以确保组件正确交互，同时对它们的邻居做出最小的假设。保留字：交互，行为，LSC，向量语义1介绍作为处理现代软件系统不断变化的需求的一种手段，近年来基于敏捷的软件开发受到了相当大的关注。特别是在嵌入式软件的背景下，新产品需要以及时和可定制的方式开发越来越复杂的软件此外，在开发过程中，不仅新产品的配置可能会发生变化，甚至单个产品的配置也可能会发生变化[14]。现代软件系统通常包括现有功能的复杂因此，需要重用软件，1 电子邮件：s. eim.surrey.ac.uk1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.01.01484S. Moschoyiannis/Electronic Notes in Theoretical Computer Science 108（2004）83是由不同的开发人员开发的，在不同的假设下，组件之间的行为往往会发生不一致这对软件组件的再利用提出了进一步的挑战，并强调有必要系统地组织这一活动实现这一目标的流行范例是基于组件的设计。组件的系统重用需要组件的接口规范和对组件接口进行兼容性检查的方法。在本文中，我们关注前者。我们描述了使用实时序列图（LSC）[2]来指定组件之间允许的交互，然后，我们提出了一个形式主义捕捉组件的相互作用，关于特定的场景。我们感兴趣的是在组件接口的事件发生建模：在该组件提供的服务被要求的顺序，以及该组件从其他组件请求服务的顺序。我们的建模方法有助于正式的分析和推理组件的相互作用。我们还暗示从组件之间的消息交互中提取基于状态的信息。当考虑快速改变配置以适应新产品或系统时，这一点特别有用本文的组织如下。在第2节中，我们展示了一个来自模拟电视嵌入式软件的示例，并使用通用LSC来捕获与组件的特定配置有关的特定场景。在第3节中扩展了该示例，其中更改了配置以包含新功能。在第4节中，我们提出了一个形式主义的交互组件，支持变化。本文件最后提出了一些结论意见和对今后工作的设想。2模拟横向交流通常，消息序列图（MSC）[16]用于将场景指定为对象或进程之间的消息交互序列。然而，MSC往往不能讲述完整的故事。它们的解释可以是模糊的;例如，MSC描述的是系统的根据ITU标准[16]，MSC只做后者。然后，当所描述的场景实际发生时，在MSC中几乎没有什么可以说的关于系统将做 LSC [2]解决了这些问题，因为它们明确区分了强制行为和可能行为。这是通过向图表的各个部分添加活性来完成的在一个图表中，活的元素，称为热描述强制性的-必须发生的事情.如果使用得当，热元件可以S. Moschoyiannis/Electronic Notes in Theoretical Computer Science 108（2004）8385CB<<组件>>一<<组件>>D一D）的方式(i)（二）Fig. 1. 在（i）中使用UML 2.0和在（ii）描述禁止的行为，即不允许的交互序列。其他元素，称为冷，描述可能的行为-可能发生的事情。它们可用于捕获条件行为和各种形式的迭代。在符号方面，所有热元件以实线/框/六边形指示，而冷元件以虚线/框/六边形指示。在讨论下面的示例时，我们回到LSC构造的符号。在下文中，我们将介绍一个取自模拟电视领域的示例。这个例子基本上是[14]中的例子的一个小版本，但包含了必要的细节，以帮助我们说明我们的方法，捕捉组件之间的交互。在[14]中，作者描述了在消费电子（CE）产品中使用的嵌入式系统中编写控制软件时出现的问题。例如，电视机中的许多控制任务需要协调同一信号路径中的设备，这意味着对硬件拓扑结构的依赖性很强，硬件拓扑结构在新产品中会发生变化，但在同一产品的开发过程中也会发生变化。鉴于这些问题，[14]中采用的方法是允许组件除了垂直控制接口之外还使用水平通信接口进行通信。这个想法是控制各个硬件设备的组件具有输入和输出端口，这些端口镜像硬件并通过这些端口进行通信。在电视机中，一项常见的任务是调谐。当调谐器的频率改变时，它会产生噪声，这可能导致电视屏幕上出现不希望出现的伪影因此，在改变频率之前，电视机的屏幕应该被消隐一旦调谐器调到新的频率，屏幕就可以取消空白（参见[14]）。图1示出了该功能所需的TV平台中的组件的配置，其中组件A是调谐器驱动器，B是控制调谐器的图1（ii）显示了使用Koala com符号的配置，<<组件>>B<<组件>>C86S. Moschoyiannis/Electronic Notes in Theoretical Computer Science 108（2004）83组件模型[15]。Koala的图形符号非常类似于硬件设计。软件组件呈现为IC芯片和接口表示为芯片的引脚。其思想是组件具有输入和输出端口，组件通过这些端口发送和接收信号。连接点上的三角形指定函数调用的方向。图1中的子图（i）使用UML展示了相同的配置，特别是考虑到UML2.0中引入的组件或复合结构图。与UML 1.x相比，在UML 2.0的规范草案中有强烈的迹象表明，关于组件，重点从实现转移到规范。2.1模拟强制性行为我们在这里关心的任务是调音。假设顶层控制软件（图1中未包含）希望更改频率。它在B的控制接口上发出请求tune（f）。为了提供该服务，B要求C放弃其信号。而C则需要D的消隐才能使其信号下降。一旦C确实已经丢弃了其信号，B就可以继续请求调谐器驱动器组件A改变其频率。一旦A完成了这个请求，B就向C发出一个新的请求来恢复它的信号。同样，C需要D取消空白，然后才能完成B.一旦C被恢复，B可以向控制软件组件确认改变频率请求。这就完成了对tune（f）的调用。可以看出，每当调谐器改变频率时，就会发生许多交互。我们使用LSC的符号更详细地说明了这些相互作用 [2]。为了对我们的示例的交互进行建模，我们使用了一个通用的LSC，因为我们想要描述强制行为;必须发生什么。如图2所示，它在其前图（用虚线边界六边形注释;它本质上是一种冷条件）和其主体（用实线边界矩形注释）之间诱导了一种作用-反应关系。在这里，我们假设一个可靠的通信媒介，在这个意义上，没有消息可以丢失。这种观点与CE产品的嵌入式软件此外，所有消息都被认为是同步的，因为在发送和接收消息（发射和吸收信号）之间没有明显的时间流逝。闭合的三角形箭头用于表示同步消息，参见图2。图2所示的图表从一个预图表开始，控制软件在预图表中发出改变B上频率的请求，即LSC上的消息tune（f）。请注意，我们使用一个参与者来表示顶层控制软件。我们想强调的是，顶层控制软件是启动随后的交互的外部实体/实例，但它S. Moschoyiannis/Electronic Notes in Theoretical Computer Science 108（2004）8387调谐dropAckunblankAckrestoreAck更改确认恢复变化（f）增辉f：=fblankAck调谐（f '）*空白下降DCB一图二、用于改变调谐器频率的LSC不参与其中。在控制软件发出调整请求后，进入图表的主体。这由接收到调优请求后B的生命线的实线部分指示组件A、C和D也必须进入图表主体。主体部分从BB请求C丢弃它的信号（LSC上的消息丢弃在C可以丢弃其信号之前，它必须协调其下游设备，即视频输出驱动器组件D。换句话说，它必须请求D的消隐。它通过发送空白来实现。在一段时间之后，D向C发送消隐确认以指示消隐操作的成功完成。只有这样，C才能确认B注意，消息drop、blank、blankAck是同步的，而tune（f）是异步的，如其开放式箭头所示。这意味着在执行调优操作的同时，参与者可以从事其他任务。 这包括在调谐操作仍在进行中的同时，将新的调谐器（fj）fj = fj施加到节点B。事实上，演员或顶级控制软件可以发出多个新的调谐请求。如果在该时段期间（在完成丢弃请求之前）确实发生了新的调谐（fJ），则B必须记住新的频率值，以便将来在change（f）中使用。调谐（fJ）只能在C确认B的丢弃请求之前发生，因此与C和D之间进行的消隐操作同时发生。使用无界循环（由子图表示）对这种情况进行88S. Moschoyiannis/Electronic Notes in Theoretical Computer Science 108（2004）83在左上角有一个“*”）。一个无限循环会永远迭代，并且只有当它内部的冷条件计算为false时才能退出。一般来说，如果冷条件放在循环子图的最开始，那么我们正在建模一个while循环。如果冷条件被放置在循环子图的底部，那么我们正在建模一个do-until循环。在我们的例子中，我们做前者。在图2的LSC中，我们使用冷条件（由Ada sh edhex eg），其中heh如果出现此消息，则冷条件评估为真，并进入循环子图。在循环内部，B更新频率值（赋值操作用一个带锯齿边的矩形进行注释，一种类似于UML中的注释构造的方式）。如果没有出现新的调优（f，J），则忽略循环，继续执行场景，紧接着在循环下面。请注意，循环子图的位置也很重要。一个新的曲调（fJ）只能发生在丢弃消息之后和dropAck消息之前。这是由沿着B的生命线诱导的偏序所强加的。 迭代的次数由新调优请求的出现次数决定，这些请求在删除操作及其“嵌套”操作时发生。消隐操作-仍在进行中。 用更简单的话来说，一个新的曲调（fJ）在B收到dropAck后不能发生。在该点之后的新调优请求被视为场景中不允许的事件序列，并且基本上对应于禁止的行为。我们在下面的小节中进一步讨论这种情况。循环中描述的活动可以与C和D之间的消隐操作同时进行。我们不需要在LSC上显式地表示这种并发，因为循环和消隐操作涉及不同的组件。如果某个组件同时参与了这两个过程，我们可以使用共域表示法（在并发消息周围的垂直虚线）来解释[5]。我们将在第3节回到关于共域的讨论。现在回到这个例子，一旦B从C接收到丢弃确认（dropAck），它就继续（它必须继续，因为它的生命线是稳固的）向A发送改变频率消息。一段时间后，A通过发送changeAck指示更改请求完成。然后B可以向C发出恢复请求。同样，C必须协调其下游设备，因此它请求D的解除消隐。再过一段时间（毫秒量级）后，D确认该去消隐请求。C然后确认B的恢复请求，这完成了控制软件的改变频率请求。电视现在调到新的频率了。请注意，在我们的例子中，引用是非常重要的，S. Moschoyiannis/Electronic Notes in Theoretical Computer Science 108（2004）8389调谐下降空白dropAckF A L S E调谐（f'）f：= fblankAck调谐（f '）*DCB一图3.第三章。删除操作完成后，不能出现新的优化请求钱。与典型的确认相反，它们不仅仅确认消息的接收，而是指示所请求的任务或功能已经完成。我们在这里模拟了在模拟电视领域，确认实际上是对上游设备的向上调用，以指示所请求的操作确实已经完成。上游设备是那些更接近信号源的设备，下游设备是那些更远离信号源的设备（见[14，15]）。2.2禁止行为到目前为止，我们已经描述了使用LSC对组件设置中的强制行为进行建模。使用LSC，也可以描述禁止的行为。也就是说，系统不允许或至少不打算在给定场景中表现出的行为。当我们想要禁止某个通信序列时，我们在LSC的前图中指定这些通信回想一下，如果热条件的计算结果为false，则整个图表将中止，并标记错误LSC [4]中的保留字“repeat”可以用于此目的，因为它使它所处的条件始终评估为false。图3中所示的LSC表明，在drop操作完成后，不能发出新的tune（fJ换句话说，CTuner90S. Moschoyiannis/Electronic Notes in Theoretical Computer Science 108（2004）83调谐restoreAck休息unblankAckunblankAckoreAck增辉更改确认增辉恢复恢复变化（f）dropAckdropAckf：=fblankAckblankAck调谐（f '）*空白空白下降下降FEDCB一见图4。 新配置组件（组件B）在其已经从CTVideo组件（组件C）接收到dropAck之后不接受任何新的调谐（fJ在该LSC中可以看出，所有通信都按照计划进行，直到B接收到最后一个调谐（fJ）。在此消息发生后，主体在热假条件导致立即（和异常）流产的整个图表。从这个意义上说，图3所示的LSC描述了上一节中描述的调优场景的反场景。3更改配置如前所述，硬件中信号流的拓扑结构以及控制单个硬件设备的软件组件的配置可能会因新产品而改变，但在单个产品的开发过程中也会改变。假设新产品具有在原始电视屏幕内显示小屏幕的附加功能。这需要添加画中画（PIP）模块，用于产生被馈送到视频输出处理器的缩小的图像，以使其具有优异的性能。S. Moschoyiannis/Electronic Notes in Theoretical Computer Science 108（2004）8391在现有的图像上。更改调谐器的频率时，PIP输出应被消隐是一项产品要求。PIP采样的图像，并存储在内部存储器之前，调谐器输出可能会下降。与模拟电视中的其他下游设备一样，它实际上需要一些时间来完成此操作。为了适应新的功能，通过添加智能PIP组件E及其相应的PIP驱动器组件F来改变配置。智能元件E应连接到B，以便在进行下料操作时得到通知。通过仔细检查图2的LSC中建模的现有组件交互，可以看出新配置中PIP组件事实上，B以任何顺序向C和E发出丢弃请求这种情况在图4的LSC中使用共区表示。在关于LSC的开创性论文[2]中，共区域对应于图表中事件无序的区域它们在与发送的消息相对应在[5]中，共域被给出了一个真并发的解释：区域中的事件“同时”发生，而不是“以任何顺序”发生在这种情况下，共区域由围绕相应事件的垂直虚线表示在我们的例子中，由于B以任何顺序发出丢弃请求，我们使用[2]意义上的共域。因此，由B发送的丢弃消息周围的垂直虚线。一旦C和E接收到丢弃请求，它们就分别继续请求D和F的消隐。这两个消隐操作同时进行，也可能与循环内的活动同时进行。消隐操作完成后，C和E可以丢弃它们的信号，并将dropAck返回到组件B，如前所述（图2的LSC）。接收对应的丢弃应答的顺序也是不相关的。重要的是，B记录了丢弃请求的数量，并知道期望相同数量的丢弃请求。如图4所示，我们使用一个子图来描述B收到两个丢弃应答后的通信。这具有同步组件B、C和E并且禁止场景的进一步进展的效果，除非B接收到两个丢弃应答。请注意，B子图中发生的事情现在应该很简单了92S. Moschoyiannis/Electronic Notes in Theoretical Computer Science 108（2004）834解释组件交互在本节中，我们提出了我们的方法的基础，对正式组件的相互作用，出现在一个给定的LSC。我们的意图不是给LSC一个正式的语义。这一点在其他地方已经做得很好，例如[2，4，5]。我们建议将LSC视为组件行为模型的起点[7，8，12]。事实上，这里提出的方法已经被[7，8，12]中组件的集合理论框架所取代。这里有几句话是为了澄清一些基本的假设。首先，我们处理同步消息，因此发送事件和接收事件被认为是同时发生的。 这与[4，5]和[14]中同步消息的观点一致，并且确实是我们示例中第二，我们专注于对执行特定任务所需的组件交互进行建模，我们不处理预图或进入预图、退出预图或到达主体结尾的行为。我们关注发送和接收消息的实际系统事件，在[4]中称为可见事件例如，变量f的新频率FJ不被认为是事件。结合未来隐藏的事件应该不难发现。我们首先考虑LSCL的图形，并尝试使用以下定义来捕获其静态特性。设ML是在L中交换的消息的集合。定义4.1我们定义L的主体排序为元组L=（CL，EL，βL），其中• CL是L• EL是L中事件的集合，定义为EL=ML× {？，！}，其中m？，m！分别表示消息m∈ML的接收和发送• βL（c）是与组件c相关联的消息的集合。功能βL定义为βL：CL→ε（ML）。请注意，我们对消息和事件使用不同的集合：这里的事件被理解为发送或接收消息。在特定场景中，每个组件都将发送和接收一组消息。因此，在LSC主体中建模的行为作为一个整体可以描述为：给每个分量c赋一个序列x∈βL（c）<$，其中βL（c）<$表示βL（c）上所有有限序列的集合这就引出了下面的定义。定义4.2假设LSC体L是LSC体L的一种。 我们定义V_L为所有函数v：C_L→E_L使得v（c）∈β_L（c）_L的集合。我们将V_L的元素称为L-向量.S. Moschoyiannis/Electronic Notes in Theoretical Computer Science 108（2004）8393≤因此，V<$L实质上是集合βL（c）<$的笛卡尔积。感兴趣的读者可以参考[12]中关于L-向量的数学. 功能v返回进入或离开组件c的消息的有限序列，并且对于参与L中描述的交互的每个组件。把这样的序列放在一起，每个组件一个，我们形成（一组）序列向量，其中每个坐标对应于一个组件，并包含该组件发送或接收的消息的有限序列基于这些定义，可以正式描述LSC主体L作为由一个sort函数L描述的静态结构和一个L-向量语言组成。定义4.3LSC体L是一对（L，S），其中•L是L• SVL是L的快照术语快照指的是所有可能的L-向量的子集，即那些确实对应于L中描述的强制行为的向量。简言之，由LSCL监控的系统的快照表示在一段时间内的任何时间拾取L激活。 每个组件的当前位置指示该组件的哪些事件已经发生。快照的排序基于其序列的前缀排序首先，让我们建立我们的符号。如果x和y是序列，我们写x.y表示x和y的连接。众所周知，该操作与恒等式Λ相关联，其中Λ表示空序列。我们在由xy给出的序列上有一个偏序当且仅当存在z使得x.z=y，并且这个偏序有一个底元素Λ。最后，级联是可消的，因此序列z是唯一的。在快照中的事件序列之间的排序映射到这些事件在图表上发生的图形位置（或位置）的自上而下的排序。在下面的内容中，我们使用前面提供的调优示例来说明如何在我们的正式模型中解释该场景中的交互。对于图2的LSC，我们具有CL={A，B，C，D}，并且ML={d，dA，b，bA，c， cA，r，rA，u，uA}，其中我们缩写了所有消息第一个字母和相应的下标A的缩写，以增加可读性。与每个组件相关联的消息集由下式给出：βL（A）={c，cA}βL（B）={d，dA，r，rA，c，cA}94S. Moschoyiannis/Electronic Notes in Theoretical Computer Science 108（2004）83βL（C）={d，dA，b，bA，r，rA，u，uA}βL（D）={b，bA，u，uA}在这种情况下，图1的改变频率LSC的快照集合2由以下向量组成S={（Λ， Λ），（Λ，d！，d？，Λ），（Λ，d！，d？b！（b）、（Λ，d！，d？b！bA？，b？bA！）、（Λ，d！DA？，d？b！bA？天啊！，b？bA！）、（c？，d！DA？c！，d？b！bA？天啊！，b？bA！）、（c？cA！，d！DA？c！cA？，d？b！bA？天啊！，b？bA！）、（c？cA！，d！DA？c！cA？r！，d？b！bA？天啊！r？，b？bA！）、（c？cA！，d！DA？c！cA？r！，d？b！bA？天啊！r？u！，b？bA！u？）、（c？cA！，d！DA？c！cA？r！，d？b！bA？天啊！r？u！uA？，b？bA！你呢？uA！）、（c？cA！，d！DA？c！cA？r！rA？，d？b！bA？天啊！r？u！uA？rA？，b？bA！你呢？uA！）}在进一步解释该符号时，我们从描述最小行为的空快照开始，并通过在每个步骤中包括一对同时发生的事件来逐步构建快照集。请记住，这里的同步事件被认为是发送和接收相同的消息（例如d！而d？分别在B和C上在第二张快照中）。最后或最大快照描述了在执行更改调谐器频率的场景时必须发生的所有交互。通过考虑最大快照的所有前趋来确定不同坐标处的相互作用之间的排序。考虑到[2]中描述的主图的骨架自动机，如果任何消息出现在[1]中给出的序列之外，我们可以说它从“活动”转换S.如果所有消息的出现都遵守S中的顺序，则图表将达到“终止”状态快照集基本上描述了参与组件的输入/输出行为，并提供了有关其状态的其他行为信息。 每个组件进入“中间”状态，它发出请求m！并且每当它接收到相应的确认m A？时返回到在稳定状态下，组件保证它提供的服务但是，当它处于中间状态时，情况并非如此，因此，在我们的示例中，所有组件在处于中间状态时都不接受任何消息（操作调用）（假设有一个S. Moschoyiannis/Electronic Notes in Theoretical Computer Science 108（2004）8395每个组件的控制线程）。唯一的例外是B。这个组件有一个额外的“宽容”的中间状态。 每当它进入这个状态时，它与C进行丢弃请求。在其容许的中间状态，B可以接受新的消息调谐（FJ）并存储新的频率值以供以后使用。接收dropAck会使其恢复到稳定状态。这反映了CE产品中的典型要求，即最后一个用户请求将首先得到服务。这些概念被正式地放在下面的定义中。定义4.4假设L =（L，S）是一个LSC天体，s =（s1，.，. s n），s∈S是L中n个分量的快照，c∈C L是L中的分量，si是s中对应的坐标。 我们可以说，C是在对于每个m，都有一个稳定的状态i！∈EL，m∈ML，则存在mA？∈EL，mA∈ML使得mA？出现在i。如果对于每个s i，i = 1. n，对应的组件处于稳定状态，则我们将说快照s处于稳定状态。接收器组件的稳定状态是双重定义的。在改变频率LSC（参见图2）中的组件交互的形式解释实质上确定在改变调谐器的频率时所展示的行为过程中的任何时间，哪些组件处于当组件处于稳定状态时，它也知道发送方组件的状态。请注意，在消息标签上使用OCL 2.0表示法，如[6]中所建议的，也可以包括发送者这种行为信息在面对诸如添加新组件、移除、替换、组件版本控制等活动时变得特别有用。作为一个小提示，我们回到关于隐藏事件的讨论。我们可以加个活动的？fortune（f）作为所有快照（空快照除外）的第二个坐标中序列的第一个元素那么我们可以说，预图也在考虑之中。以类似的方式，添加一个tA！在最后一个快照的第二个坐标中的序列的结尾可能会解释包含到达主体的结尾的行为。然而，由于我们希望对组件配置中响应“外部”事件所发生的事情进行建模，因此在任何情况下，这都不会严重影响我们解释的本质5结论和今后的工作我们已经提出了一个正式的方法来描述行为在组件之间的接口，在一个给定的LSC的上下文中。我们的方法是96S. Moschoyiannis/Electronic Notes in Theoretical Computer Science 108（2004）83通过来自用于消费电子产品的嵌入式软件的小示例来说明组件交互首先使用LSC建模，然后使用LSC生成的快照进行形式化。此外，一个基本目标是使用LSC中描述的强制行为作为我们在其他地方描述的组件模型的起点[7，8]。在组件设置中建模交互的另一个选择是使用UML序列图。有趣的是，UML2.0 [10]正在经历一些变化，试图采用LSC的基本概念。事实上，它们提供了一种类似于地方合同公司的强制行为概念。然而，选择使用LSC的主要原因是，UML 2.0中的序列图仍然被赋予了交错语义，就像UML1.x中一样。两个事件同时发生的情况在基于组件的系统中很常见，因此真并发语义更适合。我们正在考虑的正式模型[7，8，12]是一个真正的并发模型，LSC非常适合真正的并发语义，如[5]所示。我们获取状态信息的方法支持我们的固有假设，即组件使用我们示例中的原始通信机制进行通信另一方面，这似乎与[13]和其他地方关于组件契约的观点以及[3]中关于组件交互的乐观观点具体来说，在[14]中提出的水平通信风格中，其中组件对其每个邻居都具有排他性端口/接口，我们的建模方法允许组件正确执行其部分，而无需了解特定配置。实际上，每个组件知道与其每个端口相关联的信号集，因此，通过从其最近的邻居接收请求或应答，它知道它们的状态。形式模型，在某种程度上，它已被采用解释组件在一个给定的LSC的相互作用，并在一定程度上，它是在这里提出的，似乎在表达并发性和非确定性的限制然而，原始的组件模型[7，8，12]更具表现力。该模型的出发点与[1]的代数规范模型十分接近。然而，这两个模型在后续中出现分歧，因为我们的模型是基于组件行为集的有序理论结构，并且在[8]中描述的某些条件下，它可以与行为呈现[11]相关联，这让人想起[9]的事件结构模型。因此，我们最终得到了一个强大的真并发模型，其中非确定性，并发性以及并发性可以表示为不同的现象。我们的例子的小扩展，在第3节中给出，对应于S. Moschoyiannis/Electronic Notes in Theoretical Computer Science 108（2004）8397使用[14]中的分叉，将组件的一个输出连接到其他组件的两个（或[14]中的fork以任何顺序发出请求，而不是同时发出请求。此外，开关用于将n个输入中的一个连接到一个输出。这种连接器的使用考虑了并行性和/或并发性，以及所发出请求的互斥。我们很有兴趣看看，使行为呈现的关联能够被施加到快照的序理论结构上的条件是如何实现的。这将允许我们使用行为呈现来确定快照中出现的事件的发生之间的时间关系。这里提出的工作的另一个可能的扩展与自动机的关联快照有关基于允许关联到行为表示的条件的结果，组件可以与某类自动机相关联[12]。在本文中，我们考虑了LSC中描述的特定场景，作为建模组件行为的起点。在某种重要意义上，我们将环境仅限于强制行为这一观点与[3]中的乐观观点一致进一步研究约束环境对从我们的模型导出的自动机的影响将是有趣的。确认我们感谢匿名推荐人的宝贵意见。引用[1] M.布洛伊反应系统的代数规范。Theoretical Computer Science，239（2000）：3[2] W.该死的D。哈雷尔LCSs：Breathing Life Into Message Sequence Charts. 系统设计中的形式化方法，19（1）：45[3] L. de Alfaro和T.亨辛格接口自动机软件工程基础（FSEACM Press，2001.[4] D. Harel和R.马雷利来吧，让Springer-Verlag，2003.[5] J. Klose和H.维特基 基于自动机的实时序列图解释 在T. Margaria和W.Yi，编者，TACAS 2001，LNCS第2031卷。Springer，2001年。[6] J. KuésterFilipe.给我一个机会，让我参加比赛。在H。-D. Ehrich，J. -J. 我是，而且M. Ryan，编辑，Agent，对象和功能：当代软件的结构化机制，LNCS。Springer，2004.出现。[7] S. Moschoyiannis和M.W. 盾牌一个组件组合的集合论框架Fundamenta Informaticae，59（4）：373[8] S. 我 的 天 啊 ， M 。 W.她 和 J 。 KuésterFilipe. FormalisingWell-BehaveedComponents. 在Proceedings Formal Aspects of Component Software （ FACS ） ， Satellite Workshop ofFME联合国大学/软件技术研究所第284号，2003年。98S. Moschoyiannis/Electronic Notes in Theoretical Computer Science 108（2004）83[9] M. Nielsen，G.Plotkin和G.温斯克Petri网，事件结构和域，第1部分。理论计算机科学，13：85[10] OMG. UML 2.0上层结构草案采用规范。OMG文档ad/03-01-07，可从http://www.omg.org获得，2003年8月[11] M. W.盾牌行为表现。在de Bakker，de Roever和Rozenberg，编辑，Linear Time，BranchingTime and Partial Orders in Logics and Models for Concurrency，第354卷，第671-689页。Springer Verlag，1988年。[12] M. W. Shields和D.皮特第一章：单组分理论（Theory of a Single Component）技术报告SCOP-TC-01-01，萨里大学，2001年。[13] C. Szyperski。组件软件：超越面向对象编程。艾迪森·韦斯利1997年[14] R.范·奥梅林横向通讯：一种控制软件的编写方式。软件：实践与经验，2003年。出现。[15] R. van Ommering，F.范德林登，J克莱默，J马吉。Koala消费电子产品组件模型。IEEETransactions on Computers，33（3）：78[16] ITU-TS建议Z.120。 消息序列图（MSC）。 ITU-TS，1996年。