模块与外部接口的完整性规范性确保方法

理论计算机科学电子笔记144（2006）73-89www.elsevier.com/locate/entcs故障监测接口Amir Pnueli1，2Aleksandr Zaks1，2纽约大学Lenore Zuck丽诺尔·扎克1，3伊利诺伊大学芝加哥摘要我们考虑模块与外部接口（环境）交互的问题，其中交互预期满足某些系统规范Φ。虽然我们有模块的完整实现细节，但我们只给出了接口的部分外部规范接口规范是部分的（不完整的）意味着接口只显示接口规范所允许的行为的严格子集。基于接口规范通常是不完整的假设，我们解决了这样一个问题：我们是否可以将接口规范收紧到一个与给定的部分规范一致的策略中，该策略将保证由模块的可能行为产生的所有可能的相互作用都将满足系统规范Φ。 我们将这种更严格的规范称为Φ-保证规范。 而不是验证接口，这往往是一个现成的组件，满足更严格的规格，本文提出了一个运行时监视器的结构，不断检查存在的Φ保证接口。我们将模块和外部接口视为2人游戏中的玩家。如果接口能够保证无论模块做什么，Φ满足。不完整规范的问题通过允许接口遵循与接口规范一致的任何策略来解决我们的方法基本上结合了传统的运行时监控和静态分析。这允许超越传统的运行时监控工具的重点关键词：运行时监控，无限游戏，通用活性，测试，基于组件的设计，接口，时序逻辑，模型检测，欧米茄规则游戏，形式化方法1本研究部分由NSF资助CCR-0205571和ONR资助N 00014 - 99-1-0131支持2电子邮件：{amir，zaks}@ cs.nyu.edu3 电子邮件：{lenore@cs.uic.edu1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.02.00574A. Pnueli等人理论计算机科学电子笔记144（2006）731介绍构建软件的过程正在经历快速的变化。代替组织内的单片软件开发，越来越多地，软件使用第三方组件（例如，JavaBean，.NET等）。开发人员对组成整个系统的组件的内部结构组成代理的一个障碍是，目前的形式化方法主要关注的是“封闭”的系统，是从地上爬起来。这些系统完全由用户控制。因此，可以通过对系统进行仔细检查来解决由不规范组件引起的问题。当使用“现成”代理组成代理时，情况往往不再如此。出于对专有信息的考虑，或为了简化表述，公司可能提供不完整的说明。尽管不规范，“现成的”组件可能仍然具有足够的吸引力，因此新服务的设计者可能希望使用它们。为了安全地做到这一点，设计人员必须能够处理这些组件可能会出现不期望或意外行为的可能性，这可能会危及新系统的正确性和安全性本文讨论的主要问题是规格不足。作为这种现象的一个简单例子，考虑一个接口规范，它保证接口的设计者可能意味着一个更强的规范，假设较新版本是足够的，并且是确保由模块和接口组成的整个系统的正确性所必需的。应用形式化的方法，如模型检查，很可能会失败，因为没有算法方法为模型检查器提供适当的接口规范加强。然而，在接口规范可能是部分的假设下，可能存在一个保证正确性的允许行为的子集，并且仍然可以使用该组件，只要可以检测到接口与这个“良好”行为集的假设我们得到：• 一个有限状态模块M，由我们的设计者设计，并附有其实现的全部细节;• 与模块M相互作用的外部组件的接口规格ΦI;以及• 整个系统的目标规范Φ，必须通过模块和接口之间的交互来满足A. Pnueli等人理论计算机科学电子笔记144（2006）7375我们将模块和界面视为2人游戏中的玩家。在计算的任何阶段，我们都要问接口是否有一个与其规范ΦI一致的策略，使得对于模块M的任何可能行为，由模块和接口的相互作用产生的系统行为都保证满足目标Φ。我们使用这种连续的游戏求解作为系统运行时监控的基础，一旦系统达到接口不再能保证系统正确运行的状态，我们就发出警报（即，满足Φ）。对上述描述的一种天真的解释似乎暗示着我们在任何一个参与者的每一步棋之后都解决了一个完整的博弈。这样的实施方式将使该过程昂贵得令人望而却步。相反，我们将注意力限制在获胜条件是普遍活性- 也就是说，在插入和删除任意有限前缀的情况下关闭。对于这样的游戏，只解一次游戏就足够了，然后只监视游戏结构内的计算进度。单个游戏求解过程可以在编译时执行，因此在监控阶段几乎没有什么要做的。在第3节中，我们证明了每个博弈都可以转化为具有普适生存获胜条件的博弈有趣的是，将我们的方法与[2，7]中描述的传统运行时监控方法进行比较。据我们所知，所有传统的运行时监控系统在很大程度上忽略了所考虑的程序的实现细节，而专注于分析特定的行为。如果一个人最感兴趣的是证明所观察到的执行跟踪是无错误的，并且可能收集一些统计信息，那么这样的监视系统工作得特别好。然而，如果主要目标是在设计本身中找到错误，而不仅仅是在特定的计算中，那么传统的方法通常是不可接受的。 相比之下，在我们的框架中，除了运行时信息之外，我们还试图使用所有可用的实现细节。这最终导致更高的精度，因为我们不仅监控电流轨迹，而且监控更多。这个想法类似于目标放大[15]，在调试多线程应用程序时特别有用本文的结构如下。在第2节中，我们描述了系统和游戏的形式化模型，并展示了系统如何与游戏相关联在第3节中，我们展示了如何解决这样的游戏，第4节描述了监视器的构造。在第5节中，我们讨论了我们的方法的各个方面。最后，在第6节中，我们提出了我们的结论和一些可能的未来研究方向。76A. Pnueli等人理论计算机科学电子笔记144（2006）732模型2.1公平离散系统我们采用公平离散系统（FDS）作为我们的计算模型，它是公平转移系统的一个变体[12在这个模型下，一个系统M：V，W，Θ，ρ，J由以下组件组成（为了简单起见，我们省略了同情）：• V：一组有限的系统变量。系统S的状态提供了系统变量V的类型一致的解释。 对于状态s和变量v∈V，我们用s[v]表示状态s赋予v的值。设V表示V上所有状态的集合。我们假设，它是有限的。• W*V：只有系统本身可以修改的拥有变量的子集。所有其他变量也可以由环境修改• Θ：初始条件。一个状态被定义为初始状态，如果它满足断言（状态公式）Θ。• ρ（V，VJ）：跃迁关系。• J：一组正义（弱公平）要求（断言）。F或变量的子集U<$V，我们引入缩写pres（U）=u∈U（uJ=u），指定U中所有变量保持其值的转换。 在不失一般性的情况下，我们假设如果sJ是s的ρ-后继，则至少有一个所拥有的变量在s和sJ之间改变其值，即，SJ[W]/=s[W]。我们定义了一个扩展的转移关系：ρ=ρpres（W）这个扩展的关系除了允许ρ步之外，还允许环境步。允许这些步骤任意更改所有变量，只要它们保留所有拥有的变量的值。FDSS的开放计算是状态σ的无限序列：s0，s1，s2，...， 满足以下要求：• 初始化：s0是初始的。• 结论：对于每个l= 0，1，. ，则状态sl+1是状态sl的ρε-后继。也就是说，sl，sl+1<$|其中，对于每个v∈V，我们将v解释为sl[v]，并且将dvJ解释为sl+1[v]。• 正义：对于每个J∈J，σ包含无限多个J-态的出现。此外，我们要求存在无限多个j，使得sj和sj +1在所拥有变量的值上这保证了环境有无限多的机会迈出一步。从现在开始，我们将开放计算简称为“计算”。给定两个FDS如果系统兼容，它们的异步-A. Pnueli等人理论计算机科学电子笔记144（2006）7377−−平行组合，M1<$M2，是FDS，其变量、拥有变量和正义的集合是这两个系统的初始条件是初始条件的合取，而过渡关系是两个过渡关系的析取。因此，执行组合系统的步骤是系统M1的步骤或系统M2的步骤。我们所有的具体例子都是在SPL（简单编程语言）中给出的。语言），其用于表示并发程序（例如，[12，3]）。每个SPL程序都可以直接编译成FDS。特别地，SPL程序中的每个语句都对转换关系贡献一个析取。例如，赋值语句“l 0：x：= y + 1 ; l 1：“对描述程序的FDS中的转换关系有贡献，在− l 0 at j l 1 x j = y +1 pres（V \ { x，π }）处的析取。谓词at-l0和atJl1分别代表断言π= 0和πJ= 1，其中π是控制变量，表示过程中的当前位置，该语句所属的（程序计数器）。2.2游戏结构根据[5]，我们定义一个（两人）博弈G=（S，A，Γ1， Γ2，δ）由以下组成：• 状态的集合S;• A.行为的有限集合;• 动作分配函数Γ1， Γ2：S→2A\n，其为每个状态定义分别可用于参与者1和参与者2的非空动作集合• 一个转移函数δ：S×A×A→S将每个状态s和每对动作（a1，a2）∈Γ1（s）×Γ2（s）映射到一个后继状态δ（s，a1，a2）;在每个状态下，玩家同时选择他们的行动。这两个动作定义了系统的下一个状态假设我们有一个如上所述的博弈G 对于i ∈ {1，2}，参与者i策略是函数i：S+→A，则任何一个序列都不满足S<$∈S+，且与Γ一致（即， 对于每个s<$∈S<$i和s∈S，<$i（s<$;s）∈Γi（s））。用于计划的一组策略表示为dbb b bi。给定一个博弈结构G，G的游程r是一个非空的，可能无限的序列s0（a1，a2）s1（a1，a2）s2. 交替的状态和动作对，0 0 1 1对任意j≥0和i∈ {1， 2}，ai∈Γi（sj）和sj+1=δ（sj，a1，a2）.j j j对于运行r：s0（a1，a2）s1（a1，a2）s2.. . ，我们参考状态序列σ（r）：0 0 1 1s0，s1，s2，. 作为R. 给定一对策略<$1∈<$1且R_2∈R_2，且状态s∈S，则由R_m~1，R_2（s）构成的策略的集合是从s开始的一个游程，其动作与策略一致.78A. Pnueli等人理论计算机科学电子笔记144（2006）73一个人，S1c，c阿瓜a，cS4c，cs0S3刚果（金）c，bS2c，c孟加拉国b、cS5c，c设h：s0，s1，. s，k = s是有限历史，k是S上的线性时态逻辑公式。历史h被认为是参与人-i，i∈{1，2}，关于G中的目标博弈，如果参与人-i有一个策略<$i∈ <$i，使得对于所有s策略<$3−i∈<$3−i，h·σ（R<$1，<$2（s））|=0。 一个合适的策略是从G中的h开始的参与人i获胜策略。在获胜历史h由单个状态s组成的情况下，我们将s称为参与者-i获胜状态。例1设S={s0，s1，s2，s3，s4，s5}且A={a，b，c}。设Γ1、 Γ2和δ定义如下：Γ1（s0）={c};Γ2（s0）= {a，b};δ（s0，c，a）=s1;δ（s0，c，b）=s2;Γ1（s3）= {a，b};Γ2（s3）={c};δ（s3，a，c）=s4;δ（s3，b，c）= s5.对于状态s∈ {s1，s2，s4，s5}，有Γ1（s）= Γ2（s）=c.对于j∈ {1， 2}，δ（sj，c，c）=s3;对于j∈ {4， 5}，δ（sj，c，c）=sj.相应的游戏结构如图所示。1.一、请注意，参与人2完全控制s0的过渡。也就是说，当博弈处于s0时，参与人2可以决定下一个状态是s1还是s2。以类似的方式，参与人1控制s3的出口。Fig. 1. 示例1的游戏结构。游戏的目标被定义为：=（（s1→s3这个目标要求，对s1的任何访问都应该紧接着对s3的随后访问，而s3又应该紧接着对s4的访问，同样地，s2应该紧接着对s3的访问，然后对s5的访问。在这个游戏中，状态{s3，s4，s5}对于两个玩家来说都是赢的。这是因为从这些状态中的任何一个都没有路径通向s1或s2。其他状态--s注意，从s0开始的获胜策略取决于到达s3时通向s3的路径，也就是说，取决于前一个状态是s1还是s2。赢得非单例历史是h：s0，s1，s3和hJ：s0，s2，s3，它们是参与者1的获胜。2.3将博弈与FDS给定一个对应于某个SPL模的FDSM=（VM，W，Θ，ρ，J），一个系统规范Φ和一个接口规范ΦI，我们定义一个博弈A. Pnueli等人理论计算机科学电子笔记144（2006）7379G=（S，A，Γ1， Γ2，δ）在模M和界面之间如下。设V=VM增广了一个不在VM中的变圈∈ {1， 2}.设S是所有V-态的集合. G的动作的集合A在游戏G中，玩家1（模块）可以采取M允许的任何步骤，非确定性地设置回合，从而决定它是否希望采取另一步骤。参与人2（接口）可以设置任何不属于M的变量，但它必须让参与人1进行下一步。形式上：• Γ 1（s）={sJ|斯，斯杰|= ρ}• Γ 2（s）={sJ|斯，斯杰|=.转J= 1转v∈VMΣ\Wpres（V\ {v，turn}）}• δ（s，a1，a2）=as[转]。也就是说，δ选择1作为当前状态s中的下一状态i_turn= 1。游戏的目标是由以下定义的：<$=（Φ <$Φ I）<$ （turn= 1）<$J ∈J（<$J）。因此，要么同时满足Φ和ΦI，要么违反其中一个正义要求，要么阻止接口执行无限多的步骤，就可以赢得游戏。我们强制模块无限次放弃它的回合，以保持交织的语义。2.4拉宾链自动机假设FDSM=（V，W，Θ，ρ，J）。我们将V的解释称为计算状态。在一组计算状态S上的索引为k的确定性全拉宾链自动机是元组R=（Q，q0，Δ，c），其中：• Q是自动机状态的有限集合;• q0∈Q是初始状态;• Δ：Q×S→Q是一个跃迁函数;• c：Q→ {0，...，2 k− 1}是一个着色函数。R在无限计算σ上的运行：s0，s1，s2，. ，是无限序列q0，q1，q2，. 其中q0是初始自动机状态，对任意i≥0，Δ（qi，si）=qi+1. 我们说q0，q1，q2，. 是由计算σ引起的游程。运行q0，q1，. 如果在颜色序列c（q0），c（q1），.中出现无限次的最大颜色是可接受的。是偶数。如果由σ导出的游程是可接受的，则计算σ被自动机R接受. R的（ω-）语言，记为L（R），是R所接受的计算的集合。 我们说自动机R接受时态公式，如果L（R）恰好是满足时态公式的计算集。80A. Pnueli等人理论计算机科学电子笔记144（2006）73S1s0，s3，s4，s5年q1S3年q3S4q0qrS5年q4S3s2q2• 检查在游戏G中接口（玩家-2）的初始状态是否为获胜。如果不是，那就报警。• 在所有后续步骤中，设h为自计算开始以来观察到的历史如果h不是接口的获胜者，则发出警报。例2在图2中，我们给出了LTL公式<$=（（s1→ s3<$s4）<$（s2→s3<$s5））的拉宾链自动机。图二. 示例1中博弈的目标链的拉宾链自动机该自动机具有状态集合Q={q0，q1，q2，q3，q4，qr}。我们通过一条标记为s的边将自动机状态qi连接到qj，以表示转移函数项Δ（qi，s）=qj。为了简化表示，我们没有明确标记将状态连接到特殊拒绝状态qr的虚线边缘。按照惯例，虚线边缘被隐式地假设为由S状态标记，S状态不标记离开相同自动机状态的其他边缘最后，着色函数c由下式给出：c（q0）= c（q1）= c（q2）= c（q3）= c（q4）= 0，c（qr）= 1。3解决游戏我们的运行时监控方法是基于这样的观察：当接口没有获胜策略时，违反规范是无法预防的。因此，监控算法跟踪模块和接口之间的交互，并在第一次检测到接口不再具有获胜策略时发出警报。在图3中，我们给出了这个想法的一个简单实现。图三. 预防维护虽然图3中的算法完全捕获了我们的监测方法的精神，但它在计算上是不可接受的。这是因为它意味着我们每次都必须重新分析这个博弈，而这个分析是关于在计算过程中可能出现的一组无界的可能历史的请注意，如果我们可以将游戏的状态划分为好的和坏的，那么，不管游戏的历史如何A. Pnueli等人理论计算机科学电子笔记144（2006）7381当游戏处于良好状态时，接口可以赢得奖励，并且类似地，模块可以从不良状态赢得奖励。 形式上，我们定义一个状态s对于参与人-i的目标是好的，如果以下成立：每一个以s结尾的历史都是参与人i相对于n的胜利我们定义一个状态s对于参与人-i相对于目标函数是坏的，如果：状态s对于参与人-（3−i）相对于目标函数是好的。例如，图1的游戏的状态{s0，s1，s2，s3}对于玩家-1（w.r.t）是好的。 这是唯一的状态，这是好的任何球员在这个游戏中。例如，状态s4是否获胜的问题取决于我们到达s 4的路径。如果路径经过s1，那么s4获胜。如果路径经过s2，则s4不是获胜状态. 从这里开始，我们只对参与人2（接口）和目标对象使用好和坏的术语。 一个博弈G称为可分的，如果每个状态s是 无论好坏在游戏G是可划分的情况下，容易构造监视器。首先，我们通过找到所有好的状态来解决游戏G请注意，在可划分的游戏中，好状态和获胜状态的概念是一致的。因此，我们可以使用[5]中提出的算法来找到所有玩家2获胜的状态，解决一个游戏。在运行时，我们只需要确保游戏不幸的是，一个状态s并不总是可以被识别为好或坏。请注意，与FDS相关联的游戏可以很容易地表示为具有Borel获胜条件的回合制游戏，该条件已知是确定的[4]。确定性保证了对于每个特定的历史h，参与人-1可以赢得1/2或参与人-2可以赢得1/2，对于第2.2节中描述的并发博弈来说，一般不成立[6]。因此，我们不能总是划分状态的唯一原因是，对于某些状态，参与人2对历史h有获胜策略，但对某些状态没有其他历史HJ如上所示，状态s4就是这种情况。因此，每当游戏到达s4时，监视器不能立即决定是否应该发出警报。原则上，我们可以做出正确的决定，仔细观察游戏的历史，并使用计算获胜状态的算法的变体然而，这将要求在每次访问s4时进行新的游戏分析。显然，这将使监测过于昂贵。为了解决这个问题，我们的游戏，它是可能的分区状态分为好和坏的特点。如果以下成立，则LTL公式Ω表示普适活性对任意的σ1∈ ε ω和σ2∈ ε ω，σ1·σ2|= Ω i <$σ2|= Ω。82A. Pnueli等人理论计算机科学电子笔记144（2006）73我注意，绝对活性[1]只满足这个定义的一个方向（即，如果σ2|= Ω，则σ1·σ2|= Ω）。普遍活性的概念在[14]中以公平的名义被考虑。此外，应该强调的是，普遍活性不应该与无记忆策略的概念混淆（即策略的选择只取决于游戏历史的最后状态）。事实上，具有普遍活性获胜条件的游戏的获胜策略可能需要记忆，反之亦然。可以证明，如果博弈G的目标矩阵是一个泛活性性质，则G是一个可分博弈。直觉上，如果某个历史h有一个获胜策略，我们可以用任何其他历史hJ替换它，共享相同的最后一个状态。因此，不可能存在这样的状态，即参与人-2仅相对于某个历史h而不相对于共享相同的最后状态的某个其他历史hJ在本节的剩余部分中，我们将展示如何将任意博弈G转换为等价博弈GJ，其目标是表示普适活性性质的Gj。从本质上讲，我们分裂了未决定的状态，如图4中的s41，以便新的状态可以被识别为好或坏。3.1将游戏的目标转换为普遍活性给定一个博弈结构G =（S，A，Γ 1，Γ 2，δ）和一个目标函数σ，我们首先建立一个关于目标函数σ的Bu？例如，在一个实施例中，[8]）。利用[13]中的c ~（？）构造了S上的完全确定性Rabin链自动机R =（Q，q0，Δ，c），使得接受用Rabin链自动机合成对策结构GR是博弈G×R=（SJ，AJ，ΓJ， ΓJ，δJ），其中：1 2• SJ=S×Q;• AJ=A;• 对于i= 1， 2，ΓJ（（s，q））= Γi（s）• δJ（（s，q），a1，a2）=（δ（s，a1，a2），Δ（q，s））.对于博弈GJ=G×R，可以直接将R的接受条件转换为LTL目标J。我们可以将“”定义为：J=k−1。（c=2i）（c≤2i）i=0，其中c在状态（s，q）中被解释为c（q）。由于公式J由以下形式的公式的布尔组合组成p和p对于断言p，很容易证明，PJ表示一个普适的活性属性。如前所述，我们可以使用[5]中的算法求解GJ例3考虑图1中的博弈结构1.一、自动机的A. Pnueli等人理论计算机科学电子笔记144（2006）7383目标函数在图中给出2，和组成的游戏概述图。四、（c，c）（c，c）（c，c）（c，c）见图4。 组成的游戏组合博弈中唯一好的状态是（s4，q0）和（s5，q0）。其他国家都很糟糕。因此，如所期望的，具有通用活性目标的组合博弈是可划分的。3.2DetterministicBuéchiSpe ci ciations上面的建筑是相当昂贵的。结果博弈的规模是原始目标博弈长度的两倍指数。此外，新目标的大小与长度成指数关系。一个重要且经常出现的特殊情况是，当指定Φ Φ I可以表示为确定性的布希自动机时。 在这种情况下，我们可以跳过昂贵的确定步骤。我们提出了一种有效的算法，用于监测这种特殊情况。如第2.3节所定义，我们的博弈G的目标定义为：<$=（Φ <$Φ I）<$（turn= 1）<$J ∈J（<$J）。回想一下，为了解决一个游戏的运行时监控，我们需要使用一个可分区的游戏。在3.1节中，我们给出了一个将任意博弈转化为具有普适活性目标的博弈的一般方法。这里我们考虑（Φ <$Φ I）可以用一个确定的Buchi自动机表示的特殊情况. 我们提供了以下几点：• 建立了一个确定性的Buchi自动机B，它有一个cepts（ΦΦI）。设F代表接受的集合。• 如3.1节所示，将自动机B与博弈G组合，得到GJ=G×B。设所得博弈GJ的目标定义为：F<$（turn= 1）<$J ∈J（<$J）.• 考虑以下形式的LTL目标Φ：ni=1（一）R1），（a，c）s4，q0（c，a，s，q）（c、c、s、q）1133（b，c）s5，qrs0，q0（a，c）s4qrs2，q2中三、四问（c，b）（c，c）（b，c）s5，q0p84A. Pnueli等人理论计算机科学电子笔记144（2006）73GGGG其中p，r1，.，rn是断言。显然，GJ的目标具有这样的形式。让Win是Φ的参与人2获胜状态的集合。在[9]之后，我们可以计算Win如下：哪里.nWin= νZ.μY。i=1ΣV X. （p<$ Z）<$Y <$（ri<$ X），[[f]]e={s∈S|n∈Γ2（s）. εa∈Γ1（s）. δ（s，a，b）∈[[f]]e}.这就是说，[f]e描述了一组状态，参与人2可以从这些状态中为了让您能够更好地适应[[f]]e，一步到位比如说，应用在示例1中，将集合{s1，s2}转换为{s0}。上述公式可以象征性地计算，最多需要|S|2步骤，尽管它有三个交替定点运算符[10]。4可行的接口监控假设一个模M，一个规范Φ和一个接口规范ΦI。如果存在一个FDSI（一个可能的界面），则M-态的有限个prefixσ相对于M、 Φ和 ΦI是安全的，使得• σ是MI的某些计算的前缀;• 对于M I的每一个计算σJ，其中σ为前缀，σJ|= ΦΦ I.FDSI可以被看作是参与人2获胜策略的具体实现（接口）。事实上，可以证明，每一个这样的接口都诱导出一个在观察到σ之后适用的获胜策略。基于前面几节的讨论，我们现在可以制定一个更有效的运行时监控过程，在这个过程中，我们只分析一次游戏--在被监控的生产运行开始使用上一节的方法，我们构造了一个可划分的博弈G，它代表了模块和接口之间可能的交互，同时评估这种交互是否满足连接Φ iΦI和模块的相关公平性要求以及模块和接口之间的适当交织由于G是可划分的，我们将交替使用术语 设Init是满足M的初始条件Θ和由任何可能已经组合成G的自动机诱导的任何初始条件的状态集合。一个可行的监测算法的草图五、下面的定理陈述了算法MON的可靠性。定理4.1若Init/Wn Win，则M与Φ ∈ Φ I不相容。 也就是说，不存在使M I的接口|= Φ Φ I.A. Pnueli等人理论计算机科学电子笔记144（2006）7385• 在所监视的生产运行之前，分析游戏G，计算接口获胜的状态的集合Win。如果是Init/InitWin，则发出警报。• 开始生产运行。对于每一个观测到的M态的有限个Prefixσ，设h为G 的 相 应 历 史 ， 由 σ 诱 导 。 让 s 成 为 h 的 最 后 一 个 状 态 。 如 果s/∈Win，则发出警报。图五. 一种可行的预防维修算法MON定理4.2只有在观察到不安全的历史记录后，算法才发出警报。这两个定理的证明都是基于这样的观察：如果一个状态s，可由历史h到达，对于接口来说不是获胜的，则不存在接口I，当与M并行运行时，它可以保证h的所有延续不会违反ΦI ΦI。如果存在这样一个接口，我们可以从中得出一个策略，这是赢得接口，矛盾的事实，即监测观察到的状态，这是坏的接口。因此，如果发出警报，就没有办法防止违反安全性的计算我们还需要证明，由一次博弈引起的每一个违反Φ的无限历史h都是违反Φ ΦI的M的开放计算。事实上，考虑违反目标（ΦΦI）的历史h（turn=1) <$J ∈J（<$J）. 违反J ∈J（<$J）保证h满足M的所有公平性要求。 违反联合判决（turn= 1）保证h包含无限多个接口步骤。因此，h是M违背Φ <$ ΦI的开放计算。请注意，由于在没有设计错误的情况下，所有前缀都是安全的，Theo- rem4.2意味着如果生成警报，则系统中存在错误。由于我们对发现错误感兴趣，上述陈述表明我们的方法是可靠的。相反，在模型检查中，上述语句通常意味着完整性，因为目标是证明程序的正确性。示例4考虑对应于图6（a）中的SPL模块的FDS。假设规格为Φ：在−l0处标记2，接口指定为平凡Φ I：true。在图6（b）中，我们给出了一个SPL程序，用于一个接口I_n，使得M_nI_n|= Φ Φ I.因此，该模块与ΦΦ I兼容。如前所述，我们可以将I/O视为界面制胜策略的具体实现。考虑一个处于−l2ag1ag2的状态。很容易验证它是坏状态，假设轮到模块因此，当达到这种状态时，我们的监视器将发出警报。警报实际上是一个早期警告。虽然违法行为是无法预防的，但要确认违法行为需要采取很多步骤86A. Pnueli等人理论计算机科学电子笔记144（2006）73shared boolean布尔值1，布尔值2 = 0本地布尔错误= 0l0：while错误⎡⎤第二章：等待l1：标记1：= 0⎣1⎥⎦l3：如果标记为2，则错误：= 1l4：shared boolean布尔值1，布尔值2= 0m0：loop forever do⎡⎤m1：等待标记12：⎢中文（简体） ：=0⎥⎣3⎥2⎦m4：标记1：= 1m5：除了及早发现问题之外，我们的方法还有另一个显著的优势-我们能够识别问题。没有办法识别违反活性属性的行为，比如Φ：在−l0处使用传统的运行时监视，除非程序终止。 当然，我们不能总是捕捉到对活性但有时候，我们可以捕捉到最终的违规行为，就像我们在这个例子中所做的那样。此外，让我们将Φ修改为<$at − l 4。 即使在这种情况下，也不能保证在使用传统的运行时监控时会提醒用户，因为仍然有可能保持规范。实际上，模块可以放弃回合，并且界面可以将标志2重置为假，这将使游戏恢复到良好状态。(a) 模块M（b）接口I图六、示例4的模块和可能的接口5讨论方法的合理性和完整性我们的方法是合理的，这意味着每当MON发出警报时，模块和/或外部组件的实现中就存在错误但是，正如我们前面提到的，生成警报的执行跟踪实际上并不一定会违反规格。尽管如此，应该像对待模型检查的负面结果一样对待警报。当然，在实践中，可能需要区分程序中什么时候只有一个bug，或者什么时候bug会导致当前观察到的执行违反规范。为了实现这一点，我们像以前一样构建一个游戏，但让界面不仅为自己做出选择，而且还为模块做出选择。如果接口甚至在这些宽松的条件下也不能获胜，那么无论何时生成警报，都肯定会发生违规。我们还需要提到算法MON的不完备性。这意味着接口的获胜策略的存在并不一定意味着这个策略可以由SPL程序实现。 这主要是由于以下两个原因。首先，我们允许接口观察所有A. Pnueli等人理论计算机科学电子笔记144（2006）7387M的变量，即使是局部变量。此外，该接口还可以访问计算的完整历史。不完整性的实际后果是，监视器可能无法尽可能早地发现bug;有时它可能根本不会推断出一个bug。 然而，应该强调的是，一旦计算违反了规范，就会生成警报。因此，在这方面，MON总是比传统的运行时监控工具更好。注意，算法MON的不完整性不应与以下事实混淆。如果我们让博弈永远继续下去，没有警报并不能保证计算实际上满足了目标仅仅因为游戏保持在良好的状态，系统可能不会更接近满足其活性属性。不幸的是，任何声音运行-时间监控系统具有上述特点。状态爆炸考虑3.2节末尾的计算获胜状态的公式。计算集合Win所需的工作量与在存在公平性的情况下对模块进行模型检查相当两需要处理至少两个交替定点运算符。因此，两者都存在状态爆炸问题。幸运的是，与模型检查的并行性并没有到此为止，我们可以应用一些用于模型检查的流行补救措施特别地，可以在应用运行时监视之前抽象模块。为了保持方法的可靠性，我们可以允许接口解决所有由抽象引起的不确定性选择。当然，这可能会对完整性产生不利影响。有趣的是，首先使用运行时监控的原因之一可能是为了应对模型检查的复杂性。实际上，我们可以将程序中难以处理的部分标记为外部组件，并应用运行时监视。由于我们允许以拉宾链自动机的形式给出规范，因此可以抽象到任何必要的程度。在极端情况下，当外部组件的规格与其实现匹配时，运行时监控将降级为常规模型检查。6我们的贡献和相关工作博弈论的形式主义已被广泛应用于解决各种验证相关的问题。例如，在[11]中研究了开放系统的验证和综合问题，并且与我们的工作密切相关。然而，据我们所知，我们是第一个利用博弈论方法进行运行时监控的公司。 此外，我们还确定并提出了解决方案，在动态信息存在的情况下解决游戏的问题我们已经提到了我们的工作和运行时监视的“trans-mapping”方法之间的一些差异。最重要的是，我们要-88A. Pnueli等人理论计算机科学电子笔记144（2006）73针对不同的目标：跟踪监视与故障发现。因此，我们在很大程度上认为我们的工作与现有方法是正交的。然而，即使我们像传统监视器那样专注于特定行为，我们的方法也有几个优点。首先，我们能够处理活性属性，当接口无法绝对保证防止违反活性属性时，就会发出警报。 此外，在大多数情况下，我们可以在违规行为实际发生之前很久就发现它们。其中一种情况是多线程应用程序中的单个线程执行一系列本地计算，这些计算通常是确定性的。如果在这段时间内出现问题，则在进行任何实际计算之前生成警报。 这些信息可能有助于有许多方法，例如，增加日志记录的级别以促进稍后的调试/恢复过程可能是谨慎的。引用[1] Bowen Alpern和Fred B.施耐德定义liveness。Information Processing Letters，21（4）：181[2] Howard Barringer，Allen Goldberg，Klaus Havelund，and Koushik Sen.基于规则的运行时验证。在Proc. VMCAI[3] N. Bjorner，A.布朗，E。张，M。Colon，A.卡普尔山Manna，H. B. Sipma和T. E. 乌里韦STeP：反应式和实时系统的演绎算法验证。在Proc. CAV施普林格出版社[4] 莫顿·戴维斯在完全信息的有限博弈中。博弈论的进展，第85-101页。普林斯顿大学出版社，新泽西州普林斯顿，一九六四年[5] L. de Alfaro，T. Henzinger和R.马宗达从核查到控制：欧米伽定期目标的动态规划。Proc.LICS'01，第279-290页，2001年[6] L. de Alfaro 和T.A. 亨辛格同时进行的欧米茄常规游戏。在Proc. LICSIEEE ComputerSociety Press，2000.[7] D. Drusinsky和M.T.阿胜结合时间序列约束的时间逻辑规范监控。JUCS，9（11）：1261[8] R. Gerth，D. Peled，M.Y. Vardi和P. Wolper。线性时态逻辑的简单的自动验证。在Proc.PSTV[9] Yonit Kesten，Nir Piterman，and Amir Pnueli.弥合公平模拟和跟踪包含之间的差距在Proc. CAVSpringer，2003年。[10] D. Long，A.布朗，E。Clarke，S. Jha和W.马雷罗一种改进的不动点表达式求值算法。在Proc. CAVSpringer，1994年。[11] F.Y.C.芒游戏在开放系统验证和合成。博士论文，加州大学伯克利分校，2002年。[12] Z. Manna和A.普努埃利反应系统的时间验证：安全性。Springer-Verlag，New York，1995.[13] S.萨弗拉关于ω-自动机的复杂性。在Proc. FOCS'88 ，第319-327 页，White Plains ，NY，1988中。A. Pnueli等人理论计算机科学电子笔记144（2006）7389[14] A.P.西斯特拉时态逻辑中的安全、活性与公平。Formal Aspects of Computing，6：495[15] C.韩阳和David L.迪尔状态空间的引导搜索验证。见1998年6月发援会会议记录加利福尼亚州旧金山市