进程代数语义中的边界穿越跃迁

理论计算机科学电子笔记115（2005）69-88www.elsevier.com/locate/entcs边界穿越跃迁Arnab Ray阿纳·雷1，2部计算机科学，纽约州立大学石溪分校，石溪纽约州11794 -4400，美国兰斯·克里夫兰3部计算机科学，纽约州立大学石溪分校，石溪纽约州11794 -4400，美国Arne Skou4部 丹麦奥尔堡大学，Fredriksbajersvej 7 E，DK-9220 Aalborg摘要本文给出了一个进程代数语义的层次状态机（HSM）的Statecharts片段，其中状态转移允许跨越状态边界。虽然研究人员不赞成促进非结构化建模，但这种转换在实践中被广泛用于对参数化开始状态和条件退出状态进行建模。 这项工作的目的是为HSM开发一个组合语义，它可以与Statecharts的组合语义解释相结合，而不需要边界交叉转换，以便为几乎整个Statecharts语言提供一个组合理论。我们的技术开发包括一个进程代数的HSMs，配备了一个操作语义，一个参数，互模拟是一个同余的代数，一个语法导向的翻译过程的HSMs到进程代数，和代数的方程式公理化。保留字：状态图，进程代数，组合语义，形式化方法1 研究支持通过军队研究奥什切赠款DAAD 190110003和DAAD 190110019和国家科学基金会资助CCR-9988489和CCR- 00980372电子邮件地址：arnabray@cs.sunysb.edu3 电子邮件地址：rance@cs.sunysb.edu4 电子邮件地址：ask@cs.auc.dk1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.09.02970A. Ray等人理论计算机科学电子笔记115（2005）691介绍Statecharts [6]是一种可视化语言，用于指定反应式、嵌入式和实时系统。 这种形式主义用概念扩展了有限状态机 层次结构（状态细化）、并发性和优先级（转换之间的抢占）。Statecharts在软件工程社区中的成功该语言的方言[22]可以在几种商业设计符号中找到，包括ROOM [19]，STATEMATE [8]，StateClockflow [10]和UML [4]。尽管它的语法是透明的，但为Statecharts语言配备一个正式的操作语义已被证明是一个挑战。Pnueli和Shalev [18]给出了该符号的第一个权威的操作语义。然而，他们的方法不是合成的：给定图表的转换不能纯粹从其子图表的转换中推断出来，因此合成推理技术不能用于状态图表。各种研究人员研究了不同的方法来克服这个组成问题，或者通过丰富存储在过渡中的信息[13，20]，或者将过渡重新定义为子过渡序列[11，12]。然而，这些后者的作品通常只考虑不允许边界交叉转换的状态图的子集支持这一限制的论点是，这种转换本质上是“非结构化的”，应该禁止使用。另一方面，跨边界跃迁在实际中应用相当广泛，并且在成分上对它们进行解释仍然是一个重要的开放问题。在本文中，我们通过定义一个进程代数来解决这个问题，其中Statecharts的分层状态机片段可以以结构和语义保持的方式转换。 算法使用从当代编程语言中发现的方法调用和异常处理的概念改编的思想来编码边界交叉转换。互模拟被证明是这个代数的一个同余，我们的翻译是结构保持的，因此，我们的语义是合成的。对于进程代数，给出了互模拟等价的公理化，并讨论了我们在设计语言时所做的设计决策我们还简要讨论了如何将该语言与[11]的SPL进程代数结合起来，后者处理Statecharts的基于并发和抢占的特性。最后一部分是我们的结论和未来工作的方向。A. Ray等人理论计算机科学电子笔记115（2005）6971对关闭古德关闭复位bugerr瓦特BAD复位2动机我们在本文中的目标是给一个操作，组合语义的边界交叉转换。组合性的动机是显而易见的：对于一个“可伸缩”的建模语言在过去的十年中，定义语言语义的操作方法也占主导地位，并且由于工具支持的原因，对于建模语言特别重要：模拟器和模型检查器等工具需要为其建模符号提供操作语义D已启用 E已启用Fig. 1.跨界过渡。跨边界转换的必要性可能不太明显，我们将在本节的其余部分讨论这一点。 作为实用程序的说明，在实践中，边界交叉转换，考虑图1中给出的示例Statechart（为了清晰起见，我们简化了传统Statecharts转换标签;特别是，标签不包含动作组件）。该图描绘了作者的个人数字助理（PDA）之一的高度抽象视图，其具有以下行为：其可以被打开，并且如果其正常工作，则其可以被关闭。然而，当机器打开时，有时会发生错误; PDA被禁用，并且在机器重置之前不会对打开或关闭做出响应图1使用两种基本模式对PDA进行建模：第一，以前者为主。这些基本模式中的每一个都具有两个子模式：在D被禁用的情况下，而吴亦凡和吴亦凡，则是一对璧人。 在每一种情况下，第一个子，所提到的模式是封闭模式中的“默认”子模式。当PDA处于D启用的OFF子模式，它可以被接通（接通转换）; PDA然后转换到E启用模式的默认子模式（即GOOD）在这种子模式下，机器可能会被切换到关闭状态，或者可能会出现故障。在后一种情况下，发生到B_AD子模式的转变，其中错误转变然后导致D_ISABLE模式的W_AIT子模式。在此子模式下，机器只有在72A. Ray等人理论计算机科学电子笔记115（2005）69重置.在机器启用的任何时间点，机器可以被重置并移动到DISABLED，其中机器进入默认状态DISABLED。这个例子强调了在系统建模中使用边界穿越转换的主要用途：条件退出和参数化的开始状态。 在范例上标记的过渡是前者：这种过渡意味着，指定模式DISABLE只能通过ON退出，当其子模式为OFF;否则将禁用此退出转换。 标记为err也说明了条件退出现象，但它也强调了如何开始状态可以 因此，这种过渡规定，当通过该转换进入DISABLE模式，开始子模式是由转换本身指定，而不是由默认值（子模式OFF）指定。使用这两种跨边界转换的动机是显而易见的：它们通过支持子模型的更大重用来保持模型简单。在上述情况下，可以避免边界交叉转换，但代价是必须复制E启用模式，以便不同的开始状态可以被指定。 (i.e.会有一个D的版本，其初始子模式）这样的复制是浪费的，并且会导致版本控制问题，因为同一子模型的不同版本必须保持彼此一致。跨越边界的转换是解决这个问题的一个优雅的本文的目标是展示如何组合的操作语义可以给出的形式主义，有边界交叉转换。相关工作有几篇论文考虑了Statecharts的操作语义问题。Pnueli和Shalev [18]定义了Statecharts的参考操作语义。然而，他们的方法是全局性的，因为它需要检查一个Statechart项的整个结构，以便计算其行为。对于大型模型，这是有问题的;在这种情况下，出于效率的原因，人们希望Pnueli-Shalev方程不支持这种方法。这些观察导致其他研究人员使用基于进程代数的各种方法来定义Statecharts语义的组合操作方法[11，13，20]。然而，这些框架不允许跨边界的转换，认为这样的转换是“抽象破坏”，因此不受欢迎。在本文中，我们反对这种观点，并确实表明，边界跨越过渡可以占，同时保持组合性。A. Ray等人理论计算机科学电子笔记115（2005）6973Huizing，Gerth 和de Roever在[9]中给出了一个包含边界交叉转换的Statecharts变体的组合指称语义。他们的方法依赖于使用这些“悬空转换”可以被看作模型的入口/出口点，这也是我们语义中利用的一个概念。然而，它们的语义是基于轨迹的：系统通过从“传入”部分转换到“传出”部分转换的转换序列来建模。当模型是确定性的时，这样的语义是合适的，如早期版本的Statecharts。然而，Pnueli和Shalev的语义允许非确定性，以及纯粹基于跟踪的模型，如[9]中的模型，这是因为无法正确地对基于事件的系统建模中占主导地位的合取非确定性（即Mikk、Lakhnech和Siegel在[15]中发表了关于赋予边界穿越跃迁意义的相关工作。它引入了扩展层次自动机（extended HA），作为一种中间格式，以促进新工具与Statemate环境的链接。与Argos语言[14]（不支持跨边界转换）非常相似，扩展HA通过使用优先级转换来支持跨边界转换。其他形式主义也使用了类似于我们定义的入口/出口点的想法。分离跃迁以定位信息的想法已经在ROOM [19]中使用。在[2]中，Grosu和Zurr定义了一种新的Statecharts类型的语言，具有组合语义和模块化推理。它们还通过将边界交叉转换拆分为入口点和出口点来处理边界交叉转换。然而，他们的语言不包含事件，他们的语义，这是基于跟踪的，有同样的问题，在建模非确定性和合取非确定性的Huizing-Gerth-de Roever的工作。3分层状态机本节介绍分层状态机（HSM），这是一个片段的传统Statecharts。与状态图一样，HSM允许定义具有边界交叉转换的分层状态机;与状态图不同，HSM没有并发性规定，并且转换标签可能只包含简单事件（没有触发器/动作对，没有否定事件等）。在本文中，我们研究了HSMs而不是Statecharts，以研究边界交叉转换;然而，最后，我们讨论了如何将我们的工作与[11]的工作相结合，以获得一个处理这些其他语言特征的复合理论。74A. Ray等人理论计算机科学电子笔记115（2005）69∈≤≤u2u1t2t1S1S23.1HSMs的数量为了形式化HSM的概念，我们首先引入状态框架的概念，它定义了分层状态结构，如图1所示1.一、定义3.1状态标架的集合F是最小集合，使得F时：(i) S是一个有限的、非空的状态集;(ii) sI∈S是起始状态;并且(iii) e：S→F，嵌入函数，是一个部分函数。请注意，F是归纳定义的，并且该定义是良构的，因为F在定义的第iii部分中的出现似乎是协变的。定义的归纳性也确保了循环结构的缺失。直观地说，状态框架包含一组状态和一个开始状态，每个状态又可能包含一个嵌套在其中的状态框架，如嵌入函数所定义的。定义的形式也确保了状态框架内的嵌套结构只能是无限深的，因为归纳定义的例3.2图2用图解的方式描述了状态帧{s1，s2}，s2，.注意e是部分的：e（s1）是有定义的，而e（s2）不是。嵌入函数未定义的状态，如s2，有时在Statecharts术语中被称为基本图二. 一个国家的框架。状态框架将用于定义HSM的状态。为了定义HSM的转移关系，我们引入了状态框架的转移端点的概念在下文中，我们使用·表示列表连接，ε表示空列表， 表示列表上的前缀排序（例如a.b是a.b的前缀，因此在排序中会在它之前）。我们还通过将单个元素列表与它们所对应的元素标识在一起来滥用表示法。包含;所以如果S是一个集合，s也是S，那么我们也把s当作一个列表，它的唯一元素是s。A. Ray等人理论计算机科学电子笔记115（2005）6975⟨⟩l·maxFJ（sJI）ifl∈S且e（l）=FJ=<$S J，sJI，eJ<$如果l∈S且e（l）是unfined，Cu2D一u1aat2S2t1S1B定义3.3状态标架F=S，sI，e的跃迁端点E（F）归纳如下。(i) S.E（F）.(ii) 若e∈S，定义e（s），且LJ∈E（e（s）），则s·LJ∈E（F）。直观地说，transition endoint可以被认为是状态列表例3.4在图2所示的状态框架F中，E（F）={s1，s2，s1·t1，s1·t2，s1·t1·u1，s1·t1·u2}.为了正式定义HSM，我们首先固定一组转换标签L。一个HSM现在由一个状态框架和一个涉及标签和框架的转换端点的转换关系组成定义3.5一个HSM具有形式S，sI，e，~ S，其中：• F=S，S，I，E，是一个状态标架。• ~E（F）×L×E（F）是跃迁关系。图三.一种分层状态机。例3.6Fig. 3包含一个HSM，其状态帧是由图。二、3.2HSMs的操作语义现在，我们通过展示如何将HSM转换为标准的、标记为“转换”的转换系统来定义HSM的操作语义。在做这个定义之前，我们首先引入一个关于状态框架的辅助概念定义3.7设F=<$S，sI，e<$是一个状态标架，且设l∈E（F）。则maxF（l）定义如下。如果l=s·lJ且lJ∈E（e（s）），则f（s）= s ·lmaxF（l）=76A. Ray等人理论计算机科学电子笔记115（2005）69∈ −→ ⊆ ××⟨ −→ ⟩12121 1 1H 12B−→直观地说，maxF（l）通过用初始状态适当地填充l来将l扩展到我们现在给出HSMs的语义如下。定义3.8设H= S，s I，e，~∞是一个HSM，定义F H= S，s I，e~ ∞。则标号迁移系统LTS（H）= SH，SH，H，其中状态集SH，初始状态SH，迁移关系HSHLSH如下给出(i) SH包含F的最大（关于≤）过渡端点：SH={l∈E（F）|n∈E（F）. l≤lJ= lJ}。(ii) sH= maxFH（sI）。(iii) l−→aHlJ如果存在l1≤l，使得l1~lJ1 且lJ= maxH（lJ1）。例3.9用图3给出的H，HF，我们有：SH={s1·t1·u1，s1·t1·u2，s1·t2，s2}sH=maxF（s2）=s2转换关系−→H由以下内容组成。s·t−→as·t−→a一HS2Hs1·t1·u1s1·t1S2·u2−→c−→HS1HS2· t2s1·t1 · u1 −→aHS2s·t·u−→ds·ts1·t1·u2−→Hs2一s·t·u−→s·ts1·t1 ·u1−→ HS1 · t1 · u21 12H123.3组合性从HSM的定义中，很明显为什么复合性是有问题的：虽然HSM的状态是由成分定义的，但边缘关系~是全局性的这就给出了语义转换关系的定义H是一个非合成的变量：特别地，状态的转换不能基于子状态的基本转换来推断。这就是为什么在Statecharts语义的组合处理中没有考虑边界交叉转换然而，第2节中的讨论暗示了语义的组合方法：将状态视为具有进入其内部结构的“入口”和“出口”点。与原子实体不同，边界交叉转换可以被认为是由多个适当连接入口/出口点的“段”组成。关于这些过渡段的信息是D一A. Ray等人理论计算机科学电子笔记115（2005）6977对D1OFFe1古德关闭复位bugerr瓦特BAD复位e2D2局部存储在过程定义中;当组成组件时，过渡段被图图4是图1的重绘图，通过涂黑的三角形明确地显示了入口和出口点。D已启用 E已启用见图4。 入口和出口。下一节在过程代数的背景下形式化这些直觉。具体地说，我们定义了一个包含入口点和出口点概念的进程代数，以及用于“进入”和“退出”进程项的运算符。我们从语义上处理这些概念，本质上将入口点视为类似于“方法声明”，入口就像方法调用，出口点作为异常，出口作为异常处理。我们通过证明互模拟[16]是代数的同余来建立代数的组合性。最后，我们使用这个代数作为一个车辆，通过语法指导的翻译，为HSM的成分语义入口点和出口点的概念已经被用于其他基于图形状态机的形式主义中，最著名的是ROOM [19]和[2]的分层状态机。然而，两者都没有提供这些概念的代数处理，并且ROOM的语义虽然精确，但不是正式的。如前所述，[2]的状态机不包含事件的概念，以及那里的基于跟踪的语义，虽然对于该框架是足够的，但是在存在合取（即，非确定性是基于事件的符号（如HSM）所固有的4一种高速加工机HPA的语法，我们的HSM进程代数，相对于定义HSM时使用的转换标签集L进行参数化，进程标识符的可数无限集合C接下来，我们假设78A. Ray等人理论计算机科学电子笔记115（2005）69CP一BQRQPBCR一(1) Q=（a）P（2）R=b。问(3) P=a。Q+b。R+[c|（4）Q=[c|[C]b. 右）图五. HSM和相关HPA术语a∈L和X∈C。自置居所津贴的条款现可规定如下。P：：=零|X| a.P|P + P（常规CCS）|P[P]（嵌入）|（a）P（切入点）|P（输入）| [a|(Exit点）|[a]（手柄退出）在续集中，我们使用T来表示所有HPA项的集合。4.1了解HPAHPA扩展了常规CCS [16]（即没有并行组合，限制或重新标记的CCS），其中操作符用于将操作员的直观读数如下。术语nil表示不执行任何操作的终止进程，而a.P表示可以执行a.p的进程PQRBP一QA. Ray等人理论计算机科学电子笔记115（2005）6979[⟩行动，成为P。P+P表示进程 X构成了对通过一个条件X = PUP所描述的过程的“调用”。 在P[Q]中，P一直在执行它的操作，直到Q通过执行一个操作“禁用”它;在这一点之后，进程的行为就像Q一样。术语（a）P可以被认为是声明了一个带有主体P的“方法”a，当被调用时，它的行为就像P一样过程P“调用”P中的方法a，导致控制转移到方法的主体。 Process[a|试图“e x it at a“;这类似于rai s ing一个名为A的异常。这种退出/异常的处理程序可以使用P来定义，[操作符用于连接引发异常的进程与它们的处理程序。图5包含了突出显示这些结构背后的HSM直觉的示例。示例（1）示出了（a）和入口点之间的预期对应关系：（a）P允许经由入口点a“附接”到P的转变例（2）显示了另一个进程R如何使用Q请注意，有两个过渡段：一个从R到Q的边界，另一个从该点到P的边界。通过将这些段连接在一起形成完整的过渡。例（3）显示了如何定义退出点。这里P可以演化为Q或R，但它也可以通过出口点c退出。最后，示例（4）展示了如何处理退出点c。这里P定义了一个出口点c，并穿过Q这里要注意的另一件事是[操作符;除了用作4.2HPA的操作语义为了形式化这种语义，我们使用SOS方法[17]。规则包含在图中。六、 作为进程代数中的标准，我们假设存在形式X = P的方程作为进程标识符的约束条件。在讨论规则之前，我们首先要注意到，转换上的标签比HSM上的标签具有更丰富的结构。具体地，除了集合L的元素之外，转变可以被标记为：（a）入口点/方法声明的存在[a|通过抗辩进行抗辩的能力附加到或处理退出/异常的能力。我们使用（L），[L|和[L]表示所有入口、出口和“句柄”的集合，80A. Ray等人理论计算机科学电子笔记115（2005）69a.P−→P一（a）P−→P（一）|一[|−→零[a的|[2014 - 05 - 23]（P）（S1）（S2）（Em1）（Em3）（右）一P1−→P1Ja[a/∈[L|]P1[P2−→P1J[P2（Em2）（进入）（进入）（Ex）（H）见图6。 紧急呼救系统的规则。行动，分别。规则（P）、（S1）、（S2）和（R）是CCS的标准，我们在此不对它们进行评级。规则（Em 1）-（Em 3）定义嵌入运算符的行为。(Em1)规定P1[EM2]P2可以在P2空闲时执行P1的非退出转换，而（Em2）规定该进程可以参与P2的非处理程序转换，其中P1在该进程中被禁用。(Em3)建立了P2可以规则（Entry）规定（a）P使能一个入口点a，而（Enter）则规定a>P可以规则（Ex）和（H）定义了a的行为，a是一个退出点，P能够连接到退出点a。P1−→一 P1JP1+P2−→一 P1JP2J一P1+P2−→2PJ2一P−→P2JJBP1[P2−→JJJ2BP−→P2J2P，[a]2J|一[P1−→P1，P−→P−→PJ，PJ−→（一）BPJJP−→BPJJ[a][aP−→一P−→PJ[X=P]一X−→PJ一P2−→P2J[a/∈[L]一P1[P2−→P2J]A. Ray等人理论计算机科学电子笔记115（2005）698121121注意，规则（Em3）和（Enter）在前提中使用链接：前提中一个转换的目标被用作前提中另一个转换的源。例如以下是图1A中的“修饰的”HSM的编码四、D是一个B LED=n（0FF+（d）. WAIT）[OFF=[d|WAIT=reset. OFFENABLED=GOOD[EOGOOD=bubg. BAD+[e|BAD=[e|DO=[d]n. ENABLE DE0=f的n[e] D是一个B LED+[e]r。D是一个BED1 2 2+复位。残疾使用SOS规则，可以推断存在如下转换。（d2）DISABLE−→bugE启用−→4.3组合性瓦多·巴加·埃奥D是BLED−o→nBAD[EO−e→rr已列入议程的进程代数有一个丰富的互模拟元理论，它是围绕SOS操作定义的。 在[21]中可以找到一个这样的结果，它断言，如果进程代数的SOS规则落入该论文中提出的特定语法格式内，则互模拟等价[16]将是该代数的同余。HPA的SOS规则满足这一标准，因此它立即遵循互模拟是HPA的同余。5将HSM转换为HPA在前面的两节中，我们发展了HSMs和HPA的理论，目的是使用后者来给出前者的合成语义。在本节中，我们通过给出一个基于结构的HSMs到HPA项的翻译来完成这个程序。82A. Ray等人理论计算机科学电子笔记115（2005）69⟨⟩S× ⟨ ⟩ →·⟨⟩J下面的算法将HSM作为其输入，并输出相应的PA项，以及该项中使用的进程标识符声明列表。转换的关键要素是：（1）使用嵌入操作符[a]将一个HSM嵌入到另一个HSM的状态中;（2）使用（a）和a >构造来处理<“传入”边界交叉转换;以及（3）通过a [ a]对“传出”边界交叉转换进行编码|”[10]“一个人的命运。更详细的信息可以在伪代码的注释中找到输入：HSM H=S，sI，e，~ s输出量：其中：• X sI 是一个与sI• E是X形式的HPA声明列表E（S，s I，e）.假设：=Pindexedbys∈存在内射函数f：~ES，s I，eL，给定一个边和一个过渡端点，返回一个唯一的标签。算法Trans（ε，εS，sI，e，~ ε）returnTransAux（ε，εS，sI，eε）end算法Trans/* TransAux负责翻译的参数l在HSM中记录到状态帧的算法TransAux（1， S，SI，e）0.E：=ε/* E是要返回的方程列表 *//* 为S中的每个状态生成方程。* */1.对于每个s∈S，do：2.eO：=nil;/*eO 将是s的“外部部分”的术语3.如果e（s）未定义，则eI：=nil/*eI：4.elseXJ，EJ：= transAux（l·s，e（s））;/* 递归调用 */5.E：= EE;6.eI：=XJ/* 现在处理涉及S中状态的转换。*/A. Ray等人理论计算机科学电子笔记115（2005）6983[··[·[|⟨⟩的|[2014 - 05- 23]7.对于每个t=<$l1，a，l2<$∈~do/* transition源自当前状态的情况8.如果l1=l·s，则9.如果l2=l·sJ，则 f * 非BCT */10.eO：=eO+a.XsJ11.否则，如果l2=l·sJ·lJ2/* BCT进入同级状态 */12.= eO+a。XsJ13.elsee O：= e O+[f（t，l）]|/* 为父节点传出 *//* 转换源自当前状态的子状态的情况14.否则如果l1=l·s·lJ1somelJ1则15.如果l2=l·sJ，则 f * 转换目标是当前状态的兄弟 */16.eO：=eO+[f（t，l·s）<$a.XSJ17.否则，如果l2=l·SJ·LJ2，则/* 转换目标是兄弟的孩子 */18.eO：=eO+f（t，ls）a. XsJelse/* transition is BCT for parent also */19.eO：=eO+f（t，ls）f（t，l）/* 转换进入当前状态时的情况20.否则，如果l2=l·s·sJ·lJ2，则21.如果l，J，2=ε，则 f *，即过渡在s，* f处结束22.eI=eI+（f（t，l·s））Xl·sJ23.eleeI：=eI+（f（t，l·s））f（t，l·s·sJ）>Xl·s·sJod;24.E：=（Xsod;=（e[2009年10月23日]））·E;25.returnXsI，E结束算法TransAux翻译的正确性现在我们概述翻译过程正确性的证明。我们的一般方法将表明，一个可以建立一个bisimulation-like的关系之间的HSM状态和HPA的条款，涉及的HSM初始当然，HPA项能够进行HSM状态所不能进行的跃迁：特别地，由（a）、a和a标记的跃迁不能被HSM状态匹配。因此，我们构建的关系将只考虑L的元素; HPA项中的其他转换可以被认为是组合性所需的我84A. Ray等人理论计算机科学电子笔记115（2005）69⟩H定理5.1设H= εS，sI，e，~ε是一个HSM，其中LTS（H）= εSH，sH，−→H和T rans（H）=P，EHPA项和我们算法构造的支持声明。 则存在R <$SH×T使得s HRP，且使得每当sR t，则对于任何a∈ L：(i) 如果s−→asJ，则n存在re，则tt−→atJ和sJRtJ。(ii) 如果t−→atJ，则n存在re，s sJ，则ts−→asJ和sJRtJ。H6HPA公理化虽然我们已经提到HPA作为一个进程代数，我们还没有赋予它任何代数结构。在本节中，我们通过给出HPA的有限（即无标识符）片段的合理而完整的等式公理化来解决这个问题。另一个与进程代数的SOS元理论明显相关的结果可以在[1]中找到;在那篇论文中，给出了一种从SOS规则自动生成互模拟的声音和完整公理化的方法。然而，HPA的规则不在该论文中考虑的格式范围内，因此我们不能使用该作品。表1列出了公理;我们在这里简单地对它们进行评论。(A1)- （A4）是CCS的标准么半群和吸收定律。其余的方程被设计为从项中消除[和的出现：其中的关键是（Em5），它解释了出口点和出口处理程序之间的交互，以及（En4），它捕获了入口点之间的交互输入操作。使用标准技术可以证明这些定律的合理性和完整性[16]。合理性来自于适当的双模拟的构建。完备性依赖于规范句法形式的定义;这些形式的定义可以从表中公理（EM 3）-（EM 6）的序言中r的定义中直观得出。虽然费力，但细节是常规的，被省略了。7讨论在本节中，我们提出了一些我们在开发本文中的工作所采取的决定的理由。我们还概述了HPA如何与[11]中给出的进程代数相结合，以获得具有边界交叉转换的Statecharts的组合语义理论首先，人们可能想知道为什么我们选择间接地给出HSM的组合语义，通过转换成进程代数。两A. Ray等人理论计算机科学电子笔记115（2005）6985Σ我JK(A1)x+y=y+x（A2）x+（y+z）=（x+y）+z（A3）x+nil=x（A4）x+x=x(Em1)nil[x]=x（Em2）（x+y）[xz]=（x[xz]）+（y[xz]）在（Em 3）-（Em 6）中rJ=αi. xi+（bj）yj+[ck|r=rJ+[dl<$zlL(Em3)（a.x）[b]r = a. （x[r]）+rJ（Em4）（（a）x）[r]=（a）（x[r]）+rJ（Em 5）（[a|）[mr=rJ+mdl=azl（Em6）]（[a<$x）[r]=[a<$（x[r] ） +rJ(En1)nil=nil（En2）a>（b.x）=nil（En3）a>（x+y）=（a>x）+（a>y）（En4）a>（a）x=x（En5）（b）x=nil ifa/ =b（En6）[b]|= nil（En7）（[b]x）=零表1互模拟的HPA公理化在作出这一决定时，考虑到了实际和哲学问题。一方面，这项工作源于对战场医疗设备（自动复苏器）的控制器进行建模和验证。 在该研究中，我们使用的状态机模型具有边界交叉转换，但我们使用的验证工具（CWB-NC [5]）只有文本界面。因此，我们必须为边界跨越转换提出一种文本语言，而这种符号在这里的工作中发挥了重要作用。然而，在更概念化的层面上，组合性是进程代数的内在特征;当试图为一个新的建模语言特征定义一个(In在我们的例子中，我们得到了一旦一个人了解了86A. Ray等人理论计算机科学电子笔记115（2005）69的|[2014 - 05 - 23]⟩基本的概念问题，然后可以探索更直接的语义帐户。另一个问题涉及进程代数HPA的设计。总的来说，有三个主要的考虑因素指导了我们对这种语言的开发：HSMs应该易于在语言中编码;操作和方程理论应该是干净的;语言应该易于与[11]中的进程代数结合，它被用作为没有边界交叉转换的Statecharts提供组合语义的工具。其他考虑因素，如如何处理各种类型的非决定论，一般都放在一边。 例如，该过程（（a）b.nil+（a）c.nil）与进程b.nil+c.nil是双相似的，尽管有些人可能会争辩说，在a > ···项的主体中存在两个然而，我们在本文中的需求并不取决于对这种内部选择的反映，我们选择不试图将它们强行纳入语言。类似的考虑支持我们对异常/退出点（a）和退出处理（a P）的处理。当前形式的语言要求处理程序立即处理退出;特别是在过程（[a|[nil）[[apa-handler不能处理a-exit，因为中间有nil。为了翻译HSM，这是没有问题的，而且由于这种设计选择，这种语言的公理化确实稍微简单一些然而，人们可以想象重新设计语言以允许更灵活地处理异常/退出（例如，消除SOS规则（Em 1）和（Em 2）中的边条件[）;结果公理化，然而，更复杂。在结束本节时，我们将评论如何丰富HPA，以便对Statecharts的其他功能（包括并发和抢占）进行建模。在[11]中，引入了进程代数SPL，以便为没有边界交叉转换的Statecharts提供组合语义SPL的语法是根据一组标签（事件名称）参数化的;它与HPA共享一些操作符（+，递归），有一些操作符在HPA中根本不存在（发射，并行组合，限制，延迟），还有一些操作符与HPA中的操作符相似，但在关键方面有所不同（前缀，禁用，启用）。 操作语义通过 一种转换关系，标记有两组事件：已发出的事件和必须从环境中消失的事件。将HPA合并到SPL中很简单：添加入口、输入、退出和句柄操作符;A. Ray等人理论计算机科学电子笔记115（2005）6987使用SPL的prefixing概念;修改并行组合和限制的定义，使其对HPA转换标签敏感;修改SPL禁用操作符，以引入退出处理功能。 由于SPL和HPA的转换标签是不相交的，因此修改并不困难。然而，最终的语言有点大，因此我们在本文中将技术开发集中在HPA8结论和今后工作在本文中，我们已经开发了一个组合的操作语义分层状态机（HSMs）。HSM丰富了传统的状态机，具有将状态机嵌入其他机器的状态中以及跨状态边界的转换的能力传统的智慧一直认为，这样的边界跨越过渡本质上是非组成的，我们证明，这不需要的情况下。语义依赖于一个结构保持翻译成一个进程代数，互模拟等价是一个同余。这最后一个事实确保了HSM的语义也是组合的。我们也给出了一个健全的和完整的公理化的进程代数互模拟等价。作为未来的工作，我们希望研究将我们的想法纳入更丰富的演算中，例如[11]的Statecharts进程代数，其中包括对Statecharts中不存在于HSM中的其他构造的处理。我们还认为[12]中的思想可以被采用到本文中，以便为高速移动提供一个直接的组合语义，而不是像本文中所做的那样引用[1] 阿塞托湖，B. Bloom和F.Vaandrager，将SOS规则转化为方程，信息与计算111（1994），pp.1-52[2] 巴尔河和R. Grosu，Modular Refinement of Hierarchic Reactive Machines，Principles ofProgramming Languages（POPL）390-402（2000）。[3] Bolognesi，T.和E. Brinksma，Introduction to the ISO specification language LOTOS，Computer Networks and ISDN Systems14（1987）. 25比59[4] Booch，G.，I. Jacobson和J. Rumbaugh，[5] 克里夫兰河和S.Sims，Generic tools for verifying concurrent systems，Science of ComputerProgramming41（2002），pp.39比47[6] D.Harel，Statecharts：A Visual Formalism for Complex Systems，Science of ComputerProgramming，8（1987），pp. 231-274。[7] Harel，D.和A.Naamad，StateCharts的STATEMATE语义，ACM软件工程与方法学报5（1996），pp.293-333.88A. Ray等人理论计算机科学电子笔记115（2005）69[8] Harel，D.和M. Politi，[9] Huizing ， C. ， R. Gerth 和 W. de Roever ， CAAPDauchet 和 M. Nivat ， editors ， CAAP ，Lecture Notes in Computer Science299（1988），pp.271-294。[10] 股份有限公司、 T. M.，http://www.mathworks.com/products/stateflow网站。[11] Luettgen，G.，M. von der Beeck 和R.Cleaveland，Statecharts via process algebra ，in：J.Baeten和S.Mauw，编辑，第十届国际并发理论会议（CONCUR '99），计算机科学讲义1664（1999），第1664页。399-414[12] Luettgen ， G. ， M. von der Beeck 和 R. Cleaveland ， 状 态 图 语 义 的 组 合 方 法 ， 在 ： D 。Rosenblum ， editor ， Eighth International Symposium on Foundations of SoftwareEngineering（2000）. 120比129[13] Maggiolo-Schettini，A.，A. Peron和S. Tini，Equivalences of Statecharts，in：U. Montanari和V.Sassone，编者，第七届国际并发理论会议（CONCUR687-702[14] Maraninchi，F.，Argos语言：自动机的图形表示和反应系统的描述，IEEE视觉语言研讨会（1991）。[15] Mikk，E.，Y. Lakhnech和M.张文，以阶层式自动机为模型之状态图，国立台湾大学计算机科学研究所硕士论文[16] 米尔纳河，[17] Plotkin，G.，操作语义学的结构方法，技术报告DAIMI-FN-19，奥胡斯大学计算机科学系，奥胡斯，丹麦（1981）。[18] Pnueli，A.和M.Shalev，What is in a step：On the semantics of statecharts，in：T.Ito和A. R. Meyer，editors，Theoretical Aspects of Computer Software：Proc. of the InternationalConference TACS244-264。[19] Selic，B.，G.林志玲，[20] Uselton，A.和S.Smolka，A co