模块化系统的形式化方法及其在PVS定理证明器中的应用

理论计算机科学电子笔记116（2005）185-198www.elsevier.com/locate/entcs一个组成框架用于正式安装的模块化系统1卡洛Furia和Matteo Rossi2Dipartimento di Elettronica e Informazione，Politecnico diMilano 32，Piazza Leonardo da Vinci，20133 Milano，Italy摘要我们提出了一个工具支持的框架，证明了一个复杂系统的各个部分的行为的组合，确保了整个系统所需的全局属性。在PVS定理证明器的逻辑中正式引入了一个组合推理规则并进行了编码。的推理规则的使用方法的考虑，然后使用的框架来证明一个简单的，但重要的，控制系统的一个有意义的属性关键词：形式验证，模块化系统，实时，组合性。1介绍随着系统规模的增长，能够将其细分为组件对于控制其复杂性至关重要。特别是，人们希望单独指定和设计单个组件，然后能够保证它们在相互交互时也能正确工作。事实上，在关于外部世界的行为的某些假设下正确操作的部分在与不满足那些假设的整个系统的其它元件交互时可能行为不当（例如，接受具有频率r的输入的数据分析器可能1由MIUR项目提供的工作支持：“Q U A C K：P i a ttfor m2 电子邮件地址：rossi@elet.polimi.it1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.076186C.A. Furia，M.Rossi/Electronic Notes in Theoretical Computer Science 116（2005）185当连接到以频率2r）发送数据的传感器时工作不正常。形式化方法越来越被认为是开发应用程序的有用工具，特别是关键应用程序，因为它们允许在早期开发阶段精确验证系统的正确性，在未捕获的错误变得过于昂贵甚至灾难性之前。然而，通常归因于形式方法的一个问题是，它们不能当系统变得复杂时，它们太笨重和难以操作而不能有效地使用。在这方面，组合框架可以提供帮助，因为它允许人们首先关注系统的单个部分，然后分析它们之间的相互作用，如果在集成时同时考虑应用程序的所有方面（本地和全局），则需要更小的时间。一个好的、面向证明的组合框架必须基于合理的推理规则，这些规则允许人们从系统单个部分的行为中推断出系统的全局属性。此外，对于实际可用的框架，它应该由（半）自动工具支持，以便于分析建模的系统。在过去[2]中，人们已经研究了将单个规范组合成复杂系统的规则，而且，不仅如此，还参考了时态逻辑[1]第三节。本文提出了一个有效的推理规则的TRIO规范语言[5，6]，是适合于形式证明的正确性的行为模块化系统的组成部分。该规则已被编码在PVS定理证明器的逻辑中[7]，并且已经开发了支持策略。本文的结构如下：第2节简要介绍了TRIO语言，使用第5节中分析的应用程序的规范作为示例;第3节介绍了我们的TRIO组合框架所基于的推理规则;第4节描述了支持该框架的基于PVS的工具;第5节介绍了使用组合框架的一些方法论考虑，并展示了如何将其应用于简单但有意义的控制系统;第6节得出了一些结论，并概述了这一研究领域的未来工作2三人TRIO [5，6]是一种类型化的线性度量时态逻辑，具有面向对象和模块化的功能，用于编写复杂系统的规范3由于篇幅所限，我们没有广泛地介绍与本研究相关的文献。感兴趣的读者可以参考[3]与相关的相关作品进行比较。C.A. Furia，M.Rossi/Electronic Notes in Theoretical Computer Science 116（2005）185187操作者TRIO定义P ast（ A，d）Futr（ A，d）Som（ F）Alw（女）AlwP（ F）AlwPi（ F） Lasts（F ， t ）Lasted（ F，t ）UpT oNow（ F）现在（F）d>0Δ Dist（ A，−d）d>0径向距离（A，d）DidDist（F，d）DidDist（F，d）d（d>0（0 TD_Fmla]，这是一个从实例到TD_Fmla的函数。这种特殊的参数-PVS中模块导入的TRIO语义需要抽象化理论来实现。事实上，PVS不允许导入同一理论的多个实例，而TRIO允许。这个问题可以通过导入相同PVS理论的多个实例来解决，实例参数使用不同的实际值（每个对应的TRIO模块一个）。例4.1[PVS中的储集层系统]让我们考虑PVS中储集层系统首先，将储液器系统类映射到以下PVS理论（类似于储液器和控制器类）：reservoir_system [instances：TYPE+，fr：posreal，.]：理论然后，我们声明两个类型，用于标识水库和控制器类（即PVS理论）。Res_type：TYPE = {n：nat| n = 0}包含0 Ctl_type：TYPE= {n：nat| n = 0}包含0IMPORTING reservoir[[instances，Res_type]]，7我们的编码基于[4]中的结果，该结果处理TRIO的小特征。8TD Fmla是时间相关公式的PVS表示，如[4]中所定义。192C.A. Furia，M.Rossi/Electronic Notes in Theoretical Computer Science 116（2005）185控制器[[instances，Ctl_type]]然后，定理水平保持在类别水库系统的边界之间（参见第2节中的示例2.4）被转换为下面所示的PVS公式Res：VAR [[instances，Res_type]]level_stays_between_bounds：定理Alw（reservoir.level（Res）>= L_l与储液器液位（Res）= L_u）TRIO语言的两个重要特性，即继承和可见性管理，不能正确地转换为相应的PVS结构。事实上，虽然PVS确实有一些机制来支持代码的重用和执行最小的信息隐藏，但它们太弱，不够灵活，无法有效地表示相应的TRIO功能。因此，继承和可见性管理应该完全由前端工具来实现，这些工具将作为用户和PVS引擎之间的接口。基本上，这些工具将确保TRIO代码自动转换为PVS代码，尊重这些重要的面向对象特性的TRIO语义。事实上，这些工具目前正在开发之中。为了简洁起见，我们没有举例说明PVS结构在翻译TRIO继承和可见性方面的局限性;感兴趣的读者可以在[3]中找到它们。4.2TRIO证明的PVS策略PVS证明策略是一个脚本，可以自动化频繁发生的证明过程，帮助管理PVS功能和TRIO映射的低级别细节。本节简要介绍了PVS策略，该策略旨在帮助TRIO模块化规范的PVS证明，特别是可靠/保证规范。在PVS证明过程中，我们必须有效管理的第一个功能是使用实例化参数，这些参数将PVS中不同的TRIO模块分开（见4.1节）。由于对应于TRIO类的PVS理论的每个项相对于实例类型的变量是参数化的，所以当我们操纵PVS中的公式时，无论是为了证明它们，还是使用它们来导出其他属性，我们都必须用相同类型的Skolem变量替换那些通用变量这样做的前件和后件的公式在PVS证明，证明者承认我们是指环相同的项目，并可以验证证明。因此，一些策略旨在减少处理这些频繁发生的实例化所需的用户交互。基本上，当开始证明时，C.A. Furia，M.Rossi/Electronic Notes in Theoretical Computer Science 116（2005）185193−{∈≤联系我们新引入的Skolem变量到持久表中。之后，每当在PVS中引入另一个公式时，其他策略都会重用我们存储的值来执行必要的实例化trans-mitting。特别是，我们可以存储多组实例化值，然后决定使用哪一组来执行给定新公式的实例化将这些基本策略与实现时态值实例化的方法的其他策略相结合，我们构建了通常能够以方便使用的形式呈现公式的命令，而无需显式的用户交互。其他一些策略是专门为简化第3节的依赖/保证框架所指定的系统的证明而定制的。 首先，PVS理论声明了以一种在证明过程中方便使用的方式来翻译+d运算符和第3节的依赖/保证推理规则所需要的内容。这个理论必须在执行可靠/保证推理的所有其他理论中导入。为了将公式E i s和M i s的集合转换为PVS，我们声明类型为[iN：1 i nTD Fmla]，和 将i的每个值与我们正在组成的模块相关联。由于这种做法，我们经常不得不将证明分成n个分支，每个分支对应一个模块。一些策略以一种方便的方式实现了这种拆分，并且通过将通常的PVS简化算法与有关模块索引的信息相结合，通常可以关闭每个分支，而无需进一步的用户交互。5为例我们考虑的案例研究是第2节介绍的受控油藏系统。在本节中，我们简要回顾了本案例研究（第5.1节）规范发展过程中出现的一些方法学方面，包括第3节中信赖/担保框架的应用。此外，我们概述了全局正确性属性水平保持在边界之间的证明（见第2节），这是使用先前介绍的合成推理规则（第5.2节）证明的。5.1方法性的考虑储层系统的具体化是两步细化过程的结果，利用了TRIO继承机制。类的第一个版本仅通过公理描述了组件的基本行为。没有对环境做任何假设，也没有派生任何高级属性，因此这个基本内核尽可能地可重用。类的第二个版本更详细地指定了194C.A. Furia，M.Rossi/Electronic Notes in Theoretical Computer Science 116（2005）185−组件，还假设对与模块交互的环境（即其他组件）的派生属性的陈述依赖于环境假设，如依赖/保证属性。我们相信，这个基本的两阶段发展类的方案可以富有成效地应用于一般组件的指定。显然，虽然规范的第一个版本通常是通用的，足以成为唯一的，但根据不同的操作系统，可能有几个不同的第二个版本。此外，多步细化是这个基本方案的自然扩展，每一步都添加了所需的细节在系统的导出性质中，连续性和非Zenoness起着重要的作用[4]。事实上，由于例2.2中描述水平项行为的公理，以及状态项的特征，我们可以证明水平是作为时间的函数的分段多项式9这个结果允许我们保证一个性质在未来的有效性“一次更长”（就像在− + doperator中一样）。应用Section3是选择公式作为模型的假设和保证。一个好的选择是有效地将全局属性的验证负担分配给复合系统的类，同时最小化模块之间的耦合。在这方面，框架的应用似乎更简单，更“自然”，只要有某种反馈关系的项目组成的特别是，在这些情况下，+d的应用更简单，因为反馈作用确保了将来作为反应的属性的有效性过去持有的另一处房产请注意，大多数受控系统都表现出这种关系，我们例子中的水库系统也不例外。让我们最终考虑TRIO假设（即时间闭合假设）在可靠/保证规范中的作用。 按照章节所述3，一个组件的可靠/保证规格基本上可以简化为一个单一的E−+dM类型的多个，其中E公式称为“一个假设”，E和M可以是任意复数公式，也可能由一些暂时关闭的子公式组成每当时间封闭公式参与到依赖/保证规范中时，我们可以使用TRIO关键字假设来假设它们。然后，当将类与其他模块组合时，这些TRIO假设必须从系统中其他组件的公式中删除（即证明）。如果我们能够解除所有的假设，那么系统的所有衍生性质（特别是rely/guar的应用[9]一个奇异函数f（t）使得k，c∈R：f（t）=k·t+c.C.A. Furia，M.Rossi/Electronic Notes in Theoretical Computer Science 116（2005）185195≤−++¬antee推理规则）保证是合理的。从方法论上讲，这种进行方式可以改善证明和规范的组织。5.2应用本节概述了第3节的信赖/保证框架的应用，并概述了最显著性质的证明reservoir类引入了一个关于填充动作行为的假设：如果reservoir已满，则不会发出填充动作（公式为满时不填充，为简洁起见，此处未显示10）。相反，控制器类做出以下假设：• 水平是时间的分段右单调函数（水平单调性）;• 如果发出填充命令，则液位增加（填充使液位升高）;• 如果水平现在大于或等于L u，则它将在下一个时间单位（delta定义）内保持在L l以上。此外，满足约束条件<$（Lu Ll）/lr。 现在让我们考虑依赖/保证框架的应用。水库和控制器类的依赖/保证行为由以下定理形式化。定理4（油藏动态）水平≤Lu−d水平≤Lu定理5（控制器行为）level≥Ll−d level≥Ll让我们简略地证明这两个定理。 根据− +运算子的定义，reservoir行为的证明分为两个分支AlwP（level ≤L u）<$level ≤L u和AlwP i（level ≤L u）<$NowOn（level ≤L u）。根据U pT oN ow（填充）或U pT oN ow（填充），将其分为两种情况。请注意，没有其他情况需要考虑，因为filling是一个状态项。 如果不及时（填充），这是微不足道的，因为水平肯定不会增加。相反，如果U pT oN ow（填充），我们依赖于假设当充满时没有填充来推断在当前水平不能突然上升到Lu以上同样，另一个分支”“是的，是的。同样，NowOn（填充）的情况很简单，因为水平没有提高。的情况NowOn（填充）可以通过矛盾来关闭，假设<$NowOn（水平）<，并将其与假设完全不填充相结合。的 证明 的 控制器行为 是 类似地 分裂 成 树枝[10]本节中提到了许多公式，但为了简洁起见，没有实际显示。感兴趣的读者可以在[3]中找到案例研究的完整形式化196C.A. Furia，M.Rossi/Electronic Notes in Theoretical Computer Science 116（2005）185¬¬¬≡++≡ ≤≤AlwP （ level≥L1 ） 表 示 水 平 ≥L1 ， AlwPi （ level≥L1 ） 表 示 现 在 开 始（level≥L1）。 正如在这些证明中所做的那样，我们将第一个分支分为U pToN ow（填充）和U pT oN ow（填充）两种情况。最简单的情况是U pT oN ow（灌装） 以来 的 水平 是 明确地 提高。相反地，如果UpT_oN_ow（填充），我们可以利用假设delta定义来推断泄漏动作不是瞬时的，并且我们具有非空时间间隔，在该时间间隔内水平保持在L1以上。1999年，《中国日报》（ 填充）。 如果现在（填充），推断出水平正在增加，使用假设填充提高水平。现在的情况下（填充）需要另一个案例的讨论，无论填充是否在当前时间保持。如果没有，我们只需要将公理填充定义（见第2节）和假设增量定义结合起来，就可以得到想要的结果。如果填充在当前时间成立，则我们引入假设水平单调性并讨论三种情况，无论NowOn（水平L1）。特别地，如果与公理填充def相结合，则情况NowOn（水平 L l中。最后，为了正确地得出Alw（M）Alw（L 1水平Lu），我们还必须解除这两个组合模的所有假设公式。更准确地说，水库类的假设是由控制器类的定理排出的;相反，控制器类的假设是由水库类的定理排出的（更多细节见[3]图2显示了在证明全局正确性属性（实线）和在解除假设（虚线）中的证明依赖性。C.A. Furia，M.Rossi/Electronic Notes in Theoretical Computer Science 116（2005）185197水库系统水库公理level_behavior 1level_behavior_3level_behavior_4init控制器公理充填行为假设TCC满时不加注定理level_behavior_6level_behavior_7level_behavior_8res_controller_auxres_tager_aux_2填充定义假设level_monotonicityfilling_raises_levelTCC增量定义定理副储集层控制器行为储层动态假设TCCs定理水平停留在边界之间图二.证明水库系统6结论本文提出了一个组合的，工具支持的TRIO规范语言的框架该框架是基于一个推理规则，可以用来证明组件之间的相互作用，一个复杂的系统，在组件集成到系统中之后，保证了全局应用的某些属性。组合推理规则已被编码到PVS定理证明器的逻辑中，并开发了一组支持策略。基于PVS的工具已被用于将我们的组合框架应用于控制系统的示例，如第5节所示。今后在这方面的研究工作将遵循三个主要方向。首先，这里提出的组成框架的效率将在现实生活中的工业案例研究进行评估。第二，通过改进现有的PVS策略和创建新的PVS策略来改进和扩展对框架的自动化支持。第三，替代的，“较弱”的推理规则将被调查。确认作者要感谢Dino Mandrioli和Angelo Morzenti在这项工作的发展过程中提供的帮助和支持，以及Marco Lovera的有用建议和意见。我们也感谢审稿人的评论。198C.A. Furia，M.Rossi/Electronic Notes in Theoretical Computer Science 116（2005）185引用[1] Abadi，M.和L. Lamport，Conjoining specifications，ACM Transactions on ProgrammingLanguages and Systems17（1995），pp.507-535.[2] de Roever，W.- P.，The need for compositional proof systems：a survey，Lecture Notes inComputer Science1536（1998），pp. 1-22[3] 富里亚，C.一、组成证明为实时模块化系统，Laurea学位论文，Politecnico di Milano（2003），在线www.elet.polimi.it/upload/rossi/Furia_LDThesis.pdf。[4] Gargantini，A.和A.Morzenti，关键系统的自动演绎需求分析，ACM TOSEM10（2001），pp.255-307[5] Ghezzi 角 ， D. Mandrioli 和 A.Morzenti ， TRIO ： A Logic Language for ExecutableSpecifications of Real-Time Systems，JSS12（1990）.107-123[6] Morzenti，A. P. San Pietro，时间关键系统的面向对象逻辑规范，ACM TOSEM3（1994），pp.56比98[7] Owre，S.，J. M. Rushby和N. Shankar，PVS：A Prototype Verification System，in：D.Kapur，editor，Proceedings of CADE-11，LNCS607（1992），pp.748-752