强制模拟：形式验证和自适应在Kripke结构上的应用

理论计算机科学电子笔记141（2005）171-197www.elsevier.com/locate/entcs使用强制模拟的Roopak Sinha1新西兰奥克兰大学帕塔河Roop2新西兰奥克兰大学Bakhadyr Khoussainov3新西兰奥克兰大学摘要Kripke结构上的模拟（前序）是一种众所周知的形式验证技术。模拟保证了抽象结构（属性或功能，F）的所有行为都包含在更大的结构（模型M）中。然而，由于存在设计错误，模型可能并不总是模拟属性。 在这种情况下，模型是手动调试的。 在本文中，我们提出了一个较弱的模拟结构称为强制模拟自动调试。当正常模拟失败时，应用强制模拟。 模型（M）和函数（F）之间的强制模拟保证了一个修改器D的存在，以适应M，使得M和D的组合在观测上等价于F。上的观测本文提出了一种称为弱互模拟的结构。 它还建立了，当两个结构是弱双相似的所有CTL双属性持有的一个也持有的其他结构。基于强制模拟的算法已被用于适应许多设计，这些设计在常规验证过程中未能达到某些性能。保留字： 形式验证，自适应，互模拟。1电子邮件：rsin077@ec.auckland.ac.nz2电子邮件：p. auckland.ac.nz3电子邮件：b. auckland.ac.nz1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.02.047172R. Sinha等人理论计算机科学电子笔记141（2005）1711介绍形式验证技术广泛应用于反应式系统的设计、定义和验证，如数字硬件和软硬件嵌入式系统[18，11]，[4，14，17]。形式化方法使用精确的语法和语义来定义系统的规范和模型，模型检查[4]是一种自动形式验证技术，用于使用M的状态空间上的可达性分析来检查设计（M）的模型是否满足给定属性（函数F）。由于初始状态空间缩减技术（如符号模型检查[2]）和最近使用SAT求解器进行有界模型检查的方法[1]，模型检查对于自动验证变得非常有吸引力。检测到模型上的属性故障是一个值得关注的问题，因为模型检查器通常只生成一些反例，设计人员必须在尝试另一个模型检查周期之前手动调试模型。因此，自动化调试的方法对社区有相当大的兴趣[6，7]。导致设计调试的模型检查失败可能是由于以下几个原因：(i) 规格或属性不一致：系统设计可能会因印刷错误而引入错误（例如将if（p≥0）写成if（p≤0）），这些错误很难使用自动化技术检测到。(ii) 建模不一致：系统可能被不一致地建模，导致模型检查失败。从给定系统中提取的形式模型可能无法准确地指示给定系统的所有行为，从而导致这种不一致。(iii) 一致但有缺陷的模型：由于设计者对需求的不正确解释，可能会出现错误。此类错误可能导致设计与规范完全不一致，或者可能引入冗余路径或状态，从而推广更精确的规范。第一类错误的自动调试是极其困难的，如果不是不可能的话。最近已经开发了用于调试第二类错误的方法自适应模型检查[6]解决了模型检查器由于建模不一致而提供假阴性的问题。另一种方法使用时序逻辑公式来控制系统状态之间的步进，从而调试并发系统的设计[7]。在本文中，我们主要关注的是第三类错误，R. Sinha等人理论计算机科学电子笔记141（2005）171173这是由于模型中存在冗余路径和状态。我们用下面的例子来说明这个问题。1.1激励实例及相关工作考虑使用信号量的两个进程互斥解决方案（图1[3] 表示为Kripke结构[5]。Kripke结构是模型检查中使用的标准模型，定义如下：定义1.1：Kripke结构[9]是一个状态机，表示为形式为M AP，S，s0，λ，δ，λ >的元组，其中：• AP是一组原子命题。• S是状态的有限集合。• s0是唯一的起始状态。• 事件是在系统环境中发生的一组有限的事件或信号。• δS××S是跃迁关系。• λ：S→2AP是状态标记函数，它用它满足的原子命题（在AP中）标记每个状态。对于互斥示例，AP ={信号量val = 0（可用），信号量val = 1（占用），p1状态= i（空闲），p1状态= c（关键），p1状态= e（进入），p1状态= x（退出），p2状态= i（空闲），p2状态= c（关键），p2状态= c（关键），p2状态= e（进入），p1状态= x（退出），p2状态= i（空闲），p2状态= c（关键），p2状态= c（关键），p2状态= c（关键），p1状态= e（进入），p1状态= x（退出），p2状态= e（进入），p2状态= x（退出），p2状态= i（空闲），p2状态= c（关键），p2状态= c（关键），p2状态= e（进入），p1状态= x（退出），p2状态= e（进入），p2状态= x（退出），p2状态= i（空闲），e（进入），p2状态 =x（退出）}。此外，S={s0，s1，s2，s3，s4，s5，s6，s7，s8，s9，s10，s11}，并且S ={p1，p2}。δ是转移关系，它包含系统的所有可能的转移，形式为（s0，p1，s1）的元组。λ是一个标签函数，它为各个状态提供特定的标签。 例如，λ（s4）={信号量val=0，p1 state= e，p2 state= e}（简称{0，e，e}）.图 1 中 的 信 号 量 示 例 包 含 12 个 状 态 ， 每 个 状 态 由 三 个 变 量semaphoreval、p1state、p2state标记。变量semaphoreval表示信号量是可用的（0）还是被占用的（1）。其他两个变量显示两个进程的状态，可以是i（空闲）、e（进入）、c（关键）或x（退出）。当一个进程不需要进入它的临界区时，它是空闲的;当它需要信号量时，它是进入的;当它进入它的临界区时，它是临界的;当它离开它的临界区时，它是退出的当触发转换的输入由系统的操作环境提供时，进行从当前174R. Sinha等人理论计算机科学电子笔记141（2005）171状态到后继状态的转换。操作环境可以被看作是一个进程选择器，它在每一个实例中决定允许哪个进程（进程1或进程2）进化。例如，在初始状态s0，信号量val= 0，P1状态 =空闲，P2状态 =空闲。 从状态s0到s1的转换被触发R. Sinha等人理论计算机科学电子笔记141（2005）1711750P1P10，i，iP2P212P10，e，iP2 4P2P10，即，e30，e，e51，c，i 1，i，cp1和p2P2P167p2 89P11，x，i1、c、e1、e、c1，i，xP2P1P210P1P211P11，x，e 1，e，x当进程选择器选择进程P1进行演进时。因此，变量p1的状态从i（空闲）变为e（进入）。其他变量保留其以前的值。如果在当前实例中没有选择任何进程处于活动状态，则系统将保持其当前状态。 为了保持系统的简洁描述，没有在每个状态上显示自循环。Fig. 1. 基于信号量的两进程系统图2中显示了一个Kripke结构F，它表示信号量系统的期望规格。在这个规范中，要求第一个请求信号量的进程（将其状态更改为-ing）是第一个完成执行其临界区的进程。在该规范中，如果进程1从其初始空闲状态（在s0中）演变为进入(ins1），则预计进程1被允许进入其临界州（第3条）。在此之后，两个进程都被允许进化，直到其中一个进程再次将其状态更改为进入。这可以被视为确保防止饥饿图1中的给定系统M并不满足这一要求。例如，从初始状态s0到达状态s1，进程1已经通过将其状态更改为entering请求了信号量。然而，当进程选择器选择进程2时，s1可以到达状态s4，进程2又通过将其状态更改为entering来请求信号量。然后，如果进程选择器选择进程2进行下一步演进，则状态s4可以转换到状态s8在这种情况下，过程2在进程1之前执行它的关键部分，即使进程1已经176R. Sinha等人理论计算机科学电子笔记141（2005）171s00，i，is1s20，e，i 0，i，eS3S41、c、i1、i、cS5S61，c，e 1，e，c首先请求信号灯。这个序列表示违反了所需的属性，因为首先将其状态更改为进入的进程没有进入并因此首先退出其临界区。图二. 所需的信号量系统行为给定如上所述的M和F，我们不能使用现有的自适应技术[6，7]来自动调试这个模型（因为模型中存在规范中不期望的错误路径和状态）。此外，像模型检查这样的技术将找到反例，模型的调试将不得不手动完成。所提出的方法尝试使用一种形式的动态模型检验其主要思想是构建一个修改器过程（另一种Kripke结构），动态地调整模型以删除错误的路径和状态。给定任意模型和规格（M-F）对，任何自适应技术都必须解决以下基本问题：(i) 在什么条件下，模型可以自动适应，以满足一个特定的？(ii) 如何确定一个给定的适应是正确的，也就是说，适应后的模型将满足给定的规范？(iii) 如何确定调整后的模型确实与其规范一致？在随后的章节中，我们将提出一个正式的框架，R. Sinha等人理论计算机科学电子笔记141（2005）171177这些问题。我们还使用称为ADVERT（反应系统的自适应验证）的自适应验证工具提供了实验结果。该文件的主要贡献是：(i) 开发了一个自动化算法框架，用于调试由于错误状态和路径而导致的验证失败。所提出的算法基于使用动态改变模型的修改器来适应有缺陷的模型的概念。(ii) 调试算法基于一种新的Kripke结构上的模拟关系，称为强制模拟，其比常规模拟弱。规范和模型的Kripke模型之间的强制模拟保证了修改器（另一种Kripke结构）的存在，以动态地适应模型，从而可以消除规范的不一致性(iii) 为了验证所提出的方法产生准确的修改器，结构之间的较弱等效（观测等效）的概念这导致了Kripke结构上的弱双模拟的发展，也是我们发展的。确定了修改器和模型的组成与所需规格弱双相似。它还进一步确定，当两个结构，图是弱双相似的，它们满足相同的CTL性质集(iv) 通过扩展NuSMV开发了一种称为ADVERT的自适应验证工具[3]。ADVERT已被用于调试许多标准的设计模型检查失败。标号迁移系统（LTS）[12]和Kripke结构[5]上的模拟和前序是众所周知的。虽然仿真和优化已用于状态空间缩减和实现验证，但它们并不直接适用于设计调试问题，因为所讨论的模型具有需要从模型中删除的错误路径和状态最近，在标记转换系统[16]上的强制模拟已经被用于动态地改变自动重用设计的LTS描述本文从根本上改变了LTS上的强制模拟思想，发展了Kripke模型上的强制模拟使用强制模拟的自动组件重用[16]提出了一种算法，该算法使用触发其转换的环境输入来匹配两个给定LTS的状态。然而，在所提出的方法中，两个给定的Kripke结构的状态匹配使用它们的状态标签。使用强制仿真的组件重用技术的目的[12][13][14][15][16][17][18][19而反观提出的方法在验证框架中工作，并基于适应，178R. Sinha等人理论计算机科学电子笔记141（2005）171使模型满足给定的时间规范。Kripke模型上的强制模拟需要比Kripke模型上的强互模拟更弱的等价性[13]，因为在调试模型中引入了τ本文发展了Kripke结构上的弱互模拟证明了该等价性保持了CTL的等价性。本文中解决的调试问题有点类似于控制系统中的可控性问题[15]，其中控制器被合成以使工厂表现为期望的规范（例如，控制器的作用是动态地适应工厂的行为任务控制器的功能是在特定点禁用工厂的某些操作。虽然这个问题已经在一般的非确定性设置中进行了研究，但它不适用于需要特定类型适应的反应式系统的调试任务。模块检查[10]是为反应系统的属性检查而开发的模型检查变量。与忽略环境的传统模型检查不同，模块检查考虑了反应式系统的异步环境。它将模型的状态视为环境状态（需要环境的状态）环境输入）或系统状态（不需要环境的内部状态输入），并在存在环境状态的情况下执行模型检查。在本文提出的自适应验证方法中，我们考虑了一种只有环境状态的设计抽象，并且由于我们提出的调试方法，一些系统状态也被引入到被调试的模型中。然而，与模块检查不同的是，所提出的方法不仅被动地考虑环境，而且还以修改器的形式引入了额外的环境，以强制某些环境事件进入模型或阻止环境中的某些事件到达模型（称为禁用）。本文的组织结构如下。第二节介绍了强制模拟关系，它已被证明是适应的必要和充分条件。自动生成的修改器如何适应给定模型的细节将在第3节中介绍。弱互模拟是一种等价关系，用于测试适应模型及其规范之间的等价性，在第4节中给出。第5节介绍了时间属性满足到弱满足的扩展，用于表明使用强制模拟适配的模型确实满足与给定规范相同的时间属性集。第七节介绍了设计调试的理论和实践结果，最后一节是结束语。R. Sinha等人理论计算机科学电子笔记141（2005）171179MMMMMMMM2强制模拟强制模拟是一种模拟关系，定义在两个Kripke结构上，一个模型（M）和一个规范（F），旨在为检查M是否适合满足F提供基础。它的定义如下（在这个定义中，函数（规范）的状态表示为sf，模型的状态表示为sm，（sf0，sm0）分别表示函数和模型的起始状态）：定义2.1：对于Kripke结构F和M，关系B=SF×SM×f-模拟关系被称为强制模拟关系（简称f-模拟关系）。假设下面的hold（sf Bσ sm用作（sf，sm，σ）∈B的简写其中σ的长度由|S M|（以M表示的州数））：(i) s f0B σ s m0，对某些σ∈ε ε.(ii) SFBa.σsm（：sm→JsfBσsJ ）对于任何σ∈εε。(iii) s B <$ s<$（λ（s）=（λ（s））（sJ，sJ ，σa.σ：s→sJ（s→afmsJ sJ Bσ sJFf））.mfmffmmfm第一个条件要求两个结构的起始态通过某个强制序列σ相关联。第二个条件要求，当任何两个状态（sf，sm）通过某个强迫序列a.σ相关时，则有必须是从sm到使用环境触发的某个状态sJ的转换输入JaJ，并且进一步地，sf，SJ 必须是相关。 这一规则是必要的，连续地减少强制序列，直到直接类似于SF找到了。当强迫序列为空或为零时，两个状态sfs，sm直接相关。在这种情况下，这些状态的状态标记必须匹配，并且sf中的每个跃迁必须与sm中的相应跃迁匹配，并且这些跃迁的结果状态必须通过某个序列σ相关。定义2.2：F±fsimM，条件是它们之间存在f−模拟关系。考虑图1和图2所示的过程M和F。F±fsimM，因为存在R ={（sf0，s m0），（s f1，s m1），（s f2，s m2），（s f3，s m3），（s f4，sm5），（s f0，s m6），，（s f5，s m7），（s f6，s m8），（s f0，sm9）}，这可以很容易地证明是f −模拟关系。3使用修改器的自动调试的方法是基于控制模型的转换，以确保满足规范。调整由自动生成的修改器过程执行，该过程执行ΣS一180R. Sinha等人理论计算机科学电子笔记141（2005）171基于状态的系统控制。修改器通过以下方式控制模型• 禁用操作：考虑M中的状态序列s0、s1、s4、s8、s11、s1（图1）。如前所述，该路径与图2中给定的规范F不一致，因为状态s1（其中进程1已经将其状态更改为进入）可以转换到状态s4（其中进程1已经将其状态更改为进入）。2也将其状态更改为进入如果国家s1被禁止转换到状态S4，可以消除故障路径。如果过程选择器信号p2在系统处于状态s1时对系统隐藏，则可以实现这一点。 这种基于状态的动作隐藏被称为禁用，当修改器吸收一个或多个环境输入并从而有效地禁止系统进行某些转换。• 强制动作：考虑M中的路径s0，s1，s3，s6，s0（图1）。这条路径也与规范不一致，因为存在状态s6（p1在其退出状态），它在F中没有对应的等价物。如果状态s3通过对进程选择器输入p1作出反应而发展到s6，并且然后如果s6不等待输入p1（其触发转换）而转换到其后继s0，则对于操作环境而言，似乎系统通过对单个环境输入p1作出反应而从s3转换到s0。因此，从s6到s0的转换成为内部转换，状态s6成为不可观察的或内部状态。这被称为强制，当修改器人为地制造环境输入以强制系统在不与环境交互的情况下进行特定转换时，可以实现强制观察路径s0，s1，s3，s6，s0的可观察部分s0，s1，s3，s 0，可以看出，它现在与F中的路径s0，s1，s3，s0一致（图2）。内部或不可观察的跃迁类似于CCSτ跃迁，仅源于内部或不可观察的状态。• 修改器可以允许M中的当前状态在没有任何禁用或强制的情况下演变。内部或不可观测的状态可以在强制期间由修改器引入适应系统。内部状态与可观察状态的不同之处在于，它对于操作环境是不可观察的，并且在不等待来自环境的任何输入的情况下进行内部τ转换到其后继状态。这种状态被称为命题intern，以表明它们是不可观察的。修改器需要严格控制模型中当前状态的所有转换，以便在需要时可以唯一地强制或禁用每个转换。因为触发转换的动作用于区分R. Sinha等人理论计算机科学电子笔记141（2005）171181S[p1]P1P2[第2页]SSP1P2SS[第2页][p1]P1P2P1P2S0、6、p1S0、9、p2P2SP12、10、p1S1、11、p2图3.第三章。信号量示例的格式良好的修饰符转换，没有状态可以有一个以上的转换由同一个动作触发。因此，只有确定性模型可以在拟议的框架下使用。定义3.1：Kripke结构A APA，SA，sa0，λA，δA，λA>被称为是确定的当且仅当对任意sa∈SA，如果（sa，a，SJ）和（sa，a，SJJ）∈δA对任意sa，SJ，SJJ∈SM且a∈M，则SJa a=sJJ.a a a a修改器必须格式良好，这意味着它不能允许任何如果修改器对其执行强制，则系统状态接受来自环境的输入。图3显示了图1中信号量示例的格式良好的修改器。修饰符本身不包含任何时间信息，它的所有状态都标记为命题True。3.1修改器和模型的组成修改器对给定系统的基于状态的控制使用新的//复合运算符定义如下。定义3.2：给定D APD，SD，sd0，λD，δD，λD>和M APM，SM，sm0，λM，δM，λM>，D//M被定义为由Kripke结构D//M AP （ D//M ），S（D//M），（sd0，sm0），λ（D//M），δ（D//M），λ（D//M）>描述的过程，其中：• AP（D//M）=APM{intern}（intern用于标记内部或不可观察状态）• S（D//M）SD×SM182R. Sinha等人理论计算机科学电子笔记141（2005）171DDDDD1• （sd0，sm0）是起始状态。• λ（D//M）（sd，sm）=λM（sm），对于所有sm∈SM和sd∈SD，如果Lab（sd）/={[a]}，否则λ（D//M）（sd，sm）={intern}.内部状态或通过强迫演化的状态被称为intern。• （D//M）=• δ（D//M）定义如下：(i) 强迫移动：D//M做出不可观察的τ移动，当D在M.s−[a→]s，sm−a→sm1（s，sm）−τ→（s，sm1）在这种情况下，状态（sd，sm）由于以下原因而成为不可观测状态：强迫。(ii) 外部移动：D//M用M和 M进行可观察的移动，D同时响应相同的环境输入。s−a→s，s−a→sm1（s，sm）−a→（s，sm1）在这种情况下，（sd，sm）是操作环境可观察到的状态。D//M的安装。开发//操作符的主要原因是允许修改器对模型的状态进行严格控制。由于这一要求，其他复合运算符，如CCS||操作员[12]可以不被使用。组合的结果是||运算符是一个模型，没有明显的控制M。在这种情况下，M或D的状态可以前进到它们各自的后继者，而不必与另一模型中的各自状态同步。另一方面，//操作符不允许任何一个模型中的任何状态在不与另一个模型中的相应状态同步的情况下前进，从而为修改器提供锁步控制。这类似于锁步过程同步[8]，但不同之处在于修改器执行强制的方式，这是不存在的在任何可用的合成操作符中。修改器不需要有关于系统处于哪个状态的显式信息。 当前状态可以通过跟踪系统到目前为止接收到对于信号量示例，给定图3中的修饰符D，如图4所示。注意，不允许状态s1和s2分别使用进程选择输入p2和p1进行转换这些禁用操作可确保不存在违规路径s1、s2、s4、s8或允许s1、s3、s4、s7如前所述，调制器在状态的基础上控制系统的相互作用，因此在状态s1和s2中被禁用的输入p2和p1在系统的所有其他状态中是允许的类似地，D//M中的状态s5、s8、s9和s10（或M中的s6、s9、s10和s11）是D1D1D1R. Sinha等人理论计算机科学电子笔记141（2005）171183s0P10，i，iS1P2S2P10，e，i0，即，eP2S3S41，c，i 1，i，cP2p1 p1 p2S5S6S7S8实习生1、c、e1、e、c实习生p1和p266实习生见图4。 D//M，图3中驱动信号量系统的被修改器强制分别转换到s0、s0、s2和s1。修改器人为地制造所需的动作（分别为p1、p2、p1和p2），使这些转换（τ转换）成为环境的内部转换我是说。因此，这些状态成为内在的，因而被贴上了“内在”命题的标签。4弱互模拟使用强制模拟调整模型后，需要确定其与给定规范等效。传统上，两个Kripke结构之间的等价性可以使用强互模拟来检查[13]。然而，如前所述，使用强制模拟的自适应可能使自适应模型中的一些状态不可观察。不可观测状态对于系统的操作环境是不可见的，并且在检查系统与规范的等效性换句话说，只需要提取系统的可观测部分，并使用这部分来检查等价性。为了验证可能包含不可观测状态或路径的两个Kripke结构之间的等价性，已经制定了一个结合LTS上的弱互模拟等价性和Kripke结构的强互模拟的较弱等价关系。两个Kripke结构被认为是弱双相似的，如果它们的可观察行为是强双相似的[13]。在介绍弱互模拟之前，定义184R. Sinha等人理论计算机科学电子笔记141（2005）171∧如下定义4.1：给定Kripke结构M AP，S，s0，λ，δ，λ >，s，SJ∈S，则：• 如果对某个作用a∈δ，（s，a，SJ）∈δ，则：· 如果λ（s）/=intern，则s→sj，其中E表示外部跃迁E从S到SJ。· 否则，如果λ（s）=intern，则s→sj，其中τ表示内部τ从S到S的• 考虑集合Trans={E，τ}。现在，如果α ∈ Transθ= A.B.C.D... Z是可能的跃迁序列，则s→SJ意味着s→s1→s2。s N−1→sJ。α A B Z这个定义用于将Kripke结构的跃迁重新标记为外部（E）或内部（τ）。例如，给定图4中的自适应模型D//M，考虑路径s0、s1、s3、s5、s0。已知的是s0→s1→s3→s6→s0。 将每个转换标识为外部或p1p 1p 1τ内部的，用E表示每个外部转换，转变为τ，我们得到s0→E s1→ES3→ES6→τ 重新标记的Kripke的s0结构我们也可以说，s0→s0，其中α=E.E.E.τ。α定义4.2：如果α∈Transnα∈{E}≠是通过以下方式获得的序列：∧从α中删除所有出现的τ。 如果在删除所有τ出现之后，α包含∧∧无元素，则α=π（τπ=π）。为了检查两个结构之间的等价性，只需要提取和比较它们的可观察路径。 这个定义描述了如何只提取一系列可观察和内部行为的可观察部分。给定适应模型D//M中的路径s0，s1，s3，s5，s0，在图4中，我们已经看到s0→s0，其中α=E.E.E.τ。提取α∧α的可观测部分，我们得到α=E.E.E。 考虑s6→s0的转变。 在τ这就导致α=τ，因此，根据定义，α=τ。图5显示了经过调整的D//M模型，其中转换被重新标记为E或τ。由环境输入触发的所有转换都标记为E，由修改器触发的所有内部转换都标记为τ（根据定义4.1）。定义4.3：Letα∈{E}。我的天α sJ当且仅当存在∧αJ∈Trans <$，使得s→sJ<$α=αJ。αJ考虑图5中自适应模型D//M的初始状态s0。R. Sinha等人理论计算机科学电子笔记141（2005）171185一则sb<$sb和B（sa，sb）B则sa≠a和B（sa，sb）s0E0，i，iES1S2EE0，e，i0，即，eS3S41，c，i 1，i，cEEEES5S6S7S8实习生1、c、e1、e、c实习生EE66实习生图五. 只有外部和内部过渡给定序列α=E.E.E，s0可以使用α到达状态s5，s6，s7和s8。然而，状态s5和s8是内部状态，因此会进行内部τ跃迁到它们的后继状态s0。因此，状态s0可以通过遵循es等式eαJ=E到达自身。E. E. τ。 从定义4。2，α_（IJ）=E. E. E=α。 从自适应模型的运行环境观察，如果提供序列α =E. E. E，则s0可以到达状态s6，s7和s0。τ跃迁在环境中不可见，因此未被考虑。定义4.4：给定两个Kripke结构A APA，SA，sa0，A，δA，λA>和B APB，SB，sb0，B，δB，λB>，在同一组原子命题APA=APB上，关系BSA×SB是弱互模拟，如果对任何sa∈SA和Sb∈SB，B（sa，sb）当且仅当：(i) （ λA （ sa ） =λB （ sb ） ） <$ （ λA （ sa ） =intern ） <$（ λB （ sb ）=intern）(ii) 如果对α∈Trans<$J Jj，sa → sjα∧α(iii) 如果对某个α∈Trans<$JJ J，s → s jαbβα图6显示了仅具有外部跃迁（标记为E）的规范F。 我们可以看到F中的s0和适应模型D//M中的s 0（图5）在弱互模拟关系上相关。 它们满足规则1，因为两者具有相同的状态标签（0，i，i）。它们也满足规则2和3。对于F中的s0可以使用任何序列α到达的每个状态sj，D//M中的s0可以明显地通过使用α-类，可以将s和s的值进行比较，结果是，S和s的值具有较强的相似性（并且，反之亦然）。186R. Sinha等人理论计算机科学电子笔记141（2005）171EE0E0，i，iE12E0，e，i0，即，e3EEE41、c、i1、i、cEE561、c、e1、e、c见图6。 规格F定义4.5：两个Kripke结构A< AP A，SA，s a0，λ A，δ A，λ A>和B< APB，SB，s b0，λ B，δ B，λ B>弱双相似当且仅当存在弱双相似规则WB满足WB（sa0，aB0）。两个结构被认为是弱双相似的，如果它们的初始状态是相关的弱互模拟关系。如上所述，F中的s0和D//M中的s0彼此弱双相似因此，根据上述定义，图4中的适应信号量模型D//M与图2中的给定规范F弱双相似。5弱满足使用强制模拟适配的系统可能包含不可观察的状态和路径。为了检查适应系统是否满足给定的时间属性，需要扩展属性满足以考虑给定系统中可能存在的不可观察行为这个问题可以解释如下。所有的时态逻辑公式，包括那些用CTL和它的子集（如LT L和CTL）表示的时态逻辑公式，都对状态及其直接后继者进行操作。然而，在适于使用强制模拟，一个国家的直接继承者可能是不可观察的。为了确保不考虑不可观察状态，需要使用以下方法来削弱属性满足：财产满足需要考察状态和路径。由于模型R. Sinha等人理论计算机科学电子笔记141（2005）171187调试引入了内部或不可观察的状态和路径，需要仅提取给定模型的可观察行为。这是使用操作符Nextob（）和Succ ob（s）来完成的，Next ob（）用于提取可观察的当前状态，Succob（s）返回当前状态的可观察后继者。Nextob和Succob函数的定义如下。定义5.1：函数Nextob：S→S其中S是重新标记的Kripke结构的状态集（定义4.1），使得：• 下一个ob（s）=s，如果s是可观察的。• Nextob （s） ={sJ|当n ≥ 1时，如果s是不可观测值，则s→sj≠bservale（SJ）。τn定义5.2：函数Succob：S→S其中S是重新标记的Kripke结构的状态集（定义4.1），使得：• Succob（s）={sJ|s→E.τn如果s是可观测的，则sJ≠observable（sJ），其中n≥ 0}。• Succob（s）={sJJ|（SJJ∈Succob（SJ），其中re（SJ∈Nexxtoob（sa））如果s是不可解的.给定图5中的适应模型D//M，考虑初始状态s0。这是一个可观察的状态。因此，下一个ob（s0）={s0}（定义5.1）， 下 一 个ob（s0）={s1，s2}。可以看出，对于可观察状态，Nextob返回原始状态，Succob返回可观察的后继状态。给定状态。 现在考虑修改后的模型D//M中的状态s5。 这是一个内部状态（标记为intern。因此，Nextob（s5）={s0}，Succob（s5）={s1，s2}。对于内部状态，Nextob返回其可观察的子状态（通过一系列一个或多个τ转换到达），Succob返回Nextob返回的状态的可观察后继者。上述定义表明，在检查属性满足时，内部状态被视为等同于其可观察后继状态。根据上述定义，可观察路径可定义如下：定义5.3：从状态s开始的无限可观测路径定义为π ob（s）= s0，s1，s2，.，s∞，其中s0∈Next ob（s），状态s1到s∞递归定义为si= sJ|sJ∈ Succob（s i−1）.定义5.4：对于从状态s开始的任何路径π（s），其对应的可观测路径πob（s）是通过从其中移除所有不可观测状态而获得的。符号|= W用于表示弱满意度。状态、路径和模型的弱满足定义如下。定义5.5：对于任何CTL状态-公式和任何状态s，s| = W当且仅当存在状态sJ使得sJ∈Next ob（sJ）且sJ|= 0。定义5.6：对于一个CTL路径公式π和任何路径π，188R. Sinha等人理论计算机科学电子笔记141（2005）171状态为s，π| = W<$当且仅当可观测路径π ob（s）|= 0。定义5.7：对于CTL公式λ和Kripke结构M< AP，S，s0，λ，δ，λ >，M|当且仅当：• 如果k是一个状态公式，则s|= W。• 如果π是一个路径公式，那么对于所有可能的路径π（s0），其起始状态为s0，π（s0）|= W。对于Kripke结构M和CTL_n公式M，如果M| = 0，则M| = W。这一论断表明，弱满足扩展了财产权的概念，该方法可以使结构与内部结构分离，同时在没有不可观察状态的结构中保持属性满足。弱满意度使得复合过程中模型内部的强制转换。在当前的自适应算法中，修改器可能会强制规范中不存在的状态，以便使模型满足所需的规范。显然，如果我们将这种自适应技术扩展到模型检查，那么强制需要受到限制，以便不应该强制坏状态（可能导致属性严重故障的状态）。因此，强制模拟需要修改，以包括处理某些不可强制的状态。6自适应验证算法给出了一种计算给定M和F的强迫模拟关系的算法。如果成功，算法生成修改器D。所提出的算法是基于强制模拟的组件匹配算法的改编[16]。该算法包括一个预计算步骤，该步骤计算M中每个状态的所有可达状态以及到这些状态的最短路径。组件匹配算法[16]计算从源状态到目的状态的路径，作为从源状态到达目的状态所需的环境信号然而，所提出的算法还计算两个状态之间的另一条路径，作为一个状态标签序列，从源状态的状态标签开始，然后是所有中间状态的状态标签，最后是目标状态的标签这些额外的信息用于根据标签匹配状态所有计算的状态和路径都存储在一个称为RS（M）的集合通过将F中的每个sf与RS（M）的所有成员配对来创建初始块集其中一个块被选为细化块，所有其他块都基于此进行细化。当达到固定点时，细化然后，按照与接口生成类似的方法，从细化的块集合生成修改器DR. Sinha等人理论计算机科学电子笔记141（2005）171189算法中的组件匹配算法[16]。 总的复杂性所提出的算法是O（NS2×NS2×m），其中NSF和NSM是F M分别在F和M中的状态数，并且m = ||CIMM||.7结果下面的定理证明了强制模拟是前面章节中描述的自动调试的充分（定理1）和必要（定理2）条件。定理3建立了如果两个Kripke结构是双相似的，则它们弱满足相同的性质集。由于自动自适应保证了D//M与F双相似，定理3保证了D//M弱满足F所满足的同一组性质（因此等价于F）。定理1：给定F±fsimM，存在D使得F<$D//M，其中Kripke结构上的弱互模拟等价。定理2：若存在一个良构的确定性界面D，使得F<$D//M，则F±fsimM.定理3：给定两个Kripke 结构A APA，SA， Sa0，λA，δA，λA>和BAPB，SB，Sb0，λB，δB，λB>，使得A<$B，则对于任何CTL<$公式<$：（A）|= W）优惠（B| = W）哪里|= W代表弱满意度。这些定理的证明在附录A中提供7.1实施结果一个名为ADVERT的自适应验证工具已经使用Java编程语言和NuSMV模型检查器实现[3]。自动调试的步骤如下：(i) 从SMV（符号模型检查器）语言文件中提取模型M和规范F。提取算法被纳入流行的NuSMV模型检查器[3]，用C编程语言编写。提取算法从SMV文件的根（或初始）节点开始执行广度优先搜索。遍历的每个状态的显式细节（标签，转换等）被写入输出文本文件。这些输出文件然后用作强制模拟算法的输入。(ii) 在如上所述读取M和F之后，强制模拟算法尝试在两个结构之间建立强制模拟，并且如果成功，则生成可以调整M以满足F的修改器。的190R. Sinha等人理论计算机科学电子笔记141（2005）171modifier以文本文件的形式存储。如果M和F之间不存在强制模拟关系，则算法退出，并显示一个适当的错误消息，表明M是不可适应的。上述过程已应用于调试几个SMV模型，主要来自NuSMV网站上的示例集合[3]。调试结果如表1所示。第一列包含被调试模型M的名称和大小（状态数）。下一列表示规格F的大小。 最后一列指示类型执行的调试（强制、禁用或两者）。在某些情况下，例如交替位协议和批处理反应器系统，给定模型的原始NuSMV描述中的实际状态数的子集用于调试。在许多情况下，例如互斥和管道示例，调试模型以满足给定的公平性约束。在其他情况下，例如生产者-消费者和优先级队列示例，基于优先级的规范用于调试模型，以优先考虑特定的子流程。大多数调试都展示了如何调试一般模型以满足更具体的规范。8结论现有的形式化方法可以全面地检测给定模型和规范之间的不一致。然而，在检测到这种不一致之后，需要对模型进行手动调试，以满足给定的规范。这种手动调试可能是耗时的，并且验证和调试的过程因此，在未能满足关键规范的情况下进行自动设计调试是非常有意义的。本文提出了一种自动化模型调试的形式化技术。给定一个模型M和一个失败的规范F，所提出的技术可以确定M是否可以自动适应以满足F。如果模型与本文提出的称为强制模拟的较弱模拟关系上的规范相关，则可以自动调试模型强制模拟的存在被证明是所提出的调试的必要和充分条件。如果M被强制类似于F，调试算法自动生成一个修改器D，它保证修改M（以D//M的形式）以满足F。调试算法已经在Java编程语言中实现，并且已经调试了NuSMV示例集合[3]中的几个模型当前的实现仅限于中等大小的模型，因为它使用模型和规范的显式表示，并在效率较低的Java平台上执行。目前正在开展工作，