基于状态的关系数据细化模型及其内部操作的模拟规则推导 - 2007论文总结.

理论计算机科学电子笔记187（2007）35-53www.elsevier.com/locate/entcs与内部操作的约翰·德里克1英国谢菲尔德大学计算机科学系Eerke Boiten2英国肯特郡坎特伯雷肯特大学计算机实验室摘要基于状态的语言（如Z）中的数据细化是使用关系模型根据抽象程序的输入输出行为来定义的。向下和向上模拟形成了一种可靠的、共同完整的方法，用于验证关系数据的细化。并发上下文中的细化，例如，在进程语义中发现的，采取许多不同的形式。通常，这是基于观察的概念，例如，系统准备接受或拒绝哪些事件。并发精化关系包括跟踪精化、故障-发散精化、就绪精化和互模拟。在本文中，我们调查最近的结果链接关系模型的细化过程代数模型。具体来说，我们详细介绍了关系框架中的变化如何导致关系数据细化与过程语义中的跟踪分歧，单例故障和故障分歧细化相对应。然后，我们扩展这些结果，显示内部操作的效果可以被纳入到关系模型。因此，可以导出故障-发散细化的模拟规则。关键词：数据细化，Z，模拟，进程代数语义，故障-发散细化，内部操作。1介绍受规范语言的精化和集成的理论比较的启发，最近人们对将关系数据精化的分类模型与并发过程中产生的过程精化关系1电子邮件：J. dcs.shef.ac.uk2电子邮件：E.A. kent.ac.uk1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.08.04336J. Derrick，E.Boiten/Electronic Notes in Theoretical Computer Science 187（2007）35上下文本文的目的是调查和推广这些结果。特别是，我们推导出包含内部操作的关系数据规范的模拟规则。关系细化模型出现在诸如Z [19]等基于状态的规范语言的规范被认为是定义抽象数据类型（ADT），其中程序（操作序列）可以被解释。在这种情况下，细化被认为是程序行为上的子集关系，其中被认为可见的是输入/输出关系。因此，如果对于每个程序和输入序列，C产生的输出是A也可能产生的输出，则ADTC精化ADTA模拟已成为使改进易于验证的公认方法[10]。理论背景在[10]中给出，它们在Z中的使用的例子在[21，11]中给出在过程代数中发现了另一种模型，其中不同的过程语义会导致不同的细化关系。例如，在CSP中，可以使用跟踪细化、故障细化或故障-发散细化[17]。在CCS中，通常使用互模拟[16]，而在LOTOS约简中，定义了扩展和一致性[3]。[20]中给出了许多重要的细化关系的综述这些关系往往是由一个理想化的机器的描述，其中一个操纵系统，并观察其行为的动机。不同的并发细化关系通过改变该机器的功能而产生。为了理解精化的性质和结构，以及提供一种将规范语言及其开发方法结合起来的方法，有必要理解数据和过程精化之间的对应关系。与这两种范式相关的工作包括Josephs [15] 、 He [14] 、 Woodcock 和 Morgan [22] 、Bolton 和 Davies [5， 6] 、Derrick 和 Boiten [2 ， 12] 以 及 Schnei-der [18] 。 由 于 Josephs [15] ， He [14] ，Woodcock和Morgan [22]定义了模拟规则和失败-分歧细化之间的基本对应关系Bolton和Davies [5，6]，Derrick和Boiten [2，12]和Schneider [18]最近的工作研究了关系模型和过程语义之间的直接对应关系，并包括对输入和输出的特殊考虑，这引入了一些微妙之处。本文件有两个目的。首先，我们调查了现有的工作，将关系模型的细化与其过程代数对应物联系起来。第二，我们通过展示如何将内部操作的结果合并到关系模型中来扩展这些结果（特别是[12关系模型和过程模型之间的对应关系可以通过在每个ADT的CSP中定义“对应过程”，然后导出过程语义来研究[18][19][20][21][22][23][24][25][ 26][27][28][29无论哪种方式，都可以为ADTA给出过程语义[A]。主要目的是得出以下形式的结果：在关系模型X中，A ±数据C当且仅当[A]] ±ps[[C]]。J. Derrick，E.Boiten/Electronic Notes in Theoretical Computer Science 187（2007）3537其中±data表示关系数据细化的一些变化，±ps表示由给定过程语义诱导的细化关系，后者通常作为CSP的语义模型给出，例如，跟踪-分歧或失败-分歧。关系模型中的变化包括对作为部分关系给出的操作的解释，以及所做的观察对于部分操作，通常有两种可能的前者表示一种契约方法--在前提条件之外，任何事情都可能发生- 后者是一种行为方法-在一个前提条件（警戒）之外，什么也不会发生。在关系模型中进行的观察通常限于ADT的输入/输出，然而，这些可以扩展到包括例如给定状态下的拒绝。因此，我们得到如下结果：在具有标准观测值的非阻塞关系模型中，A ±数据C当且仅当[A]是由[C]限定的迹-发散]。这个特殊的结果是由于施耐德[18]。阻塞模型中的一个版本是由Bolton和Davies提出的，其中引入的流程语义是单故障模型。Derrick和Boiten [12]展示了需要哪些额外的观测来诱导失效-发散修正，并推导出相应的模拟规则。在本文中，我们扩展了这些结果的考虑内部（不可观测）的操作，特别是导出模拟规则的故障发散细化。这是对以前方法的重要概括，特别强调了由于无界内部演化及其对模拟规则的影响而导致我们推导了阻塞模型的向下和向上模拟条件，因此，关系精化可以用作检查具有内部操作的并发进程的故障-发散精化的基础因此，使用模拟的细化验证现在可以应用于所有CSP，包括隐藏。本文件的结构如下。第2节强调了背景材料的关键要素，并请其他来源提供全部细节。第3节概述了关系和过程语义中的相关细化第4节提供了阻塞模型到内部操作的扩展，我们将在第5节结束。2背景2.1Z的关系修饰有关关系设置中抽象数据类型精化的全部细节以及如何使用它来开发Z的精化理论，无论是在阻塞还是非阻塞方法中，请参见[11]或本文的完整版本[13]。抽象数据类型包含一个（隐藏的）状态空间、初始化、操作和终结。一个程序对应于一系列的操作，初始化和finalisation，表示一个关系表征观察，38J. Derrick，E.Boiten/Electronic Notes in Theoretical Computer Science 187（2007）35可见状态空间上。抽象数据类型之间的细化的定义要求（关系）包含所有程序的此类观察，即，减少非决定论。向下和向上的模拟通过考虑单个操作形成了证明精化的合理和完整的方法关系精炼理论有两个同样有效的分支：部分关系和整体关系。在这里，我们只考虑总关系版本操作通常由部分关系描述，需要通过向观察空间添加数字元素来将其嵌入到总关系中（“总计”）。这也有两种变体，有相应的解释。分块累加只将操作域之外的状态与一个数值联系起来非阻塞累加将这些状态与所有可能的状态联系起来，包括一个有限状态，表明任何结果都是可以接受的，从而引入了可以在细化中减少的非确定性。在这两种方法中，部分运算的模拟规则都是通过删除对数字元素的引用而从整体运算的模拟规则中导出的。Z中的规范提供了额外的复杂性，即操作可能有输入和输出。这在关系模型中通过将输入和输出的序列添加到可见和隐藏状态来适应，其中输入在初始化时提供，并且所有输出在最终化时观察。每个操作消耗一个输入并产生一个输出。以下定义，由Z数据类型（不包含显式终结）引起的关系终结，完全包括在内，因为它将在本文的其余部分进行更改Fin=={State;is：seqInput;os：seqOutput·（is，os，θState）›→（θ State，os）}以下Z中的细化的（标准）定义来自上述构造。定义2.1（Z中的标准向下模拟）给定Z数据类型A=（AState，AInit，{AOpi}i∈I）和C=（CState，CInit，{COpi}i∈I）。AState上的关系R是在非阻塞状态下从A到C的向下模拟。模型如果CStateJ·CInit对于所有i∈I，输入和输出：CState·preAOpiR preCOpiCSTATE;CSTATE;CSTATEJ;· preAOpiRCOpiASTATEJ·RjAOpi在阻塞模型中，最终条件（CSTATE;CSTATE;CSTATEJ;Input;Output·RCOpi输入ASTATEJ·RjAOpiJ. Derrick，E.Boiten/Electronic Notes in Theoretical Computer Science 187（2007）3539定义2.2（Z中的标准向上模拟）给定Z数据类型A=（AState，AInit，{AOpi}i∈I）和C=（CState，CInit，{COpi}i∈I）。 然后，AState上的关系T是从在非阻塞模型中，如果CSTATE·CSTATE·TAStateJ;CStateJ·CInit对于所有i∈I：CState·AStateJ;CState;CStateJ·（COpiTJ）（AState·T（preAOpiAOpi））在阻塞模型中，正确性条件变为AStateJ;CState;CStateJ·（COpi2.2工艺改进一种与之相反的细化观点是通过系统的过程代数描述所实现在那里，不是一个全局状态上的关系代表一个程序，而是记录事件的痕迹（本质上是所有终止程序的记录）。CSP有许多语义模型，每一个都有自己的细化关系。失败-分歧语义CSP的标准语义是在[9，8，17]中开发的失败-分歧语义一个过程是由三重模型（A，F，D）其中A是它的字母表，F是它的失败，D是它的分歧。一个过程的失败是成对的（t，X），其中t是一个有限的事件序列，进程可能经历的事件，X是进程在经历t之后可能拒绝执行的事件的集合。也就是说，如果进程在经历了t之后处于一个只允许它经历X中的事件的环境中，它可能会死锁。过程的分歧是事件的序列，在此之后，过程可能经历内部事件的无限序列，即。活锁失败和分歧是根据过程的字母表中的事件来定义的。具有字母A的过程的失败是一个集合FA ×PA这样，一些属性成立：一个进程可以经历的事件序列形成一个非空的、前缀封闭的集合;如果一个进程可以拒绝集合X中的所有事件，那么它可以拒绝X的任何子集中的所有事件;一个进程可以拒绝任何不能作为下一个事件发生的事件。具有字母表A和故障F的过程的发散是集合D的集合F，使得：40J. Derrick，E.Boiten/Electronic Notes in Theoretical Computer Science 187（2007）351t1∈ D <$t2∈A<$t1-t2∈ Dt∈ D <$X <$A<$（t，X）∈F这些概念抓住了这样一个思想，即在有限时间内不可能确定关于发散过程的任何东西因此，不能排除它可能发生进一步事件的可能性。换句话说，发散过程表现为混沌。失败-分歧语义引入了根据失败和分歧定义的细化排序[8]。过程Q是过程P的精化，记为P±fdQ，如果F（Q）<$F（P）且D（Q）<$D（P）。还有两个其他的语义模型CSP相关的本文。traces-divergences语义traces-divergences语义就是去掉了拒绝信息的failure-divergences语义。过程P现在由（A，T，D）建模，其中T是P的迹。它是从失败中获得的-通过将轨迹定义为T（P）=={tr|（tr，n）∈ F}.迹-发散语义诱导了一个细化排序，其中P±tdQi ∈T（Q）∈ T（P）和D（Q）∈ D（P）。Bolton [4]（并在[5，6]中发表）使用CSP的单例故障语义来定义与阻塞数据细化的适当对应。本质上，单例失败语义是一种失败语义，其中拒绝集的基数最多为1。具体来说，一个过程现在可以用（A，S）来建模，其中S <$A<$×P1A（P1形成cardinality at most one）。如果P是一个用stop、→、H、Q和A表示的过程，则它的单点失效是由它的失效给出的明显投影，即S（P）= F（P）<$（A <$×PA）.这不适用于包含隐藏的进程。单例故障语义诱导了一个细化排序，其中P±sfQi ∈S（Q）∈ S（P）.显然，失败发散细化比迹发散细化更强，即P±fdQ<$P±td Q. 对于无发散过程，我们有P±sfQ<$P±tdQ，对于无发散基本过程（即，用stop、→、H、Q和表示的），我们有P±fdQ<$P±sfQ。单例故障与其他语义模型的关系在[20]和稍后的[7]中讨论。3相关数据和流程优化上一节概述了精炼的标准关系理论，并简要提到了相关的基于过程的定义。现在，我们将对最近有关关系细化和过程细化的下表总结了这些通信。J. Derrick，E.Boiten/Electronic Notes in Theoretical Computer Science 187（2007）3541关系细化过程模型引文非阻塞数据细化迹发散施耐德[18]使用确定性输出单例故障博尔顿和戴维斯[5，6]阻塞数据细化进程单例故障和输入过程博尔顿和戴维斯[5，6]模块化数据参考，适用性增强，但无输入/输出失败约瑟夫斯[15]使用扩展finalisations故障-分歧德里克和博伊滕[2，12]非阻塞数据参考，具有扩展finalisations，但没有输入/输出故障-分歧德里克和博伊滕[2，12]Bolton、Davies和Schneider都考虑了数据细化的标准定义，并通过定义2.1和2.2中给出的模拟（以Z表示）进行了验证。Derrick和Boiten的3.1非阻塞数据精化和踪迹发散语义受Bolton和Davies [5，6]工作的启发，Schneider [18]表明，非阻塞数据细化对应于过程语义中的跟踪发散细化。为了说明这一点，他直接将ADT转换为CSP，并在最终的CSP流程上使用跟踪-分歧语义与所有方法一样，首先证明了没有输入和输出的ADT的结果，然后扩展到一般情况。对具有输入和输出的ADT的扩展（Schneider称之为Bolton之后的通信数据类型）涉及到将输入和输出序列嵌入到与上述类似的全局状态中。对于这样的ADT，ADTA到CSP处理过程（A）的转换由下式给出：process （ A ） ==Hs∈State ， （ n ， s ）∈Init·ProcA（s）ProcA（s）==Qi∈I，in∈Input，（in，，s）∈domAOpi·HsJ∈State，out∈Output，（in，out，s）›→（in，out，sJ）∈AOpi·奥普岛in. 输出→过程A（sJ）QQi ∈ I，in ∈ Input，（in，，s）/∈ dom AOpi· Hout∈Output·AOp i. in. out→div请注意，这里的div是发散的CSP进程，它确保在操作的前提条件之外调用操作后，所有事件下面的（在本文中使用的符号），然后证明。定理3.1在非阻塞模型中，A±dataC当且仅当process（A）±tdprocess（C）。42J. Derrick，E.Boiten/Electronic Notes in Theoretical Computer Science 187（2007）353.2阻塞数据细化和单例故障语义Bolton在[4]中以及Bolton和Davies在[5，6]中讨论了数据细化与单例故障语义[20]模型之间的关系。他们考虑了阻塞和非阻塞关系数据类型语义，并且像Schneider一样，将ADT直接转换为CSP。对于阻塞模型，将ADTA转换为CSP进程过程b（A）由下式给出（为了一致性，使用已经引入的符号）：过程b（A）==Hs∈State，（n，s）∈Init·PA（s）PA（s）==Qi∈I，in∈Input，（in，，s）∈domAOpi·HsJ∈State，out∈Output，（in，out，s）›→（in，out，sJ）∈AOpi·奥普岛in. out→PA（sJ）可以看出，该过程的启用与Schneider的相同，然而，在其前提条件之外调用操作的后果现在不是发散，而是因为我们处于阻塞模型中，所以只是无法执行与该操作相关联的任何因此，这正确地反映了分块模型的预期含义。对于具有确定性输出（或无输入/输出）的ADT，如下所示。定理3.2在阻塞模型中，对于具有确定性输出（或无输入/输出）的ADT，A±数据C当且仅当过程b（A）±sf过程b（C）。包含非确定性输出使所需的过程语义复杂化，并且需要额外的约束来消除阻塞数据细化。为了做到这一点，引入了进一步的部分翻译，称为inputProcess，它提供了特定输入在域中时的特征。对于阻塞模型，这被定义为：输入过程b（A）==Hs∈State，（n，s）∈Init·PA（s）P A（s）== Qi∈I，in∈Input，（in，，s）∈ dom AOpi· HsJ∈State|（输出∈输出|（in，，s）<$→（，out，sJ）∈AOp i）·奥普岛in→PA（sJ）可以看出，这与过程b相同，除了输出是不可观察的。阻塞数据细化可以被证明等价于过程和输入过程的单例失败细化那就是：定理3.3在阻塞模型中，A±数据C当且仅当进程b（A）±sfprocess b（C）和inputProcess b（A）±sfinputProcess b（C）。J. Derrick，E.Boiten/Electronic Notes in Theoretical Computer Science 187（2007）3543有两个推论值得注意。首先，这种特征化等价于检查输入流程的单例失败和流程的跟踪细化。二是过程b（A）±fd过程b（C）过程A±数据C在阻塞模型中。Bolton和Davies也考虑了非阻塞模型。然而，所使用的相应工艺与Schneider的工艺不同。具体地说，他们通过以下方式定义过程nb：过程nb（A）==Hs∈State，（n，s）∈Init·QA（s）QA（s）==PA（s）Q（（Qi∈I，in∈Input，（QinQ，Q inQ，s）/∈domAOpi·HsJ∈State，out∈Output·AOp i. in. 出→混沌）H停止）其中混沌==（Hi∈I，in∈Input，out∈Output·AOp i. in. （out→Chaos）H停止是一个非发散的过程，它可以执行任何事件，也可以拒绝任何事件。在过程QA中，下止点用于表示非终止的行动。利用该相应的过程，得到类似的结果（即，数据细化对应于单例，而不是失败-分歧细化）。这种非阻塞翻译在关键方面与Schneider定义的翻译不同。特别是，使用混沌和停止来模拟非终止似乎比使用显式发散更不自然地嵌入非阻塞。3.3定义与失败-分歧细化Derrick和Boiten [2，12]受到Bolton和Davies工作的启发，探索了关系细化需要哪些附加条件，以实现与失败-分歧细化的对应。事实证明，对拒绝的明确观察是必要的成分，由于最终化决定了什么是可观察的，这涉及到对所使用的最终化的概括3.3.1基本建设为了向数据类型的观测值添加拒绝，所使用的finnalization从{State·θState <$→ E}一般化为{State·θState<$→E}。 E将是一组操作名称，表示可能在在这个国家，最终的结果是。操作是在I上索引的，这些操作被用作操作名称的集合拒绝E是最大的44J. Derrick，E.Boiten/Electronic Notes in Theoretical Computer Science 187（2007）35999给定状态下的拒绝：{i：I|在Op i之前}。 完整的嵌入如下3.定义3.4（拒绝嵌入）拒绝解释中的ADT（State，Init，{Opi}i∈I）嵌入关系模型中，如下所示。全局状态G是PI，终结由下式给出：Fin =={State; E：P I|（i∈E·<$pre Op i）·θ状态<$→E}初始化由下式给出：初始化=={初始化;E：PI·E<$→θ状态J}局部状态和操作的嵌入保持不变。Derrick和Boiten得出了两个结果。第一个问题是说明这种扩展终结的模拟规则的结果是什么。第二个是显示与失败-分歧细化的对应关系。3.3.2模拟规则相关的向下和向上模拟规则[11]包含了最终化的条件。具体来说，对于向下模拟，RoCFinCFinran（domAFinDR）domCFin，对于向上模拟，CF输入到AF输入2016 - 05- 25 01：01：02（|{c}|）dom AFin <$c ∈ dom CFin对于扩展的最终化，在观察到拒绝的情况下，总是满足第二个向下模拟条件，第一个条件相当于标准向下适用性条件。在拒绝的情况下，2.1表示正确的形式化。对于一个向上的模拟，CSTATE：CSTATE·T（|{c}|）dom AFinc ∈ dom CFin总是满足的，但是，CFinToAFin导致从定义2.2到(1)CState·正如[12]中所指出的：要求我们必须考虑每个操作的抽象和具体状态对。另一方面，终结条件要求，对于每一个抽象的状态，我们都能找到一个具体的状态，使得所有抽象操作的前提条件都蕴含着它们的具体对应物的前提条件3由于finalization的结果类型和初始化的输入都应该是G，初始化将采取一组操作作为其输入以保持一致性。J. Derrick，E.Boiten/Electronic Notes in Theoretical Computer Science 187（2007）35453.3.3对应于故障-分歧细化Bolton和Davies以及Schneider都通过首先定义CSP中的“对应进程”，然后使用该进程的适当语义来定义进程语义然而，Derrick和Boiten直接定义了过程语义。差异并不重要，只要结果是一致的。在没有输出的情况下，两种模型中的迹线、故障和发散都可以很容易地定义，对于存在输入和输出的结构，请参见[1]。阻塞模型跟踪产生于在其保护中定义的操作序列。拒绝表示不可能在其前提条件之外应用操作。此外，没有分歧，因为每个操作要么被阻塞，要么给出一个定义良好的结果。非阻塞模型由于没有阻塞操作，因此每个跟踪都是可能的：阻塞模型中出现的跟踪，以及发散之后的任何其他跟踪。在发散之后没有拒绝，因为没有操作被阻塞，它要么给出一个定义明确的结果，要么导致发散。然而，现在有分歧，这是由于在其前提条件之外应用操作而产生的然后证明以下内容。定理3.5在非阻塞模型和阻塞模型中，具有扩展finalization的关系精化对应于失败-发散精化。3.4讨论我们已经看到，在非阻塞和阻塞模型中，都需要设置额外的限制（即，观察），以便在过程语义中实现故障-分歧细化为什么会这样，也许最好通过一个例子来说明。非阻塞模式。我们已经看到，如果没有输入/输出，非阻塞数据细化相当于跟踪发散细化。然而，值得注意的是，这并不意味着数据细化可以克服CSP跟踪模型的弱点。具体而言，尽管跟踪细化通常被认为太弱，因为死锁行为停止细化所有进程，但这种行为不是ADT的可行转换。也就是说，没有ADT会有相应的进程停止，因为非阻塞模型允许所有跟踪，因为没有操作被拒绝。此外，与跟踪细化不同，细化排序没有底部，因为所有操作都是确定性的和完全定义的所有ADT在此框架中没有严格的细化没有输入/输出，非阻塞数据细化实际上也等同于故障-发散细化。要看到这一点 ， 请 注 意 ， 在 没 有 输 出 的 情 况 下 ， 所 获 得 的 进 程 语 义 标 识 了 traces-divergencesrefinement和 failures-divergencesrefinement，即 进程（ A）±td进程（C）i进程（A）±fd进程（C）。 这仅仅是因为在流程语义中没有拒绝（除了分歧之后的那些），因为拒绝只会由于输出的存在而出现46J. Derrick，E.Boiten/Electronic Notes in Theoretical Computer Science 187（2007）35书电视TVTESF不不TVF豪华书套间EST一个C图1.一、非阻塞，无输入/输出=跟踪-发散和故障-发散考虑图1，在这个和随后的例子中，我们通过简单的LTS来定义它们，这些LTS表示ADT在这两个规范具有相同的迹线和发散，因此是数据细化等效的。没有拒绝，因此它们也是失败-分歧等价物。然而，请注意，阻塞模型所需的更强的适用性条件在这里并不成立-例如，对于stateensuite，任何抽象状态都不具有i：I·T差异（即，为什么这在迹-分歧模型中不重要）是，对于失败，拒绝与迹相关联，而对于分歧，我们只需要包含它们。封锁模式。然而，当考虑在一个阻塞的总和，A和C是不失败的分歧等价。事实上，在阻塞场景中，这些是单例故障等价，因此是阻塞数据细化。要看到这一点，在阻塞模型中没有分歧，迹线是每个都一样。 现在，虽然A有失败（失败的书，{TVF，ESF}），这不是存在于C中，在A中的单例故障模型下，我们仅获得单例故障（TVF，{TVF}），（TVF，{ESF}），.因此，差异是不可观察的。要恢复阻塞模型中的故障-发散细化，需要添加加强适用性条件。 也就是说，这正是CState·4将内部事件添加到阻塞模型在本节中，我们考虑细化，并推导出模拟规则，在阻塞模型中，分歧可能源于内部或非线性的存在。简单ESF书TVF没有一没有一TVT书ESTJ. Derrick，E.Boiten/Electronic Notes in Theoretical Computer Science 187（2007）354799able，操作τ。如在上述设置中，可观察操作以及τ将被描述为部分关系。因此，我们调整了上述总体，我们可以使用数据细化的标准定义我们使用标准的关系框架，但现在包括一个内部操作τ作为ADT的附加组件。从一个（部分）抽象数据类型S==（State ，Init，{Opi}i∈I，τ，Fin ），其中FinalizationFin观察到了定义3.4中的拒绝，我们的总和是^d^d^dd^dS==（State，Init，{Opi}i∈I，Fin）定义如下。我们采用标准的块累加，并添加另一个状态，bad，以表示发散。^d状态==状态，d==状态{，d}其中，，d/∈State和d。 由于这些值最终将是可观察的，它们也将被包含在全局状态G中。为了定义累计运算等，我们将使用以下符号。状态↓表示稳定状态，即这些是不可能从内部进化的。也就是说，v<$State↓i<$v<$domτ。τ表示有限的内部演化。 它可以被定义为最小固定点，λR·idτoR.τ∗|==τ−D（domτ）ismaximalfiniteint ernalevolutionn，leadingtoa stablestate. τω表示无界内部演化，特别地，集合domτω由无界内部演化可以开始的所有状态（“发散状态”）组成这个集合被定义为λ S的最大不动点。dom（τ DS）. 我们还使用谓词State↑来表示状态是发散的，使用Init ↑来表示状态是发散的。这表明ADT具有发散的初始状态。τ^ωencodesunbonundedinasdivergencena sdinedi nasd i v e r g e n ce n edin asdin e dinτ^ω==domτ ω×State，对于适当的状态空间State。IE==ττ^ωencdesalinternalevolutin。在无约束约束的情况下，所有的进化都是不可能的，因此，在这样的状态下，子和的编码是所有的进化。divOp描述了Op的应用可能伴随着无限内部演化的所有状态，定义为：divOp == dom（Opoτω）D48J. Derrick，E.Boiten/Electronic Notes in Theoretical Computer Science 187（2007）359^9DP=={d}×State，d使用适当的状态空间State对发散发生后的保持进行编码。BP=={（，）}编码阻塞的保留初始化初始化的总和将对应于初始化，随后是由于τ引起的任何潜在内部演化，在无界处编码为包括BP和DP以确保初始化的完整性。I^nitd==初始化IEBP-DP运算部分关系Op的累加分两个阶段实现。^B首先，应用分块累加，产生运算Op^d国家一级总。第二，我们形成了Op：状态，dParticipState，d附加任何潜在的演变由于τ，编码为发散，其中它是无界的。^d^boOp==（Op9IE）因此，我们将τ的效应吸收到运算和初始化中，并将其行为表示为非决定性和发散性。最终确定我们假设部分ADT为了实现与稳定故障模型的对应，我们需要确保拒绝仅在稳定状态下被记录，即，人其中τ未启用。为此目的，我们预先考虑最大内部行为，到最后。如果观察到的状态已经发散，则这将被前一个操作考虑在内（或如果没有初始化）。否则，我们记录从当前状态通过内部演化4可达到的所有稳定状态中的所有拒绝。D翅片==（τ∗|oFin）BBP BDP数据细化数据细化通过累加来定义，即A ±数据CiA^d±dataC^d.4.1与失效-发散修正接下来我们需要定义抽象数据类型的失败-分歧语义，即它的稳定失败和分歧。这可以直接定义，或者经由相应的CSP工艺（例如，如[5，18]）。我们做前者。我们用[A]表示数据类型A的失败发散语义（α（A），F（A），Div（A））[4]请注意，这不是严格必要的，因为这些状态已经是对同一迹的语义的考虑的一部分;然而，使终结成为部分关系的替代方案，尽管最终可能无害，但将我们带到基础理论的约束之外[11]。5请注意，此语义模型中的跟踪可以从故障中导出。J. Derrick，E.Boiten/Electronic Notes in Theoretical Computer Science 187（2007）35499Op奥普奥普tauD dC b c dc b图二. 噢，噢，噢关于Op\DivOp字母表α（A）是运算指数I的集合。 每个迹都是一个索引序列。 一个（非发散的）跟踪表示一个计算（非空关系）由初始化组成，随后是相应的操作序列也就是说，是A i ∈ Nj=0. n状态j·状态0∈ ran（Initoτ）k：1.. n·（Statek−1，Statek）∈Op好的。 如果数据类型在上下文中是明确的，则我们使用以下内容标识跟踪：ik9例如，（g，StateJ）∈tr或StateJ∈rantr。分歧是迹线，从这些迹线可以得到内部操作的无限序列一条迹tr是发散的（记为tr↑），只要存在tr的一个前缀trJ和一个状态StateJ∈rantrJ使得StateJ∈State↑。稳定故障是对（tr，X），其中tr是迹，并且存在稳定状态StateJ∈rantr使得<$i∈X·StateJ<$domOpi。每一个非发散的迹线都导致至少一个这样的稳定状态。定理4.1在阻塞模型中，A ±数据Ci <$[[A]] ±fd[[C]]。证据 参见[13]。Q4.2模拟规则我们已经证明，在抽象数据类型的过程语义下，在我们包含内部事件及其潜在分歧的上下文中，关系细化对应于失败-分歧细化。现在剩下的是提取可以应用于模式演算的模拟规则，因为我们不希望处理当前嵌入在终结中的事件集，也不希望明确计算发散迹。我们使用标准方法来描述底层部分关系的模拟规则，以验证扩展finalization的数据细化。关键^d就是要看到^B它被构造成两个总和。 第一个，OP，第二个是标准的块累加，我们在其中添加了bad，实际上，^BOp\divOp上的标准非阻塞累加 参见图2。Optau50J. Derrick，E.Boiten/Electronic Notes in Theoretical Computer Science 187（2007）35˜o^^99^^^99^B让我们表示Op\divOpbyO^p.4.2.1向下模拟在基本状态空间之间的模拟R的定义的特定空间上，我们定义了如下的模拟关系RR==RBPDP也就是说，状态空间中的阻塞和发散之间的关系是显而易见的。我们首先展开向下模拟条件。目前，我们省略了初始化和每次操作之后的有限内部演化。^d^Op上的仿真规则是根据Op展开的。 具体而言，我们认为R从AState到CState的重新定位，使得R是一个新的镜像，即：^d^doCInitAInit9 RDR9 CF输入DARAFini：I·R9i i9标准的关系论证[11，pp.77-^ ^您的位置：C^初始化A^初始化或R^ ^您的位置：RoC^FinA^Fin^ ^您的位置：ran（domAFinDR）随机domCFin^ ^您的位置：i：I·ran（domAOpiDR）^i：I·（domAOpDR）oC^Op^AOpo（RBP）i 9 i9这些被展开以给出关于潜在的部分关系的等价条件集。具体而言，它们成为：CInit↑ AInit↑<$AInit↑CInitAInitoRRoCFinCFini：I·ran（<$divAOpiDR）i：I·ran（<$divAOpii：I·（<$divAOpDR）oCOpi 9 i9我们现在将这些关系条件转换为抽象数据类型的Z表示的条件。初始化和操作后的有限内部演化仍然被省略。J. Derrick，E.Boiten/Electronic Notes in Theoretical Computer Science 187（2007）35519TA^Init^˜o^99CInit↑ AInit↑<$AInit↑初始化CStateJ·CInit初始化AStateJ·AInit初始化RJi：I·i：I·i：I·<$divAOpi<$R<$COpi<$AStateJ·RJ<$AOpi因此，这些是Z模式演算向下模拟规则，用于不考虑输入/输出的阻塞语义。让有限的内部进化再次明确给出：CInit↑ AInit↑<$AInit↑CStateJ·CInitoτAStateJ·AInitoτRJ9C9Ai：I·i：I·i：I·<$divAOpiRCOpioτAStateJ·RJAOpioτ9C9 A(Note这是因为，前（Opoτ）是前Op，而类似地，对于div。4.2.2向上模拟我们现在对向上模拟规则执行类似的解卷。具体地，我们认为从CState到AState的T满足C^InitdddDCFinDAFT9AFinD di：I·C^OpoTi9 9i并暂时忽略了内部进化。标准的关系论证[11，pp. 79^ ^您的位置：C^InitoTA^Init^O^CFin CBT9 AFin ^ ^您的位置：2016 - 05- 25 01：01：02（|{c}|）dom AFin <$c ∈ dom CFin^−^i：I·domCOpi-哦i：I·dom（TDdomAOpi）DCOpi9T52J. Derrick，E.Boiten/Electronic Notes in Theoretical Computer Science 187（2007）35同时考虑到有限的内部进化，我们将这些转化为：CInit↑ AInit↑<$AInit↑AStateJ;CStateJ·CInitoτTjAInitoτ9C9 ACSTATE·CSTATE·Ti：I·CState·i：I·（COpioτTJ）（AState·T（preAOpiAOpioτ））9C9 A5结论本文讨论了进程代数加细的关系观点在调查了该领域的现有结果之后，我们集中精力推导出失败-分歧细化和关系数据细化之间已经给出了所需的广义终结的精确特征，以及作为所使用的终结的结果的附加模拟条件的推导。通过考虑阻塞模型中内部事件的显式存在，这些结果扩展了[12]。在这方面的进一步工作包括将结果扩展到非阻塞模型，以及充分考虑输入和输