基于组件的软件设计中的程序行为和程序结构的组合验证问题的研究

理论计算机科学电子札记203（2009）87-101www.elsevier.com/locate/entcs用过程Marieke Huisman1，2INRIA Sophia Antipolis，法国Dilian Gurov Dilian Gurov3，4瑞典斯德哥尔摩皇家理工学院摘要在基于组件的软件设计中，关于程序的形式化推理必须是组合的，允许从其组件的属性中推断出全局的、程序范围的属性。本文讨论了用模态逻辑表示的顺序程序的行为控制流性质的组合验证问题。我们使用作为出发点的最大模型为基础的方法以前开发的作者，它假设的本地属性是结构（而不是行为）。为了处理当地的行为属性，我们提出了上述方法的组合，从行为属性的结构集的翻译。本文提出了一个直接的解决方案的逻辑，并准备了基础的翻译更有表现力的逻辑获得增加最大固定点递归。保留字：程序行为，程序结构，组合验证1引言背景基于组件的软件设计是一种设计范式，其中多个软件组件，每个组件都有自己的良好描述的功能，被组合成一个单一的应用程序。 这种技术作为一种手段正变得越来越普遍 构建先进复杂的软件系统但是，为了确保应用程序作为一个整体的良好运行和安全性，需要组合1部分由欧洲委员会IST FET方案在IST-2005-015905 MOBIUS项目下供资。2电子邮件：Marieke. sophia.inria.fr3由欧盟委员会IST FP 6方案在IST-FP 6-STREP-27004 S3 MS项目下提供部分4电子邮件：dilian@csc.kth.se1571-0661/© 2009 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2009.03.02888M. Huisman，D.Gurov/Electronic Notes in Theoretical Computer Science 203（2009）87验证技术，允许从组件的功能和安全属性得出结论。当系统中的不同组件可以相互通信和协作在移动代码的背景下，组合验证技术的开发变得更加相关，因为在这里，新的应用程序可以在运行系统上发布后下载。一般来说，我们研究的组合验证问题如下：如果我们希望确保组合应用程序具有全局属性φ，我们能否为不同的组件找到足以确保组合应用程序具有属性φ的局部属性φ。这个想法可以用下面的证明原理来描述（其中X是一个分量变量）：► A：φX：φXB：► AB：这一原则减少了表明A和B满足以下任务：• 通过找到A的局部性质φ来分解全局性质φ，• 证明分解的正确性，即，验证对于任何满足φ的X，与B构成的X满足φ（第二个前提），并且• 当选择了A的一个具体实现时，验证它是否满足局部性质φ（第一个前提）。在我们的工作中，我们专注于小程序，这是一个连续的过程语言描述的组件小程序配备了一个小程序接口I，它描述了其实现所定义和需要的方法极大模型的组合验证在早期的工作中，我们提出了一种基于最大模型的组合验证方法[9]，提供了工具支持，并通过智能卡生产商Gemplus [3]提供的工业电子钱包案例研究评估了其实用为了证明局部性质φ足以确保全局性质φ，我们计算了一个所谓的极大模型w.r.t. φ。这个模型是最大的，因为它模拟了所有具有属性φ的小程序。我们已经展示了如何为我们的模拟逻辑计算最大模型，这是模态μ演算的一个片段，只有框模态和最大固定点。我们区分两种性质：结构性质和行为性质。结构属性限制了可能的applet实现，而行为属性限制了可能的行为。对于结构属性φ和applet接口I，我们可以定义一个最大appletθI（φ），它精确地模拟了所有具有接口I的applet，具有属性φ。因此，我们可以证明下面的证明原理是合理和完整的（[9]中的定理3.11）：（结构）A |=sφθ I（φ）B|=bA B|=bA：我M. Huisman，D.Gurov/Electronic Notes in Theoretical Computer Science 203（2009）8789这一原则应理解如下。假设我们有一个局部结构假设φ，描述具有接口I5的小程序。如果我们想证明任何具有这种属性的小程序都可以安全地与某个已知的小程序B交互，特别是，这考虑到一些全局行为安全性质，我们通过为φ和I构造最大appletθI（φ），将其与B组合，并模型检查（使用合适的算法，参见调查[1]），得到的applet满足θ。为了安全地组合小程序A和B，我们还必须模型检查小程序A确实满足局部结构假设φ。然而，对于当地的行为特性，情况就更成问题了。一般来说，给定行为属性φ和接口I，不存在唯一的最大applet来模拟所有具有属性φ的applet（具有接口I）。假设我们有下面的行为公式[acallb]r，这意味着在从方法a到方法b的调用之后（即在b的入口点），原子命题r应该成立。即使对于这个简单的公式，也有两个最大的应用程序（提供和要求方法a和b）：第一个是每个满足公式的小程序都由这两个小程序中的一个来模拟;然而，这两个小程序并不相互模拟。用applet结构描述行为特性有几种方法可以解决这个问题。第一种可能性是用一个不一定是行为的模型来过度行为公式的最大模型给出了一个这样的近似值。一个更好的近似，可以通过一个标准的产品之间的构造小程序PDA诱导的最大的小程序为给定的接口和这个最大的模型。然而，这必然导致核查原则不完整因此，我们采取另一种方法，我们的目标是计算整个最大applet结构集，通过一组结构公式表征行为公式本文介绍了如何行为模态逻辑公式使用框模态只能由一组结构公式。 我们把这个模拟逻辑片段称为模态模拟逻辑。目前正在进行的工作是将这项工作扩展到最大的固定点;这需要使用画面结构，一个全局放电条件。我们表明，在公式不包含析取的情况下，这个特征是准确的。下面，我们提出了一个从行为模态模拟逻辑公式到（等效）结构属性集的翻译。 当局部假设是行为属性时，这是 如果一个行为属性可以用一组结构属性来表征，我们可以应用我们为结构属性定义的最大applet构造（见[9]）来获得一组最大5接口将在下面正式定义。 它们指定applet已知的方法集。90M. Huisman，D.Gurov/Electronic Notes in Theoretical Computer Science 203（2009）87行为属性的模型。然后，成分验证原则变为：一|=bφ{θ I（σ）B|=bχ}σ∈φI（φ）A：IA B|=b×A注意，不是显示A |=bφ它的表面显示A |=sσ，对于某个σ ∈ φI（φ）。除了填补我们的成分验证方法的空白之外，这种特征化本身也具有更普遍的意义，因为它揭示了结构与行为之间的关系特别是，在我们的翻译中，我们利用了一个行为属性是平凡的满足一个小程序，如果小程序的结构不允许这种行为。相关工作并发程序的组合验证已经得到了广泛的研究，特别是以基于假设/承诺的推理的形式对同步消息传递的进程进行推理，以及以基于依赖/保证的推理的形式对共享变量并发进行推理;参见De Roever等人 [7]对这些和相关证明方法的系统概述。 然而，这些技术不解决具有递归过程的程序。使用最大模型进行算法成分验证是由于Grumberg和Long [2]对CTL的uniform片段的使用，后来由Kupferman和Vardi [5]扩展到CTL*。这些作品研究公平性假设下的顺序进程的同步并行组合物。我们采用这种方法来模拟逻辑在当前的上下文中的组合验证的控制流属性的顺序程序与过程在[9]。据我们所知，目前的工作是第一个解决的表征的行为控制流属性的结构。本文结构第2节简要介绍了我们早期的结果，特别是程序的结构和行为，逻辑和最大模型的定义。它还介绍了有用的符号。第三节定义了行为模态仿真逻辑公式到结构公式的转换，并证明了其正确性。 第4节证明了无析取的行为性质的组合验证原理的可靠性和完备性，前提是局部假设由行为模态模拟逻辑描述。最后，第5节给出了结论并讨论了未来的工作。2分类：模型与逻辑我们简要回顾了构成我们的成分验证方法基础的一些定义和结果。对于完整的概述，读者可以参考[8，9]。M. Huisman，D.Gurov/Electronic Notes in Theoretical Computer Science 203（2009）87912.1模态模拟逻辑我们使用模态逻辑的一个子集作为我们的规范语言。在我们关于组合验证的工作本文所讨论的模拟逻辑的子集是模态模拟逻辑。在整个过程中，我们固定了一组标签L和一组原子命题A。定义2.1（模态模拟逻辑）模态模拟逻辑的公式归纳定义为：φ：：= p |p|φ1∧ φ2|φ1∨ φ2|[a] φ其中p ∈ A，a ∈ L。该逻辑的语义是模态逻辑的标准，并以模型（Kripke结构）的形式给出。特别地，公式[a]φ对一个状态（“可能世界”）成立，注意，常量公式true和false是可定义的;它们应表示为分别为tt和tt为方便起见，我们用φ1<$φ2表示<$φ1<$φ2。接下来，我们定义模型和规范的一般概念定义2.2（模型）模型是一个结构M=（S，L，→，A，λ），其中S是一组状态，→S×L×S是一个标记的转移关系，λ：S→ P（A）是一个赋值，给每个状态s分配在s中成立的原子命题。 一个规范S是一个对（M，E），其中M是一个模型，E是一组状态。直觉上，我们可以把E看作是模型的入口状态的集合。我们定义了满意度（M，s）的通常概念。|=φ且模拟（M1，s1）≤（M2，s2）（其中相关态满足相同的原子命题）。一个规范满足一个公式，如果它的所有入口状态都满足这个公式。一个规范被另一个规范模拟，如果对于它的所有入口状态，在另规范，它模拟了第一个入口状态。这种模拟关系保留（向后）逻辑属性。定理2.3 S1≤S2且S2|=φ隐含S1|= φ证明推论2.16 in [9]Q2.2Applet结构和行为我们的程序模型受[4]的启发，是基于控制流的，因此过度近似实际的程序行为。它定义了两种关于applet的不同观点：结构观点和行为观点。 这两种观点都是模型和规范的一般概念的实例化。特别注意，这些实例化产生了模拟和模拟逻辑的结构和行为版本。再一次，我们参考[8，9]以获得更多细节。92M. Huisman，D.Gurov/Electronic Notes in Theoretical Computer Science 203（2009）872.2.1Applet结构由于我们从所有数据中抽象出来，applet结构被定义为applet实现的方法的调用图的集合。设Meth是一个可数无限方法名集合。方法规范是一般方法具体化的概念定义2.4（方法规范）在方法名的有限集合MM th上的m∈Mth的方法图是有限模型Mm=（Vm，Lm， →m，Am，λm）其中Vm是 m的控制节点的集合，Lm=M<${ε}，Am={m，r}，并且λm：Vm→P（Am）使得m∈λm（v）对于所有v∈Vm（即， 每个节点用它的方法名标记）。其中r ∈ λ m（v）的节点v∈Vm称为返回点。m∈MethoverM的一个方法规范是一个对（Mm，E m），其中Mm是M上m的一个方法图，E m∈ V m是m的一个非空入口点集。接下来我们定义applet接口的概念。定义2.5（Appl eti nterf ace）一个appletint erface是一个 对I=（I+， I−），其中I+，I−Mth分别是提供的和需要的方法的名称的有限集合。两个界面I1=（I+，I-）和I2=（I+，I-）的合成为：定义为I1<$I2=（I+<$I+，I−<$I−）。1 1 2 21 2 1 2为了正式定义具有接口的小程序的概念，我们使用规格的不相交并集S1S2的概念，其中每个状态分别标记为1或2和一（s，i）−→S1±S2（t，i），对于i∈ {1，2}，当且仅当一s−→Sit.定义2.6（Applet）一个appletA，带有实现接口I，写A：I，归纳地定义为：• （Mm，Em）：（{m}，M）如果（Mm，Em）是m∈ Meth的方法规格，M和• 如果A 1：I1和A 2：I 2，则A 1 A 2：I 1 = I2。A nappletissclos eddifI−I+，i. e. 这不是一个简单的方法。模拟和满意度，实例化到这种特定类型的模型称为结构模拟≤s，结构满意度|=s，分别。例2.7为了说明结构模态模拟逻辑中的性质，考虑第一个公式a [b]（如上所述，它将<$a [b]简化）。它对控制节点v成立，如果v |=<$a（即a/∈ λ（v），意味着v不属于方法a），否则所有节点 v，J，使得Bv−→a vJsatisfy，意思是不这样的节点v J存在（因为没有节点满足v j）。 这个公式对applet成立，如果它对它的所有入口节点都成立;因此它指定了从方法a的任何入口节点，都没有对方法b的调用边。类似地，公式b r指定方法b的任何入口节点都不是返回节点。M. Huisman，D.Gurov/Electronic Notes in Theoretical Computer Science 203（2009）8793模态逻辑不能表达一般的不变或可达性性质，例如b2.2.2小程序行为接下来，我们在行为层面上实例化规范m∈ I+v →mv Jv |=<$r（转账）（v，σ）−→τ（vJ，σ）m，m ∈I+m2vJv|=<$r1 2 v1−−→m111v 2|= m 2v 2∈ E（电话）m1呼叫M2J（v1，σ）−→（v2，v1·σ）（返回）m1，m2∈ I+v2|= m 2rv 1|= m1m2retm1（v2，v1·σ）−→（v1，σ）图1. 小程序转换规则定义2.8（行为）设A=（M，E）：I是一个封闭的applet，其中M=（V，L，→，A，λ）。A的行为由规范b（A）=（Mb，Eb）描述，其中Mb=（Sb，Lb，→b，Ab，λb）使得Sb=V×V，即状态（也称为配置）是控制点和堆栈对，Lb={m1km2|k ∈{call，ret}，m1，m2∈I+} ∈{τ}，→b由Figure1的公式定义，Ab=A，且λ b（（v，σ））= λ（v）.初 始 状 态 的 集 合 E b 定 义 为 E b= E × {\displaystyle\mathbb {E}} ， 其 中\displaystyle\mathbb{E}表示V上的空序列。注意applet行为定义了一个下推自动机。 我们利用这个用于PDA的模型检查器，以验证行为属性（参见，例如，，[1]用于无限过程结构的验证技术调查）。同样在行为层面上，我们实例化了模拟≤b和满意度的定义|=b：A1≤bA2惠b（A1）≤b（A2）且A|=bφ惠b（A）|=φ。任何两通过结构模拟相关的小程序也通过行为模拟相关（[9]中的定理3.9），但反过来不成立（因为行为模拟只需要相关的可达状态）。例2.9作为行为模态模拟逻辑中的一个性质的例子，考虑公式[a call b] r。一个配置（v，σ）满足公式，如果通过执行从方法a到方法b的调用从（v，σ）到达的所有配置都满足r（即，有一个返回节点作为控制点）。如果applet的所有初始配置都成立，则该公式对applet成立;因此，它规定，如果applet的第一个操作是从方法a到方法b的调用，则紧接着94M. Huisman，D.Gurov/Electronic Notes in Theoretical Computer Science 203（2009）87我们应该在一个返回节点同样，不变的行为属性，如2.2.3清理applet结构请注意，方法规范允许返回点有向外的边。然而，只有当小程序在返回节点中没有输出边时，由一组稍后定义的结构公式对行为属性的表征才是正确的;这样的小程序被称为干净的。我们定义了一个一元的cleaning操作，返回一个具有相同行为的干净applet。定义2.10 [清洗]给定方法规范Mm=（Vm，Lm，→m，Am，λm），则清洁的一元操作由以下定义：M·=（Vm，Lm，{s−→lmt|s−→lmt<$r/∈λm（s）}，Am，λm）很容易看出清理过的小程序是干净的。我们列出了几个有用的清洁性能。（A·）·=A·一|=bφ惠A·|=bφ（A·，s）|= sr l，σ. （A·，s）|= s[l] σ因此，清洁是幂等的，并且保留了行为特性。而任何作为返回点的状态，都在结构层面上满足任何盒子公式。下面，在特征化的正确性证明中，我们将定义可达性的概念（行为可以到达的节点集），我们将在干净的小程序上使用它，这与盒公式的满足一致2.3使用极大小程序的我们的组合验证方法，在[9]中提出，是基于性质φ的最大模型的计算。如果一个模型模拟了所有其他具有性质φ的模型，则该模型被称为对于性质φ是最大的。然而，当我们在applet结构（或applet行为）上有一个性质φ时，我们不能确定φ的最大模型也是一个合法的applet结构（或applet行为）。 对于applet结构，这个问题可以解决，因为我们可以精确地识别合法的applet结构。接口I作为模拟逻辑中的公式（在结构级实例化）。如果φI是具有接口I的applet的特征公式，并且φ是任意结构公式，则公式的最大模型φ<$φI精确地描述了所有接口I满足φ的applet。 如果我们定义最大applet w.r.t. φ和I，记为θ I（φ），是性质φ <$φ I的极大模型，则我们可以证明下面的合成验证原理对于全模拟逻辑是可靠的和完备的（[ 9 ]中的定理3.11）：M. Huisman，D.Gurov/Electronic Notes in Theoretical Computer Science 203（2009）8795ˆ（结构）A |=sφθ I（φ）B|=bA B|=bA：我对于我们的子集模态模拟逻辑，我们只能证明这个规则的可靠性为了建立完整的模拟逻辑的完整性，我们使用每个模型都可以用特征公式来描述。但是，由于规格可以包含循环，因此最大固定点的可用性在这里是必不可少的。如上所述，没有这样的方法来精确地验证applet行为，因此我们不能为applet行为上的局部公式建立相同的组合验证原理的可靠性和完整性。下面我们将定义一种将行为公式转换为结构公式的方法，这将使我们能够利用applet结构的组合验证原理执行applet行为属性的组合验证2.4记法惯例我们用标号ε表示applet结构中的转移边，用标号τ表示无声的递归转移。对于序列σ，我们用σ表示顶部元素（头），用σb表示去掉顶部元素的序列（尾），即（v·σ）=v和（v·σ）b=σ。空序列表示为，其中和b是未定义的。在模态模拟逻辑公式的翻译中，我们允许标签序列α在boxmodalities中出现，并将其转换为标准公式：[]=^ ^您的位置：[l·α]=[l] [α]3表征行为特性在本节中，我们假设小程序是干净的;如果不是，可以按照上面的解释清理它们，而不改变行为。我们定义了一个从行为属性到结构属性集的映射，我们可以证明，一|=bφ <$$> σ ∈ <$（φ）。一|=sσ这不是一个等价的原因是（与逻辑的其余连接不同）析取不能被组合地处理：A的有效性|=bφ不能仅从A的有效性（或无效性）推断|=bφ和一|=b，因为A|因为A的某些初始配置满足φ，其余满足φ。然而，如果行为性质φ不包含析取，则映射是精确的，并且我们获得等价性（即，我们找到表征行为性质的精确结构公式集）。一|=bφ惠σ∈φ（φ）。一|=sσ（φ disjunction-free）（1）96M. Huisman，D.Gurov/Electronic Notes in Theoretical Computer Science 203（2009）87⎨b{tt}i/=a⎧π（i，F）·H（p）={i<$[F] p} <${iJ<$[FJ]<$|（iJ，FJ）∈H}π（i，F）·H（<$p）={i<$[F]<$p} <${iJ<$[FJ]<$|（iJ， FJ）∈H}π（i，F）·H（φ1<$φ2）={σ1 <$σ2|σ1∈π（i，F）·H（φ1），σ2∈π（i，F）·H（φ2）}π（i，F）·H（φ1<$φ2）=π（i，F）·H（φ1）<$π（i，F）·H（φ2）π（i，F）·H（[τ]φ）=π（i，F·ε）·H（φ）{tt}如果我是π（i，F）·H（[acallb]φ）=<$π（b，n）·（i，F·b）·H（φ）ifi=aBπ（i，F）·H（[aretb]φ）=<${i<$[F]<$r}<$πH（φ） 如果i=a<$π1（H）=b图2. 映射πH3.1将行为特性映射为结构特性我们的翻译是基于行为属性的象征性执行。首先，我们定义（辅助）映射πH：Behform→ P（Structform），由非空历史堆栈H参数化。历史堆栈中的每个元素都是一个元组，包含当前方法名称和一个边标签序列（称为frame），即：e. ：H：（I+×（I−ε }）ε）+.映射π最初应用于包含具有空帧的单个元素的初始历史堆栈我们用H，m来表示这个单元素序列（m，）。历史堆栈更新如下：• 当行为属性规定了从a到b的调用，并且H的顶部元素在方法a中时，我们在该帧的末尾添加b，并且我们将新元素（b，n）推到H上;• 当行为属性规定从a返回到b时，H的顶部元素在方法a中，并且前一个元素在方法b中，我们从H弹出顶部元素;并且• 当行为性质规定了内部转移时，我们将ε附加到H的顶元素的框架的末尾。映射π在图2中通过对公式结构的归纳来定义映射象征性地执行公式，并且对于它遇到的标记有返回的每个框模态，它生成一个结构公式，该结构公式捕获这种行为不可能发生的可能性。然后，递归调用将生成其他结构公式，这些公式必须在所描述的行为实际发生的情况下保持不变。标记有调用或内部传输的框模态的符号执行不会产生任何显式结构公式M. Huisman，D.Gurov/Electronic Notes in Theoretical Computer Science 203（2009）8797（捕捉这种转变是不可能的可能性），因为这样的公式将总是被由剩余公式生成的结构式所包含。当翻译遇到一个原子命题（的否定）时，它会生成一个公式，描述原子命题在当前框架中成立的情况。此外，它生成表征applet不满足历史栈中收集的一个或多个结构约束的可能性的公式（在这种情况下，当前原子命题将永远不会被评估）。注意πH（tt）={tt}。进一步注意，历史堆栈的非空性是构造的不变量。最后，我们可以定义φ w.r.t.的映射。 给定接口I：I（φ）={m∈I+σm|σm∈π<$H，m（φ）}最后一个表达式导致公式数量的爆炸，但请注意，对于成分验证，我们只需要最弱的结构公式这一套。特别是，只要集合包含tt，所有其他元素都可以从集合中删除，因为任何applet都将满足局部假设tt。3.2示例这个映射的工作是最好的解释与一些例子。我们始终假设I=（{a，b，c}，{a，b，c}）。例3.1考虑以下翻译。π<$H，a（[acalla]r） =π（a，n）·（a，a）（r） ={a<$r，a<$[a]<$}πH，a（[acallb][bcall a][ acallb] r）={ br，a[b]，b[a]}πH，a（[ acallb][bret a][ acallc] r）={ cr，a[b·c]，b<$ r}πH，a（[ acallb][bret d]）={tt}第一个属性涉及自调用，第二个是回调，第三个是返回。最后一个属性显示了如何检测无意义返回（导致公式为空真）。下一个例子展示了一个调用行为的整个接口的计算例3.2我们研究例2.9中的性质。π<$H，a（[ acall b] r）={ b<$ r，a<$[ b]<$}πH，b（[acall b] r）={tt}πH，c（[acall b] r）={tt}I（[acallb]r）={b98M. Huisman，D.Gurov/Electronic Notes in Theoretical Computer Science 203（2009）87A Aa最后，最后一个例子展示了整个接口的计算，只有内部行为。实施例3.3πH，a（[τ]）={ a[ ε]}π<$H，b（[ τ]<$）={ b<$[ ε]<$}πH，c（[τ]）={ c<$[ ε]<$}bc}3.3翻译的正确性为了证明翻译的正确性，我们通过在历史堆栈上相对化满意度的概念来概括它。至于翻译，在证明中我们也假设appletA是干净的。直觉，满足的广义概念，相对w.r.t. H，可以理解为：A|如果对于方法i中的任何节点v，可以通过遵循方法i中的框架所描述的路径来到达，则公式φ对于小程序A成立。H的顶部元素，对于对应于历史堆栈其余部分的任何调用堆栈σ，我们有（v，σ）|=bφ。为了正式地定义它，我们需要几个辅助定义。首先，我们定义一个函数reach，它计算给定的appletA，一组节点V和标签序列L，其中节点在A中是从V中的节点可达的，下面是带有L中标签的边。达到A（V，V）=Vreach（V，l·L）=reach（{v，J|v∈V <$v−→lvJ}，L）具体调用栈σ和历史栈H之间的对应关系定义如下：如果σ=v和H=（i，F），那么我们要求v∈到达A（Ei，F），并且σb和Hb对应。其正式定义如下：γA（i，f）=tt γA（v·σ，f）=<$γA（i，F）·H）=<$γA（ v· σ，（i，F）· H）= v∈reachA（ Ei，F）<$ γA（ σ，H）注意，γA（v·σ，<$H，i）在v∈Ei且σ=<$时成立，因为v∈Ei在v∈reachA（Ei，n）.我们现在准备正式定义满足的广义概念定义3.4给定appletA和历史堆栈H，我们定义广义满足w.r.t.H通过：一|=Hφ惠V，σ。（γA（v·σ，H）<$（v，σ）|=bφ）M. Huisman，D.Gurov/Electronic Notes in Theoretical Computer Science 203（2009）8799BH，m一|=（i，F）·H [a call b] φWhy？（v ∈ reachA（Ei，F）<$γA（σ，H）<$（v，σ）|=b[a call b] φ）{Def. 3.4，γA}Why？（v∈reachA（Ei， F）<$γA（σ，H）<${D ef. |=b}B1，2。（v−→iv1<$v2∈Eb<$（v2，v1·σ））|=bφ））惠率v，v1，v2，σ. （v∈reachA（Ei， F）<$γA（σ，H）<$v−→biv1<$v2∈E<$ {Logic}（v2，v1·σ）|=bφ）惠率v1，v2，σ. （v1∈reachA（Ei， F·b）<$γA（σ，H）<$v2∈Eb<${D ef. 反应A}（v2，v1·σ）|=bφ）惠率v1，v2，σ. （v2∈Eb<$γA（v1·σ，（i，F·b）·H）<$（v2，v1·σ）|=bφ） {D ef. γA}惠率v1，v2，σ. （v2∈reachA（Eb，H）<$γA（v1·σ，（i，F·b）·H）<$（v2，v1·σ）|=bφ）{D ef.反应A}惠率v1，v2，σ. （γA（v2·v1·σ，（b，n）·（i，F·b）·H）<$（v2，v1·σ）|=bφ）{D ef. γA}惠A|=（b，c）·（i，F·b）·H φ{Def. 3.4}惠σ∈π（b，c）·（i，F·b）·H（φ）. 一|=sσ{Ind. 好的。}惠σ∈π（i，F）·H（[acallb]φ）. 一|=sσ{D ef. π}图3. case[acallb]φ的正确性证明满足的标准概念与相对化的满足概念的关系如下。Proposi tion3.5A|=bφ惠m∈I+. 一|=φ我们现在可以陈述主要定理，它使我们能够证明翻译的正确性。定理3.6设A是applet，H是历史栈，φ是无析取的行为公式。然 后 又道：一|=Hφ惠σ ∈ π H（φ）。一|=sσ证明这个定理已经被形式化，并通过使用φ的结构上的归纳法用PVS定理证明器[6]证明是正确的。证明中使用的两个主要属性如下：• （E_i，L）_v∈reachA（E_i，L）_v|=σ）优惠A|= [L] σ• （|（i，F）∈ H}. 一|= φ）其余的证明是对定义的仔细重写，案例分析和逻辑的使用。图3显示了最有趣的情况之一的完整推导，即当i=a时的case[acallb]φ。Q等价性（1）是定理3.6和命题3.5的直接推论。4行为特性上一节的结果证明了下面的组合验证原则，其中φ是模态模拟逻辑的行为公式一|=bφ{θ IA（σ）B|=bχ} σ∈θ（φ）IAA：IAA B |=bX100M. Huisman，D.Gurov/Electronic Notes in Theoretical Computer Science 203（2009）87注意，不是显示A |=bφ它的表面显示A·|=sσ对于某些σ∈φ（φ）IA.这个规则的合理性来自等式（1）和结构式（结构）的组成验证原理的合理性。因为如果我们把自己限制在模态模拟逻辑中，组合验证原理是不完备的，所以我们得不到完备性。然而，由于本文中描述的行为公式的特征是精确的，只要公式不包含析取，一旦它被扩展为最大固定点，我们就可以利用满意度和模拟相互重叠的事实，也可以得到行为公式的完整组合验证原则。5结论本文介绍了从行为到结构特性的翻译。这种转换被定义为所谓的模态模拟逻辑，它对应于仅具有框模态的模态逻辑。在早期的工作中，我们定义了一个组合验证原则，其中局部性质必须是结构性质。基于这一原则，我们开发了一种成分验证方法，通过工具集提供了机器支持，并在工业案例研究中评估了该方法的实用性通过从行为性质到结构性质的转换，我们将成分验证原则扩展到了行为性质。翻译通过行为公式的符号执行进行：这个公式中的每一个它已在Ocaml中实现，并包含在工具集中。我们为之定义翻译的逻辑片段是相当有限的，但本文所描述的工作构成了一个更大项目的一部分，我们正在将翻译扩展到最大的固定点。这种扩展要求将平移转换成一个tableau构造，展开最大的固定点算子，直到某个全局放电条件成立，这意味着固定点已经充分展开以捕获所有结构属性。然而，我们认为模态逻辑片段的翻译本身值得详细描述，因为这是翻译中行为和结构之间相互作用最突出的地方。在不同的工作领域，我们目前正在研究是否可以将翻译扩展到也考虑到钻石模式。然而，由于钻石形态无法通过标准模型的模拟来表征，因此这不会进一步有助于我们的成分验证工作。引用[1] Burkart，O.， D. Caucal，F. Moller和B. Ste Escheren，无限结构的验证，在：J。伯格斯特拉，A. Ponse和S.Smolka，editors，Handbook of Process Algebra，North Holland，2000 pp.545-623.[2] 格伦贝格岛和D. Long，Model checking and modular verification，ACM TOPLAS16（3）（1994），pp. 843-871M. Huisman，D.Gurov/Electronic Notes in Theoretical Computer Science 203（2009）87101[3] Huisman，M.，D.古罗夫角Sprenger和G. Chugunov，Checking absence of illegal applet interactions：a case study，in：M. Wermelinger和T. Margaria，编辑，软件工程的基本方法，FASE84比98[4] 詹森，T.，D. L. Métayer和T. Thorn，基于控制流的安全策略的验证，在：IEEE安全和隐私研究研讨会（1999年），pp. 89比103[5] Kupferman，O.和M. Vardi，模块化模型检测的自动机理论方法，ACM TOPLAS22（2000），pp. 87比128[6] Owre ， S. ， J. Rushby ， N. Shankar 和 F. v. Henke ， Formal veri fication for fault tolerantarchitectures ： Prolegomena to the design of PVS ， IEEE Transactions on Software Engineering21（1995），pp. 107比125[7] Roever ， W.-警 察 ， F. D.布 尔 、 美 国 Hannemann ， J. Hooman ， Y. Lakhnech， M. Poel和 J. Zwiers ，“Concurrency Verification：Introduction to Compositional and Noncompositional Methods”，第54期，剑桥大学出版社，剑桥，英国，2001年。[8] Sprenger ， C. ， D. Gurov 和 M. Huisman ， Simulation logic ， applets and composite verification ，Technical Report RR-4890，INRIA（2003）。[9] Sprenger，C.，D. Gurov和M. Huisman，智能卡小程序安全加载的组成验证，在：合作设计的正式方法和模型（Memocode 2004）（2004），pp. 211-222