并发自动机模型下的组件行为描述及接口兼容性检查方法

理论计算机科学电子笔记141（2005）199-220www.elsevier.com/locate/entcs用并发自动机放大图片作者：Michael W.Shields和Paul J.Krause英国萨里大学计算机系，吉尔福德，萨里，GU2 7XH，英国摘要组件的有效（重用）使用需要精确描述可观察行为的语言，以及检查设计中组件接口兼容性的方法。这在并发的情况下更具挑战性。 在以前的工作中，我们已经考虑了一个基于集合的组件及其组成的模型，在并发设置。 在本文中，我们提出了一类自动机，称为真并发自动机，其中真并发被视为一个显式的结构属性。 我们展示了如何自动机可以从一个组件，每个这样的自动机生成回一个组件。除了确定底层组件的使用协议外，对我们模型的这种扩展还提供了对组件组成的有用见解。关键词：构件行为，并发，自动机1介绍复杂的高完整性软件系统，例如[9]中描述的那些，通常被划分为互连的组件。然而，经验表明（例如，在消费电子行业[28]），由于组件接口之间的复杂调用相互作用期间出现的细微不一致性，因此最终软件可能无法按要求运行。例如，一个组件可能需要某些信号连续到达，而另一个组件同时生成它们。因此，系统可能会表现出1电子邮件：s. eim.surrey.ac.uk1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.04.035200S. Moschoyiannis等人理论计算机科学电子笔记141（2005）199病态行为也就是说，行为不是故意的，而是由这种不一致造成的。我们研究交互系统的离散模型，自然，我们的兴趣在于组件的可观察行为，而不是它们的内部结构。在这种情况下，将行为描述为在组件的接口我们提出了一个基于自动机的语言来描述这样的行为的一个组件。这允许捕获有关组件的操作被调用的顺序以及组件（作为响应）调用外部操作的顺序的说明从某种重要意义上说，我们本质上也在对组件的环境进行建模，当涉及到组合时，如果有一些环境满足两者的所有假设，则可以将两个组件这与[6]中的乐观虽然使用基于自动机的形式主义建模行为并不新鲜，但所提出的自动机很有趣，因为它们可以显式地表达并发性。可能有人会说，在组件设置中存在一些现象，例如竞争条件，这些现象只能被理解为并发性和非确定性之间的不幸交互。这种现象在诸如通信和消费电子产品的领域中是令人感兴趣的。也有人认为，交错的方法，并货币是不够的，适当的处理性质，如公平[14]。此外，在以前的工作[19，18]中，我们一直关注组件的形式模型的开发，该模型允许对组件及其组成的通用属性进行推理在本文中，我们关注的是从模型中导出一类自动机，它生成模型的对象，并且只生成它们。相应的自动机可以被看作是一个扩展，使模型更接近自动化并最终获得工具支持。本文件的结构如下。在第2节中，我们给出了我们的组件模型和概述组件组成。在第3节中，我们介绍了用于描述组件行为的自动机。我们从一种类型的抽象机器开始，然后将并发性视为进一步的结构属性，这导致了自动机的定义。我们还概述了初步工作的一个正式的概念组成的自动机。本文件最后提出了一些结论意见和对今后工作的设想。S. Moschoyiannis等人理论计算机科学电子笔记141（2005）1992012组件模型在本节中，我们简要概述了我们正在考虑的组件模型介绍仅限于模型背后的关键概念。更多的细节和适当的介绍可以在[19，18]中找到。在熟悉的“契约式设计”范例[ 15 ]中所提供的服务是通过一组提供接口提供的，而相互的义务是通过一组要求接口来满足的根据组件的契约使用，组件的静态语义是根据两个不相交的接口集来捕获的。组件需要的和组件提供的此外，静态语义为每个接口指定了它支持的操作。设I为接口名称的集合，Op为与I中的接口相关的操作的集合。定义2.1分量签名是元组n =（Pn，Rn，βn），其中• P接口是一组提供接口的• R接口是一组需要的接口• β：PR→（Op）;因此，β（i）返回与接口i并且我们求出了PR =。 De finn e I=PR。组件的动态语义由一组可能的语义组成。每个行为都将一系列操作与每个接口相关联。 我们定义V为所有函数v：I→Op的集合，使得对于每个i∈I<$，我们有v（i）∈β<$（i）<$。我们将提到的元素V as分量向量我们用β（i）表示β（i）上的有限序列的集合。在数学上，V是集合β（i）的乘积。分量向量基本上是序列的n元组，其中每个坐标对应于一个整数。组件的接口（因此n是组件接口的数量），并包含可能在该接口上发生的事件（例如操作调用）的有限序列。 其思想是，组件作为一个整体的行为可以通过将这样的序列分配给它的每个接口来描述我们现在可以通过限制到适当的子集来定义组件包括仅描述预期行为的分量向量定义2.2分量c是一对（V，V），其中• 是c202S. Moschoyiannis等人理论计算机科学电子笔记141（2005）199• VV（和V）是由一个Viursofc构成的。因此，一个组件的静态结构是由一个特征向量描述的，而它的行为是由一个组件语言V描述的，它本质上是一个向量2.1组件语言在本节中，我们将介绍基本的操作，这将使我们能够manipulate一个组件的语言和原因组件的行为。我们已经看到，分量向量本质上是序列的元组。因此，我们可以根据众所周知的序列运算来定义分量向量上的运算。对于u，v∈V，我们定义，• 联合v是唯一向量w，使得w（i）= u（i）。v（i），对于每个i ∈I<$（concatenation）• u≤vi <$u（i）≤v（i），对于每个i∈I<$（前缀序）很容易看出V是一个具有二元运算'的幺半群和单位元Λ，其中Λ是唯一向量，其中Λ（i）= Λ，对于每个i∈I，Λ表示空序列。此外，V是偏序集（偏序集），偏序为现在基于V的序论性质，我们可以进一步定义，对于u，v∈V，• uHv是满足w（i）=min（u（i），v（i））的向量w，对于每个i• uH v（如果存在）是满足w（i）= max（u（i），v（i））的向量w注意，uH v仅在max（u（i），v（i））存在时定义，对于每个i。在偏序方面，这些操作基本上给出了最大的较低的界和最小上界，分别为u，v∈V<$，在通常意义上的格和域理论[5，29]。为了预测，最大下限和最小上限在定义正态性属性(cf定义2.5），它允许我们限制到一类组件，即所谓的行为良好的组件。我们将引用标识一个远程通信操作符“/”。 因此，如果u是行为v的初始部分，使得u≤v，则v/u是u的“延拓”，将其扩展到v。形式上来说，如果u≤v，那么我们定义v/u为唯一的元素z∈ V，使得u。z= v右消去算子对于定义相应自动机的转换结构特别有用，因为它决定了从u表示的行为到v表示的行为发生了什么事件。我们将有更多的话要说，当我们也定义得很好，S. Moschoyiannis等人理论计算机科学电子笔记141（2005）199203行为组件。2.2行为良好的组件在我们对组件行为建模的方法中，我们限制到特定的组件类。这些组件的语言是离散的和局部左闭的。这些属性的定义如下（也见[19]）。定义2.3设c=（v，V）是一个分支，则V是离散的i ∈ V，Λ∈V，且只要u，v，w∈V使得u，v≤w，则（i）uHv∈V和（ii）uHv∈V注意，uHv∈V被理解为断言uHu被定义。定义2.4设c=（v，V）是一个分支，i∈I<$且x∈β<$（i）<$。 则V是局部左闭的i ∈ V，当v∈V使得ΛΛ的事件e（i这些对应于在相应的行为表现中事件发生的连续性类别关系下面的结果将' a '与右取消运算符相关联命题2.7设V<$V<$是正规的，且u，v∈V。如果u是v，那么v/u∈E为了进一步预测，这使我们能够定义一个过渡结构，在第3节中，当涉及到将行为良好的组件与自动机相关联时，例2.8考虑图1中的示例组件，该组件预期如下操作（可能在给定场景的上下文中• 组件在接口p1上接收对操作c的调用（来自其他组件或环境）• 一旦接收到操作调用c，组件通过在接口r1和r2中的每一个上对操作d进行调用来响应（这些接口的实现由其他组件提供）。• 该组件然后继续在接口R3上进行操作调用T然后准备好在P1上接收新的C当P∈x时，由y∈x=（P∈x，R∈x，β∈x）给出了该函数的特征值 ={p1}，R∈x ={r1，r2，r3}和βex（p1）={c}，βex（r1）={d}=βex（r2）anddβex（r3）={t}. 我们可以把PexRex =S. Moschoyiannis等人理论计算机科学电子笔记141（2005）199205图1.一、且Pex<$Rex=Iex.我们现在可以获得一组行为，这些行为表明，相对于上面给出的其功能的非正式描述，ex组件的期望行为是什么。因此，我们考虑符号空间上的向量如果我们写（x，y，z，w），其中v（ p1）= x，v（ r1）= y，v（r2）= z 和v（r3）=w该行为的描述可解释如下─ing组件语言Vex={（Λ， Λ），（c，Λ），（c，d，Λ， Λ），（c，Λ，d， Λ），（c，d，d，Λ），（c，d，d，t）}每个分量向量应被理解为指示哪个分量向量事件已经发生，以及在哪个接口上。注意cex=（Vex，Vex）是一个分量。这里值得指出的是，集合Vex通常通过组件开发人员给出的行为（部分）描述来获得，甚至可能以序列图的形式描述组件与我们正在考虑的行为片段的交互例如，在[17]中，我们描述了使用LSC [4]（仅限于基本功能）作为组件模型版本的起点。然而，关于获得组件语言的进一步考虑超出了本文的范围我们示例中的组件行为良好。由于篇幅限制，我们在此不检查正态性。通过绘制订单的Hasse图来检查情况是否确实如此是相对简单的Vex的结构。关于“a”的定义2.6（Λ， Λ）a（c，Λ）和（c，Λ）a（c，d，Λ， Λ）（c，Λ）a（c，Λ，d， Λ）和（c，d，Λ， Λ）a（c，d，d，Λ）（c，Λ，d， Λ）a（c，d，d，Λ）和（c，d，d，Λ）a（c，d，d，t）与组件（我们的示例中考虑的行为片段）相关联的列向量（事件）集为e1=（c，Λ），e2=（Λ，d， Λ， Λ），e3=（Λ， Λ，d， Λ），e4=（Λ，t）并且，E∈ex={e1，e2，e3，e4}。 该示例在第3节中进行了说明。Q2.3组分组合物我们一直关注的是一个单一的组成部分。在本节中，我们简要概述了我们的框架内的组成。完整的细节可以找到<<组件>>p1R1RR3206S. Moschoyiannis等人理论计算机科学电子笔记141（2005）199KK1 2 12在[18]中。组成背后的关键思想如下。如果组件c1提供接口i，而组件c2需要接口i，则如果它们对接口i的限制相同，则可以组合c1的行为和c2从这些行为的构成来看，移除对应于i的组合发生在互补的接口上;也就是说，一个组件需要的接口和另一个组件提供的接口，在CCS [16]或CSP [11]中的复杂标签的精神。我们假设每个组件的提供接口和必需接口的集合是不相交的。因此，一个条件是在组件签名上需要。我们定义1，2是一致的，并写1↓2 i•P1 P2=•R1 R2=• <$i∈I<$1<$I<$2：β<$1（i）=β<$2（i）请注意，组件签名之间的一致性意味着互补接口是属于集合的接口I<$1<$I<$2=（P<$1<$R<$2）<$（R<$1<$P<$2）通过消除所有互补界面，由单独组件的签名形成复合物的签名。因此，复合签名将所有共享接口内部化。因此，我们定义12 =，其中• P=（P1<$P2）\（R 1<$ R2）• R=（R1<$R2）\（P1<$ P2）• β（i）=β（i），其中i∈I，k=1，2在定义了复合的签名之后，我们现在继续定义它的组件语言，以类似于处理单个组件的方式。首先，我们描述如何组成分量向量。定义2.9Letc1=（V1，V1）anddc2=（V2，V2）becomponts. 向量u1∈V1和u2∈V2是一致的，且我们可写u1↓u2，如果u1[II=u2[II其中f[X]表示函数f对集合X的限制，在这种情况下，我们定义，u1<$u2=（u1<$u2）[I<$1ΔI<$2S. Moschoyiannis等人理论计算机科学电子笔记141（2005）199207当reI1ΔI2=（I1\I2）（I2\I1）和u1u2：I1ΔI2satis时，⎧i∈I<$1（u1<$u2）（i）=u（i），i∈I22这是很好的定义，如果u1↓u2。现在我们可以给出成分的合成的形式定义。定义2.10Letck=（Vk，Vk），对于ea chk，becomnts。定义它们的组成c1<$c2=（v，V）其中，• =• V=V1V2，V<$1<$V<$2={v∈V<$|<$u1∈V<$1，<$u2∈V<$2：u1<$u2<$v= u1<$u2}最后，我们将需要一些符号来表示元素的向量的投影，因为它可以将元素的向量投影到元素中。对于v∈V<$1<$V<$2，在h1↓2下，我们定义ev[k]=v[I，其中k= 1， 2. 这种结构让人想起用于给出并行[12]《易经》中的阴阳五行。3用于组件行为在这一节中，我们定义了一类自动机，即所谓的自动机，用于对组件的可观察行为进行建模。完整的细节和完整的证明可以在[26]中找到。所提出的自动机可以被看作是异步转换系统[23，2]的细化和混合转换系统[25]的在正规分量语言V中，如果v = u，则向量z将向量u扩展为向量v。z，并且V中没有其他向量严格位于u和v之间。后一个要求可以通过说v覆盖u来表达，在定义2.6的意义上。将u扩展到v的延拓z使用右消去算子定义，即v/u=z。在一个普通的组件语言中，这样的延续变成了E的元素（通过命题2.7）。这一观察给出了一个过渡关系，它导致定义一种过渡系统。定义3.1设f是一个组件签名。 我们定义一个机器为一对M=（Q，>），其中• Q是一组状态• ><$Q×E<$<$ ×Q是转换关系，对于（q，e，qJ） ∈>，我们写q>eqJK208S. Moschoyiannis等人理论计算机科学电子笔记141（2005）199Σ其中满足：(i) q>eq1<$q>eJq2<$e≤eJ<$e=eJ<$q1=q2(ii) q>eqjq>eJqje=eJ我们还定义了一个根机器为一对M=（M，q），其中M=（Q，>）是一个根机器，q∈Q。我们写q>e来表示存在qJ∈Q使得q>eqJ。注意，条件（i）包括e=eJ的情况，在这种情况下，条件可以重写为q>eq1<$q>eq2<$q1=q2。该条件保证了明确性，并且还涉及随后的自动机的定义（参见定义3.6）。有根的机器以通常的方式确定向量的语言定义3.2设M=（Q，>）是一台机器，q∈Q. 定义q→uqJ，如果(i) q=qJ和u=Λ(ii) u= v。e，e∈ E<$，使得q →vq <$>eqJ，某些q <$∈ Q我们还定义了V（M，q）={u∈V<$：<$qJ∈Q，q→uqJ}。这给出了一个并行机的执行向量。实际上，这些是通过重复地连接列向量e而形成的分量向量，并且可以被理解为描述各个转变的序列定义3.2中的第（i）点指的是内部过渡，当涉及到构图时，这些过渡可能并不令人惊讶。定义的第（ii）点说，只要有一个分量向量是另一个向量v和一个列向量的连接，那么就有一个状态通过列向量的简单转换将你带到目标状态，并且该状态可以通过向量v所暗示的转换从源状态到达。 可以看出，这可能涉及将分量向量分解成一系列具有列向量的级联，如[27]所示。这是进一步利用表明，相应的向量语言的自动机是局部左闭的，作为建立一个自动机生成一个正常的组件语言的一部分。在介绍自动机之前，我们讨论了如何从一个行为良好的组件导出一个自动机这是通过将V中的分量向量作为状态来完成的，并以一种反映观察结果的方式定义一个转移关系，即行为可以通过重复连接列向量来从空向量中建立起来。事实上，这占用了在定义机器之前提出的想法。定义3.3设c=（v，V）是V正规的分量。 定义Mc=S. Moschoyiannis等人理论计算机科学电子笔记141（2005）199209e1VCCΣQ（V，>V）其中u>e v惠uavv/u=e我们还定义了M=（M c，Λ）。注意v/u∈E，只要uav，由命题2.7，这样定义就有意义了。这种结构给出了一个机器Mc。 此外，可以证明，由Mc从初始状态Λk生成的向量语言使用定义3.2的执行向量确定相同的组件。在我们的符号中，这表示为V（M）=V。我们现在开始考虑组件语言和相应的并行机中的真并发性，同时仍然处理正常的组件语言。为了在这种情况下明确地表示并发性，其中相同的事件有时可能是并发的，有时可能不是，我们定义了分量向量上的独立关系（参见定义3.4），并确定其与并行机的转移结构的关系（参见定义3.5）。这导致了对自动机的额外约束，从而导致了自动机的定义。我们首先考虑分量向量的独立关系定义3.4设u，v是V中的分量向量。u和v是独立的，我们写uindv，i ind v，iind v。i∈I该定义的动机是行为u和v可以独立发生，只要它们涉及组件的不同接口。可能值得指出的是，独立性本身并不足以保证并发性。通过考察以下定义，这一点应该变得清晰起来。定义3.5设M = （Q，>）是一台机器。我们定义一个关系IM<$Q×E<$X E<$，对于（q，e1，e2）∈IM，我们记为e1IMeeIMe在de（q， q，qJ∈Q：q>e1qq>e2q>e1qJ）1q21 21 2 1 2我们将像往常一样，删除上标时，它是明确的从上下文。年q1e1inde2e1qq'e2Q2图二. 并发转换e1，e2210S. Moschoyiannis等人理论计算机科学电子笔记141（2005）199ΣQ21Q因此，对于状态q处的并发性的最低要求是，两个独立的传出转换都被启用，并且都以不特定的顺序在状态q和qJ如图2所示。关系Iq定义了局部并发性，在这个意义上，列向量E1和E2在机器的状态Q我们现在要把自动机改进为自动机，同时考虑到这两种关系。定义3.6设k是一个签名。 一个自动机M是一个自动机M=（Q，>），满足(i) Ife1IMe且q>e1q1>e2q1，henq>e2q2>e1q1，someq2∈Q(ii) 如果q1>e1q1且q2>e2q1且q1/=suchthatq>e2q1且q>e1q2q2，则e1inde2，存在q∈Q(iii) 若u，v∈V 且q→u，vQJJ，则有<$QJ∈Q使得q→uQJ惠QJ→vQJJ(iv) Ife1，e2∈Es. t. q>e1，e2且x∈V（M，q），其中e1，e2≤x，我们还定义了一个有根的自动机是一个有根的自动机M=（M，q），其中M是一个自动机。注意，通过定义3.5和定义3.6的（i），我们得到Iq是对称和不对称的。对称性反映了并发总是相互的事实，而不对称性则禁止将事件视为与其自身并发。条件（i）是非交错表示行为的自动机的特征，有时称为菱形规则[23，25，27]。如果两个独立的事件发生在两个状态q和qn之间，那么它们的发生没有特定的顺序。换句话说，它们应该有可能以互换的顺序发生。如图3所示。年q1e1Iq e2q年q1e1e2=>qqe2e1Q2图三. （一）定义3.6条件（ii）涉及生成语言的离散性。下面几句话是为了进一步解释这一点。离散性要求向量语言中上界的元素有它们的最小上界和最大下界。因此，为了保证离散性，我们需要偏序集是（有限）格的条件。分析[26]e1e2QS. Moschoyiannis等人理论计算机科学电子笔记141（2005）199211e1e2e1e2e2e1证明了当↓u={v∈V：v≤u}是V的子格时，V是V的离散子集.只有当V满足以下条件时，情况才会如此u，v，x∈V，u/=v<$uax<$vax=<$x=uHv <$uHv这就是所谓的下菱形属性（LLP），本质上说，只要我们有菱形的上半部分，那么我们就有整个菱形。它以条件（ii）的形式表现在自动机的结构中。如图4所示。Q Qq1q2=>e1inde2q1q2Q见图4。 定义3.6的条件（ii）条件（iii）排除了执行向量可以以两种不同的方式从各个转换的序列中产生的可能性。换句话说，当执行向量的第一部分将我们从其初始状态带到中间状态时，剩余部分将我们从该状态带到（执行向量对偶地，我们可以对执行向量的第二部分进行同样的这种情况如图5所示。q ''quuQv=>Q'uq ''u.VQq ''Q'Q=>q'q ''图五. 定义3.6的条件（iii）条件（iv）是说，如果两个不同的转换可以从q开始相同的行为，即从q开始相同的执行向量的一部分，那么它们必须同时进行。这种情况的动机并不难理解。明白了给定描述组件在状态q处的行为的组件向量u，两个不同的转换e1、e2实质上提供两个不同的方法，比如说v1，v2，扩展到由x描述的行为。换句话说，联合v1 = x和u。v2 = x.但这意味着v1和v2描述了相同的行为。因为e1是v1的前缀，e2是v2的前缀，e1，e2是不同的，所以我们一般不可能有v1=v2。只有当e1，e2是并发的时候才会出现这种情况这就是条件（iv）。UML [21]被广泛用于软件系统的建模和文档化虽然它不是为基于组件的设计而开发的，但一些vu.VuQvu.V212S. Moschoyiannis等人理论计算机科学电子笔记141（2005）199ex它的符号可以使我们的组件模型更接近于软件设计的更传统的方法。关于UML 2.0状态机和其中定义的复合转换的概念（[21]中的第500-1页），条件（iv）可以被看作是复合转换的头部有多个转换到一组正交状态（fork）的情况的形式化。此外，通过将条件（iv）应用于条件(ii)对于UML2.0状态机中的复合转换的尾部，我们可以说是相同的。关于在UML和条件（iv）（和（ii））中建立复合转换之间的关系的唯一问题是，UML 2.0规范文档中给出的复合转换的语义不允许触发进入连接或从分叉发出的转换（[21]中的第470-4根据我们的“语义”，在这两种情况下，转换都我们的解释是它们是同时发生的（见条 件 （ iv ） ） . 事 实 上 ， 这 与 statecharts [7] 中 joins 和 fork 的STATEMATE语义（[8]中的第302-3页）一致作为定义3.6的最后一个注释，可以看出条件（iii）是一个全局性质而不是局部性质。这使得检查它变得困难。[26] 为此目的制定了以下规定。设M=（Q，>）是一台机器，V<$V <$.若（a）存在一个到上函数φ：V→Q使得φ（u）>eφ（v）i <$v= u. （b）若u，v∈V且u≤v，（u/= v），则存在e∈E ∈V，使得u. e∈V和u. e≤v，则M满足定义3.6的（iii）。例3.7考虑例2.8的组件，我们现在可以定义元组Mex=（Qex，>ex），其中Qex=Vex且>ex由下式给出：e 如果f∈e∈E 且u，v∈ V exs. t. ua v v/u= e对于V ex中的分量向量，我们有，Λ>e1（c，Λ）（c，Λ）>e2（c，d，Λ，Λ）（c，Λ）>e3（c，Λ，d，Λ）（c，d，Λ，Λ）>e3（c，d，d，Λ）（c，Λ，d，Λ）>e2（c，d，d，Λ）（c，d，d，Λ）>e4（c，d，d，t）我们检查定义3.1的条件。• q>e和q>eJ 其中e≤ej，对noq∈Qex，e，EJ∈E∈ex. 因此，（i）定义3.1成立。• q>eqj和q>EJQJ，其中对于noq，e，EJ， 因此，定义3.1的（ii）也成立。因此，Mex是一台机器。Q>exS. Moschoyiannis等人理论计算机科学电子笔记141（2005）1992131223为了进一步证明Mex是一个并行自动机，我们需要考虑局部并发性。我们从识别独立的列向量开始我们有e1ind e5−k，其中k = 1。3，和e2inde5−k，对于k= 1， 2和e3inde4。因此，在这种情况下，所有e∈Eex都是独立的。 根据定义3。五，J如果eIqeJ，则eindeJ且q>eq且q>eq>eqJ。 我们观察到所有事件与组件相关的组件是独立的，因此我们只这是一个很好的例子。q>e和q>eJ仅对e和e成立，3同样，如果q1，q2，qJ满足at（c，Λ）=q>e2，q1=（c，d，Λ，Λ）和d（c，Λ）=q>e3，q2=（c，Λ，d，Λ）>e2，则q1，q 2，q 2也成立qJ=（c，d，d，Λ）。因此，e2I（c，Λ）e3。请注意，这个例子表明独立性本身不足以保证本地并发性。此外，它还表明，两个列向量在某些状态下可能是并发的（这里q=（c，Λ）），但在其他状态下则不是;例如，我们没有e2I（c，d，d，Λ）e3。最后，我们通过检验M ex的条件，证明了Mex是一个自相关自动机定义3.6.第一个条件仅与e2，e3相关（取q=（c，Λ），q1=（c，d，Λ，Λ），q=（c，d，d，Λ）），其中在这种情况下，e具有q>e3q2>e2 对于q2=（c，Λ，d，Λ）∈Qex.因此，定义3.6的条件（i）成立。J对于条件（ii），我们有，q1>eq，且q2>eq，且ei=eJ，是J只有当e=e2和e=e时才有情况。但是对于这些列向量，这里ex是tsq=（c，Λ）sucht h在q>e3q1和q>e2q2。因此，条件（ii）成立。对于条件（iii），我们发现更容易检查相关引理。我们定义一个函数φ：Vex→Qex：φ（u）= qk，φu∈Vex，k = 0. 5使得φ（（Λ， Λ））=q0φ（（c，Λ））=q1φ（（c，d，Λ，Λ））=q2φ（（c，Λ，d， Λ））=q3φ（ （ c，d， d，Λ ） ）=q4φ（（c，d，d，t））=q5通过定义φ和例2.8中的关系式条件（b）是从成分语言Vex和覆盖关系中得出的。因此，我们可以推断定义3.6的条件（iii）成立。对于条件（iv），只有当q>e时，eJ 对于q=（c，Λ）e=e，EJ=e，我们也有e，e≤x=（c，d，d，Λ）。因此，在本发明中，2 3 2 3对于E2、E3，满足条件（IV）的前提。 但是，对于这些列，向量我们有e2I（c，Λ，Λ）e3，因此，定义的条件（iv）成立。因此，Mex是一个自动机。它可以用状态图来表示除了相互关系之外，它符合UML 2.0状态图[21]和状态图[7]的符号。Mex的状态图如图6所示，其中q1co q2意味着从q1到q2和q3的转换没有特定的顺序。这是用相关的214S. Moschoyiannis等人理论计算机科学电子笔记141（2005）199Σe1（，）（c，）e2e3（c，d，，）co（c，，e3e2e4（c、d、（c，d，d，t）见图6。 自动机Mex它们是由Iq相关的。注意，在不引入状态之间的相关性的情况下，di-gram将简单地表示取e2然后取e3与取e3然后取e2之间的不确定性选择。因为在一个自动机中我们可以表达真并发，我们需要一个表示e2，e3hap的图形符号，没有特别的顺序。我们选择使用一氧化碳主要是由在异步转换系统中指示事件之间的独立性的早期建议（例如[23，25]中的菱形阴影或在[10]中使用菱形内的α-淀粉。选择适当的符号仍是一个需要进一步考虑的问题。Q通过利用从机器到自动机的额外结构，可以证明：• 行为良好的组件从初始状态Λ生成Λ-自动机，相应的Λ-自动机生成相同的组件语言• 一个有根自动机的向量语言对应于一个正常成分语言，该语言又产生一个有根自动机，其初始状态是ΛΛ。在后一种构造中，出现了关于我们开始时的有根的λ-自动机（M，q）和从相应的分量导出的有根的λ-自动机（Mc，Λλ）之间的关系的问题。给出的答案[27] 在[16]中，它们在强互模拟的意义上是互相似的本节的主要结果总结在下面的定理中。定理3.8设C_n表示所有行为良好的分支的类，签名M，M表示所有有根的n-自动机的类。 然 后 ，S. Moschoyiannis等人理论计算机科学电子笔记141（2005）199215ΣKKK12存在一个上函数σ：M→C，σ[M] =（，V（M））而且，σ[M]=σ[M]MM1 2 1 2其中，表示存在从M到M的1 23.1基于自动机的合成在这一节中，我们简要介绍了自动机的组成。其目的是表明，到目前为止所描述的自动机理论框架确实是组合的。以类似于组件合成的方式，关键思想是组件向量v表示行为产品M1||M2提供它的结果从行为vk的Mk，每个k，同意互补的接口。本质上，过渡关系由（q1，q2）>e （qJ，qJ）如果且1 2e[k]J J仅当对于ea chk，则re[k]/=Λk且qk>q或e[k]=Λk且qk=q。这是表示为qk>>e[k] qJ，eachk。数学好，q1>>eq2（q1>eq2）（e=Λq1=q2）在记法上，用q表示（q1，q2）∈Q1×Q2，从而最近qK 对于qk，每个k，我们可以写q>eqJ，用于复合，这是翻译的组成自动机方面，q>>e[k] qJ，eachk。K K在定义复合的过渡关系时，我们需要考虑两种可能性：i) e（i）/=Λ，i∈I1I2，其中，对于a c h k，ichcae[k]/=Λk，并且来自每个自动机的转换的执行涉及通信。这意味这两个转换必须同时执行，有一个跃迁（q1，q2）>e（qJ，qJ）。1 2ii) e（i）=Λ，alli∈I1 I2，其中c是一个非共同的整数，执行组成自动机之一的转换（用于其中，e[k]=k，k=1或k=2）m可以表示在另一个中的任意跃迁。 因此，复合自动机具有转换（q1，q2）>e（QJ，q2）如果k= 1，并且如果k= 2，则（q1，q2）>e（q1，qJ）注意，当e（i）=Λ，alli∈I1I2时，直到f或e[k]=Λk是可能的，每个k。组合将迫使其余的事件（那些出现在在对应于每个非连接接口的坐标上，I.E. e[k]（i），eachk：i/∈I1I2）可以是相同的，而这显然不需要是一般的情况。因此，对过渡的额外要求结构是，如果e[k]都是非空的，那么它们必须有一些非空的216S. Moschoyiannis等人理论计算机科学电子笔记141（2005）19912空的坐标。把上述概念结合起来，我们现在可以给出合成的正式定义。定义3.9设M1=（Q1，>）和M2=（Q2，>）是k-机器，k= 1， 2，其中k1↓ k2，设k 1 = k1↓ k2。定义M1||M2=（ Q1×Q2，>），其中> Eq（ Q1×Q2）× Eq×（Q1× Q2）由q>eqJ给出• q>>e[k]qJ，对于eachk• Ife（i）=Λ，alli∈I<$1<$I<$2，nei there[1]=Λ<$ 或e[2]=ΛΛ。上述定义中的第（1）点指的是上文讨论的情况i）。点(2)涉及情况ii），并且表示了另外的要求，即组合不强制另外独立的列向量必须是同时的。我们的目标是证明所提出的自动机理论框架是合成的，为此，我们需要建立自动机的合成（遵循定义3.9）本身就是一个自动机。首先，我们需要考虑的兼容性，在各自的过渡的自动机。关于定义3.9之前的讨论，我们关注的是涉及沟通的情况在这种情况下，对应的部件具有（至少一个）互补的接口，因此，它们的分量向量应该在相应的非空坐标上一致。我们可以正式地表达这一点，写作u1u2i<$i∈I<$1<$I<$2：u1（i），u2（i）/=Λ<$u1（i）=u2（i）此外，我们可以将机器的事件（转换）集定义为E（M）={e∈E<$|<$q∈Q：q>e}因此，我们现在有，在所有非空的公共坐标上，e 1 e 2 i ek一致。因此，“"并不适合这样的情况，比如，e1（i）=Λe2（i）/=Λ，i∈I<$1<$I<$2。下面的定义通过暗示如果两个转变具有至少一个非空公共坐标，同意，那么对于它们的所有公共坐标都必须是这种情况定义3.10设M1和M2是k-机，k= 1， 2，且m1↓ m2。然后，M1，M2是相容的，我们写M1↓M2，如果E1∈E（M1），E2∈E（M2）. e1e2e1↓ e2这给出了我们的自动机理论框架内的兼容性条件。这样做的一个重要结果是，复合自动机的执行向量正是投射在执行向量的组成，即。 （q， q）→u（QJ，QJ）→u[k]QJ，对于一个chk.1 212kk kS. Moschoyiannis等人理论计算机科学电子笔记141（2005）199217我MQM第二，我们需要在成分中的局部并发性和复合自动机的局部并发性之间建立关系我们首先讨论独立性。这是相对简单的证明，行为u，v的复合自动机可以独立地发生，如果他们的投影到组成自动机是独立的。正式地说uindvu[k] indv[k]，each k这允许复合自动机中的并发性根据成分的复合转换关系的转换来定义定义3.11设M是一台机器，q∈Q，e，e∈E∈ E。定义，1 2 Σ1张图片2第一章因德2（现在，我们可以通过以下方式来建立成分中的并发性与复合自动机中的并发性之间的关系：QeIM Fe[k]Q我kf[k]，每个k其中e，f∈E∈M，M1，M2是k-机，k = 1，2，且M = M1，其中k = 1，2，且M = M1，||M2。综上所述，我们已经考虑了一个概念的兼容性之间的过渡组成自动机和相关的并发成分的复合。现在可以证明，遵循定义3.9中给出的构造的自动机的合成本身就是一个自动机。4结论和未来工作我们已经提出了一个基于自动机的形式主义建模组件的可并行的行为，在并发的存在我们还描述了如何组成自动机。事实上，对我们的前自动机组件模型的这种扩展[19，18]允许两种组合方法：生成相应的组件然后组合，或者组合自动机然后从组合自动机生成组件。这两种方法在[26]中被证明是可互换的。进一步的工作组合正在进行中，特别是在自动机组合下保持常态。初步结果正在确认中。从自动机的角度来看，追求组合的双重方面的一个有趣的方面是放松兼容性条件，以确保在组件组合中保持正规性[18]。自动机可以看作是组件的