理论计算机科学电子笔记185（2007）77-91www.elsevier.com/locate/entcsGTO工具集和方法Lars-Henrik Eriksson Lars-HenrikEriksson1，2乌普萨拉大学337号信箱SE-751 05 UPPSALA，瑞典摘要一个合适的方法支持的工具集具有高度的自动化是必要的正式方法在工业项目中的自20世纪90年代中期以来，GTO工具集和方法已经开发并成功应用于与铁路信号相关的安全关键控制应用中的正式方法该工具集和方法支持整个形式化方法过程，从编写和验证形式化规范，到实现建模，再到形式化验证和验证结果分析。工具集和方法的一个目标是通过简化过程使正式方法更具竞争力，以便-根据这一目标，该工具集旨在与可配置系统一起使用，其中通用规范适用于一系列系统，并适用于使用配置数据的特定系统。该工具集执行的功能包括静态检查和规格的模拟，检查配置数据的生成、从PLC程序代码或继电器原理图生成实现模型、实现模型的仿真、通过精化证明进行形式验证以及失败精化证明的分析。精化证明由用户选择的满足性（SAT）求解器自动执行我们将概述该工具集的方法和功能，以及该工具集使用的正式符号关键词：形式化方法过程，形式化方法工具，形式化验证，通用规范，精化证明1导言和背景形式化方法越来越多地进入安全关键系统的开发和质量评估。特别是，在过去十年中，非常快速的命题满足性（SAT）求解器的发展使实际工业系统的自动验证成为可能。在过去的10年里，咨询公司Industrilogik开发并使用了一套工具和方法来正式验证控制系统-1这项工作是作者在Industrilogik L4i AB（2005年被Prover Technology AB收购）时完成的。我要感谢我以前的同事们的参与。2 电子邮件地址：lhe@it.uu.se1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.05.03078L- H. Eriksson/Electronic Notes in Theoretical Computer Science 185（2007）77纳林。早期的项目，虽然在技术上是成功的，但需要正式的方法专家进行大量的项目特定工作-它们具有实验性质，成本很高。该公司的一个明确目标是以“装配线”方式以最小的开销验证新系统-这一目标已在很大程度上实现。成功是几个因素的结果：• 采用了一个已建立的和有充分根据的理论基础• 一种简单的正式符号，在与客户和应用程序专家交流时，易于用自然语言解释。• 形式规范的发展是一般的，即用一般术语来表述，而不是参照任何特定的系统。一个例子是描述一般铁路信号原理的规范，而不是特定安装的要求。使用通用规范，规范工作可以在同一应用领域内从一个验证项目重复使用到下一个验证项目。• 允许将实现从通用描述格式自动转换为验证器使用的符号• 一种验证工具，可连接任何最先进的SAT求解器，并允许用户根据规范中使用的概念分析失败验证的结果（反例）。• 为应用领域制定方法和策略。在这里，我将给出方法、符号和工具集的概述虽然在工具中使用的大多数技术以及与工具一起使用的大多数技术在今天都是成熟的，但是当GTO已经开发出来，并在许多工业项目中取得了成功值得注意的是，2000年挪威发生的ARASTARAILWAY碰撞[ 5 ]中的显著连接系统的分析以及2000年的ALISTER联锁系统的开发。瑞典国家铁路局GTO工具的最初灵感来自爱立信（电信公司）与Prover Tech- nology AB 4在20世纪90年代初开发的实验建模工具该工具使用了一个图形化建模符号结合谓词逻辑和基于事件的方法来描述状态变化的真值维护问题，这是创新的，但计算复杂。该模型主要是由St tterkSATsolver[12]来实现的，之后通过固定所涉及的集合的大小和内容将它们拉丁化为命题逻辑。在许多方面，这个建模工具背后的目标和想法与Alloy工具背后的目标和想法类似[10]。GTO是作者在Indus- trilogik L4 i AB用Prolog完成的一个完整的重新实现，将重点从建模转移到验证。的基本思想3以法拉利GTO赛车命名。关于该工具的早期版本的一个评论是，就像汽车一样，它可以快速地带你去地方，但你必须熟练地操作它。4当时称为Logikkonsult NP AB。L- H. Eriksson/Electronic Notes in Theoretical Computer Science 185（2007）7779保留了翻译成命题逻辑的谓词逻辑符号，但丢弃了真值维护功能。状态变化的事件概念后来被一个适当的（尽管简单的）时间逻辑所取代。此外，该工具是独立于任何特定的SAT求解器，通过引入一个通用的接口。该工具已与HeerHugo [7]，Sato [14]，Z-Cha [11]，Limmat一起[2]为了进一步发展战略目标，Pr overCL-Tool。 这也是NuSMV符号模型检查器的实验接口[3]。符号模型检查器今天被广泛用于解决验证问题。然而，我们的经验是，SAT解决方案似乎比模型检查在铁路信号中遇到的问题的类更好地工作在这个领域中使用模型检查器的报告[9]以及我们所做的比较实验都支持这一印象。2概述本节概述了符号、工具和方法。它们在第3节中通过一个完整的例子来说明。2.1基本原则该方法基于对规范和实现的建模，以基于时序逻辑的符号表示。实现的状态及其与环境的接口由谓词的真值表示，谓词的真值可以随时间变化，因此系统的行为由真值分配序列描述。时间的概念是离散的和线性的。根据同步假设[1]，假设系统的状态变化比环境变化快，因此可以假设动作是瞬时的，时间步长是有限短的。由于需求规范模型确定了系统的可允许行为，而实现模型确定了系统的可能行为，因此正确的实现必须是规范的细化。精化关系是通过证明指定模型的不变公式是（即）的逻辑结果来建立的可以从）实现模型公式（以及指定模型的任何定义公式）中证明2.2符号GTO的形式表示法是LTL（线性时间逻辑）[4]的变体，使用过去时间模态.该逻辑被扩展为包括多排序谓词逻辑，即具有不同量化域和谓词的量化公式。为了使实现更简单、更有效，逻辑上有几个限制。特别是，所有的排序必须是有限的（每个排序的值显式枚举），只有一个时态运算符（前一刻运算符），并且不允许谓词逻辑的函数符号80L- H. Eriksson/Electronic Notes in Theoretical Computer Science 185（2007）77符号是。 此外，前一时刻运算符可以不嵌套。公式的语法和语义是相当标准的。&用于连词，#用于析取，~用于否定，->用于蕴涵，<->用于等价。关键字ALL、SOME和PRE分别用于泛量化、存在量化和前一刻算子也有关系运算符=和<>用于等式和不等式。由于符号使用过去时间模态，公式在特定时刻的真值仅取决于从初始时刻开始的有限个时刻。一个GTO模型文件由许多声明语句组成。有些声明说，• decompression类型（或• 常量、变量和谓词的十进制类型。• 说明表示输入或输出的谓词。• 用公式定义谓词。• 根据其真实实例定义谓词。• 十进制不变公式（或公理）。• 包括子模型（文件）。一个不变式语句采用单个公式的形式。这样的公式被当作公理每时每刻都是真实 谓词定义语句具有形式p（x1，.，xn）==公式。一个定义公式的限制在于它不能在同一时刻依赖于p。从逻辑的角度来看，它可以被理解为一个公理，说明定义的谓词之间的等价性。和它的定义公式，但它对模拟也有操作意义（见2.3.2节）。其他声明将在第3节中作非正式解释。2.3工具该工具集包括主要的形式化规范和验证工具GTO，以及辅助工具，用于将其他形式化转换为GTO符号，并检查模型的逻辑等价性。GTO的基本用户界面是面向行的。用户输入文本命令，响应同样以文本形式给出。还有一个简单的图形用户界面。本文中的所有示例都将使用面向行的用户界面。GTO工具有一个状态的概念，这是一个真值分配给预测在一个特定的时刻（称为“当前时间”）和当前时间之前的时刻。由于前一时刻算子不一定是嵌套的，因此为了确定公式的真值，GTO工具具有三个基本功能：L- H. Eriksson/Electronic Notes in Theoretical Computer Science 185（2007）77812.3.1静态分析在读取模型之后，GTO执行静态分析，包括对模型进行类型检查，并检查是否进行了正确的声明和定义GTO还发现任何定义的谓词，其中定义不依赖于任何先前的时刻或输入谓词。这些谓词的真值分配与时间的时刻无关，并且是一次性计算该工具还检查不依赖于任何先前时刻或输入谓词的不变量是否成立。2.3.2仿真模拟是一种功能，其中工具递增地构造与模型一致的状态序列模拟的特点是可能的选择过去的时间，而不是通常的未来的时间。当每个公式仅依赖于过去时刻时，该工具可以仅使用关于来自先前时刻的真值的信息来确定谓词实例在连续时刻的真值。也就是说，一个在每个仿真步骤中，更新工具的状态，使得当前时间真值分配变为过去时间真值分配，并且根据每个谓词的计算规则本质上，该工具成为同步数据流编程语言（如LUSTRE[8]）的解释器计算规则主要由谓词定义给出。已定义谓词的实例的值是根据其定义公式的值计算的。由于谓词的定义可能不依赖于谓词本身在同一时刻的值，因此在给定前一时刻的真值和当前时刻其他谓词的真值的情况下，总是可以计算它。表示来自环境的输入的谓词的计算规则是，它们从上一时刻到下一时刻保持相同的值，除非用户在模拟步骤中进行修改如果某个谓词p既没有被定义也没有被声明为输入，GTO试图通过自动构造谓词的定义来获得计算规则。这个定义是由一些涉及谓词的不变量构成的，因此它总是满足不变量。如果所有的不变量都是x1... 所有xn（p（x1，.. . ，xn）->. . ）（或类似的等价物，p在右边），GTO将选择一个任意的，并把它变成一个定义p（x1，... . ，xn）==。. . .否则，如果有影响所有x1. 所有xn（p（x1，.. . ，xn）->. . ），GTO将把它们合二为一，并将其加强为一个等价物，例如，从所有x（p（x）->q（x））和所有x（p（x）->r（x）），可以构造定义p（x）==q（x）r（x）如果这些情况都不适用，GTO将寻找p的蕴涵不变量并以类似的方式处理它们。这个过程被称为“完成”，因为它试图为谓词提供一套完整的计算规则。如果某个未定义的非输入谓词可以82L- H. Eriksson/Electronic Notes in Theoretical Computer Science 185（2007）77没有完成，那么模型就无法模拟。2.3.3证明GTO可以从当前模型中对公式F进行自动证明，即确定F是否是公理和定义集的逻辑结果。“逻辑结果”的概念证明是通过将模型和F转换为命题逻辑来完成的。由于量化是在有限集合上进行的，这样的转换总是可能的。在前一时刻对谓词的引用被认为是对不同谓词的引用对嵌套前一时刻运算符的限制确保每个谓词最多有一个这样由于与特定时刻没有联系，因此效应是对所有时刻的隐含普适量化。涉及转换公式的结果证明问题被发送到单独的SAT求解器。如果证明失败，SAT求解器产生一个反例，该反例被读回GTO并用于设置其状态。然后，用户可以检查此状态以找出证明失败的原因然而，GTO解决的证明问题并不完全对应于上面定义的逻辑结果的概念。SAT求解器检查一个任意但奇异的时刻。不能保证存在一条从时间的初始时刻开始的、公理在每一时刻都成立的实际路径。换句话说，一个证明可能失败，因为F在一个公理都为真的状态下为假，但这个状态不在任何公理在前一刻都为真的路径上其结果是，证明方法是健全的，但不完整。为了获得完整的证明方法，GTO的用户必须采用一种基本上是数学归纳法的技术，使用单独的基本情况和归纳步骤证明。在基本情况下，F被证明假设公式I，它表征系统的初始状态（S）。在归纳步骤的情况下，F被证明，假设它在前一时刻成立。通过这种方式，无法到达的状态将从分析中排除。就像普通的数学归纳法一样，在步骤的情况下，可能会发生要证明的公式不足以作为归纳假设在这种情况下，一个更强的公式必须通过归纳法证明，而从归纳法得出的要求公式必须通过单独的证明来证明。2.4方法该方法的步骤和信息流程如图1所示。下文第3节说明了这些步骤。规格化模型是从非正式需求或从其他正式符号转换该方法的一个重要组成部分是开发-L- H. Eriksson/Electronic Notes in Theoretical Computer Science 185（2007）7783配置信息需求文档执行配置数据误差特性规格型号对应公理实现模型偏离描述（分析结果）反例搞定了！Fig. 1. GTO方法一个应用领域的正式理论，以促进开发和使用通用规范模型。对此的描述超出了本文的范围作为规范模型验证的一部分，可以通过GTO工具通过模拟或通过证明其具有某些所需的正确性特性来分析。如果规范被写为通用规范，则必须添加配置数据特别是，量化只能在有限的对象集合上进行，所以这些集合必须被定义。通常，分析是针对几种不同的配置进行的。在一般情况下，对规范的分析必须通过不同的工具来完成，这些工具可以处理未确定的集合，例如Isabelle或PVS5。实现模型是通过某种翻译过程从对实现的描述中获得的GTO工具集包括两个辅助工具，用于自动执行两种常见情况下的翻译，即用STEP 5语言编写的PLC（可编程逻辑控制器）程序或继电器电路原理图。作为GTO的主要应用，继电器电路转换器是GTO的重要5验证系统PVS已被用于证明GTO规范模型的一般正确性。（自动）翻译模拟/正确性证明属性形式化验证84L- H. Eriksson/Electronic Notes in Theoretical Computer Science 185（2007）77到目前为止，工具集是铁路信号。在这个领域中，中继实现仍然很常见翻译器将继电器电路中的连接的文本描述作为输入。 它使用图形重写技术，通过重写表示继电器电路的图形来完成各个翻译步骤。通过改变重写规则，翻译器可以适应可能需要不同翻译策略的不同类型的电路原理。也有一些有前途的尝试，自动解释CAD（计算机辅助设计）图纸的继电器电路，消除了非常繁琐和容易出错的手动步骤，创建一个文本描述。由于规范是通用的，系统环境状态的表示通常在规范和实现模型之间是不同的在验证实现模型之前，必须使用对应公理将不同的表示关联起来。有了规范和实现模型、配置数据和对应公理，就可以尝试进行形式验证。通常情况下，证明失败是因为实现不完全遵循规范。除了在实现（或建模！）中的真正错误之外，原因可能是规范实际上对行为的限制超过了必要的程度。当正式验证与实现的开发分开进行时，这并不罕见。当需求证明失败时，该工具将自动创建一个“反例”状态，表示系统表现出这个反例本身用处有限，部分是因为它的细节太过详细，但也因为它没有解释错误行为的原因。反例中描述的大多数信息与违反的特定要求一致。例如，反例将包括与失败函数无关的实现部分的状态信息。该方法的一个重要步骤是分析一个反例状态，以提供一个表征的情况下，系统表现出错误的行为。这种分析目前是手工进行的，需要对验证系统如何工作有实质性的了解。该分析的结果用作验证过程的输出，以描述验证系统的特定问题。该特征也用于发现违反相同（或其他）要求的其他情况。定理证明的尝试是重复的假设，最近的特点错误的情况下不能发生。这将导致定理证明器忽略特定的情况，它要么报告证明成功（在这种情况下，所有错误都被发现），要么它将生成一个反例，用于不同的错误情况，反过来可以进行分析。通过连续分析反例并以这种方式重新尝试证明，系统违反要求的所有方式最终都会被发现。L- H. Eriksson/Electronic Notes in Theoretical Computer Science 185（2007）77852.5可靠性问题形式验证的结果通常用作实现正确性的证据，例如在安全关键系统的安全情况下。这就提出了证据本身的有效性问题。我们如何依靠形式验证来产生正确的结果？在GTO的情况下，这个问题已经在必要时通过多样性和工具本身的正式验证的结合来解决GTO工具的核心功能已经使用Prolog程序的LPTP [13]验证系统进行了正式验证多样性是通过独立制作两种实施模型来引入的-重复任何手动步骤，例如继电器电路图的手动编码，在某些情况下甚至复制翻译工具-并比较结果。此外，由于GTO不绑定到任何特定的SAT求解器，因此可以使用两个不同的SAT求解器重复分析3例如3.1应用我们将通过一个简单的例子来说明这个方法该应用是用于起重机电机的控制单元。控制单元有三个输入，向上按钮，向下按钮和停止按钮，连接到按钮。它有两个输出，moveup和movedown控制电机。当按下“向上”或“向下”按钮时，应激活相应的输出。输出将继续激活，直到按下“停止”按钮。控制单元的设计必须确保两个输出不能同时激活，否则会损坏电机。3.2实现模型假设控制单元根据以下伪代码程序实现boolupbutton，downbutton，stopbutton，moveup，movedownmoveup←movedown←false重复输入upbutton，downbutton，stopbuttonifdownbuttonthenmovedown←trueifmoveupthenmovedown←falseifupbuttonthenmoveup←trueifmovedownthenmoveup← falseifstopbutton thenmoveup<$movedown<$ false输出moveup，movedown末端重复上面实现的GTO模型示例如下PRED向上按钮、向下按钮、停止按钮、向上移动、向下移动、开始;86L- H. Eriksson/Electronic Notes in Theoretical Computer Science 185（2007）77输入向上按钮、向下按钮、停止按钮;输出向上移动、向下移动;movedown ==（downbutton# PRE movedown）~stopbutton PRE ~moveup; moveup==（upbutton# PRE moveup）~stopbutton ~movedown;start== ~movedown~moveup;模型的第一行声明了使用的谓词。这些谓词缺少参数，即它们是命题变量。接下来的两行声明用于表示输入和输出的谓词。谓词moveup和movedown由表示执行伪代码程序start谓词用于在循环的第一次迭代之前，在moveup和movedown都被设置为false之后，恢复系统该模型可以通过GTO来模拟以研究其行为。>符号后面的文本输入到GTO，其他文本从GTO输出> init> 做向上按钮移动> do ~upbutton> 执行按钮> do ~downbutton> 执行停止按钮~moveup> do ~stopbutton> do downbuttonmovedown模拟由init命令初始化，该命令将所有谓词的初始真值设置为false。然后根据定义计算新的真值。使用do命令，用户要求在输入谓词upbutton设置为true的情况下发生一个时间步。这会导致输出谓词moveup为true。然后，用户在下一步中将moveup重置为false（用户模拟向下按钮的按下和释放。这没有任何影响，因为向上输出已经激活。按下停止按钮会导致moveup变为false。现在按下向下按钮将使movedown为true。3.3质量标准我们将对控制单元的两个安全属性进行正式说明为了说明通用规范，我们将使需求规范更加通用。该规范将表示控制单元的安全属性L- H. Eriksson/Electronic Notes in Theoretical Computer Science 185（2007）7787它可以处理任意数量的函数，而不仅仅是此外，可以定制规格，以排除任何特定的输出对同时有效，而其他输出是独立的。TYPES函数;VARf，f1：函数;PREDrequest（function），activate（function），cancel，cancelrequest（function），exclude（function，function），initial;输入请求，取消;输出激活;ALLf（activate（f）-> ALLf1（exclude（f，f1）-> ~activate（f1））; cancelrequest（f） ==cancel# PREcancelrequest（f）~request（f）; ALLf（activate（f）->~cancelrequest（f））;ALLf ALLf1（exclude（f，f1）-> exclude（f1，f））;initial== ALLfcancelrequest（f）~cancel& return（i）;指定从类型函数的声明开始，表示指定系统控制的一组不同接下来，变量f和f1被声明为覆盖类型函数的对象。 在下面的行中，声明了各种谓词及其参数类型，例如。 request是一个带有一个function类型参数的谓词。第一个不变量指出，如果一个函数被激活，那么任何其他被排除在活动之外的函数实际上必须被停用。cancelrequest被定义为从cancel输入为true直到它变为false的时间对于每个函数为true，并且相应的请求输入变为真的第二个不变量声明在cancelrequest为true的时间间隔内，输出不能被激活。 第三个不变量是排除谓词的一致性检查，说明它必须是对称关系。注意，排除谓词没有定义，类型函数的常量也没有给出。当规范与特定实现一起使用时，此信息作为配置数据提供例如，在这种情况下：CONSTup，down：function;事实exclude（up，down），exclude（down，up）;通过声明常量符号up和down属于类型函数，并定义谓词excludes在所述实例中为真，该规范可用于起重机电机应用程序当将规范加载到GTO中时，将根据上述第三个不变量检查排除谓词的对称性，如果存在差异，则报告。我们现在通过模拟来分析特定模型。示例规范是不确定的，因为它仅描述了可以以不同方式满足的安全属性没有要求输出何时应该是活动的，只有当它们不应该是。在这种情况下，GTO可以88L- H. Eriksson/Electronic Notes in Theoretical Computer Science 185（2007）77构造激活的定义，使模型确定。构造的定义是activate（f）== 所有 F1（exclude（f，f1）-> ~activate（f1））&return（f）;这个定义的情况下，输出将被激活时，它是我们希望在一个特定的初始状态下开始模拟，在这个初始状态下，我们假设没有请求输入是活动的，但是取消输入是活动的。这种状态的特征在于初始谓词。> 满足初始公式是可满足的。> 请求（up）激活（up）> do ~request（up）> 请求（down）> do ~request（down）> 取消~activate（up）> 做~取消> do request（down）activate（down）交互开始于用户请求GTO找到一个初始为真的状态，即规范处于初始状态。SAT求解器被要求找到这样的状态。然后，交互沿着与实现模型的模拟相同的路线进行。请注意，activate谓词的完整定义使GTO在规范允许时自动激活相应的输出。3.4正式核查在验证之前，必须创建一个复合模型，包括实现和规范以及对应公理：USE实现; REFINES规范;所有f（request（f）<-> f=up up_button # f=downdown_button）;所有f（activate（f）<-> f=up moveup # f=downmovedown）;取消-> stop_button;假设实现和规范分别是包含实现和规范模型的文件的名称，前两行说明这个复合模型包括实现和规范，目的是细化规范模型。这有一个重要的效果，将规范文件中的不变量作为公理，因为它们是需要证明的公式。L- H. Eriksson/Electronic Notes in Theoretical Computer Science 185（2007）7789在加载复合模型之后，可以进行需求公式的证明。这些公式由它们出现的文件名和序列号标识。下面的交互表明，规范的第一个需求公式通过实现得到了满足。> 证明规范_1公式有效第二个要求公式不能直接证明。只有当系统在需求已经成立的状态下初始化时才是真的相反，它必须通过第2.3.3节中描述的归纳证明方法来证明。由于系统在谓词start为真时处于其初始状态，因此归纳证明可以如下进行：> prove start ->specification_2公式有效> 证明PRE规格_2->规格_2公式有效现 在 ， 假 设 在 实 现 中 犯 了 一 个 错 误 ， 例 如 ， 伪 代 码 语 句ifmovedownthenmoveup←false被省略了。在这种情况下，moveup的定义将成为上移==（向上按钮#PRE moveup）~stopbutton;证明的尝试就会失败> 证明规范_1这个公式是可证伪的。> 为什么公式是无意义的，因为f=up，activate（up）=>. f1=down，exclude（up，down）=>. 激活（向下）> evf向下移动按钮TRUE由于该公式不能被证明，GTO创建了一个状态，其中它是假的。 使用why命令，用户要求GTO尝试解释为什么不能证明需求。 该工具为量化公式为假的量化变量提供实例（见证），并显示量化公式的相应实例。在这种情况下，只有两个类型函数的对象，很明显，它们中的每一个都必须涉及，但在更复杂的情况下，解释函数可能会有很大的帮助。用户还可以直接检查状态，例如通过使用evf命令来评估其中的公式。在检查状态和实现之后，用户识别错误--如果起重机电机已经向下移动，则按下向上按钮将激活向上输出。错误情况可以通过公式向下移动按钮来描述。为了找到实现中可能存在的其他问题，通过假设其否定来排除错误情况，重复90L- H. Eriksson/Electronic Notes in Theoretical Computer Science 185（2007）77产品说明：> prove ~（movedown& upbutton）->specification_1公式有效。证明成功了，所以这是关于这个要求的唯一错误4结论和今后的工作我们已经概述了GTO工具集的功能以及如何将其用于正式规范和验证工作。自动化过程中耗时部分的目标在很大程度上已经实现。主要任务仍然是手动的反例分析失败的证明尝试。尽管这一过程不太可能完全自动化，但该工具可以为用户提供实质性支持，帮助他们找到需求失败的原因，并描述发生这种情况的特征。引用[1] Benveniste，A.和Berry，G.，反应和实时系统的同步方法，IEEE会议录，第79卷，第9期，pp. 1270[2] Biere，A.，Limmat，http://fmv.jku.at/limmat。[3] Cimatti，A.，Clarke，E. M.，Giunchiglia，F.，和Roveri，M.，NuSMV：一种新的符号模型检查器，International Journal on Software Tools for Technology Transfer，Vol. 2 No. 4，pp 410[4] 克拉克法医格伦贝格岛和Peled，D.A.Model Checking，MIT Press（1999）.[5] Eriksson，L-H.在回顾性安全案例中使用形式化方法， Liggesmeyer，P.，Wittmann，S.（编辑）：计算机安全性、可靠性和安全性-[6] Eriksson，L-H.领域理论在应用形式化方法中的应用，技术报告2006-029，乌普萨拉大学，系。信息技术（2006）。[7] Groote，J.F.和Warners，J.P.，陈文龙，数学与计算机科学，清华大学出版社，1999年.[8] Halbwachs，N.，Caspi，P.，Raymond，P.和Pilaud，D.，同步数据流编程语言LUSTRE，IEEE会议录，卷。79不。第9页。1305[9] Huber ， M. 和 King ， S. ， Towards an Integrated Model Towards for Railway Signalling Data ， 载 于Eriksson，L-H。和林赛，P.A.（编辑）：FME'2002：正式方法-正确使用，pp。204-[10] Jackson ， D. ， Alloy ： A Lightweight Object Modeling Notation ， ACM Transactions on SoftwareEngineering and Methodology，Vol.11没有。第2页。256[11]Moskewicz，M.，Madigan，C.，赵玉，张丽和马利克，S.，Cha Cha：Engineering an Eccient SATSolver，Proceedings of the 38th ACM/IEEE Design Automation Conference（DAC'01），pp. 530[12] Sheeran，M. 和S. ，ATutoRialonStalmarcks P r o f P r o cedu r e for P r o p os i t i o n a l L og i c，InGopalakrishnan，G.和Windley，P.（编辑）：Proc. 2nd Intl.计算机辅助设计中的形式化方法会议，FMCAD82 - 99[13] 斯特尔克河F. ，LPTP的理论基础（一种逻辑程 序 设计 理 论 ） ， 逻辑程序设计杂志，卷。36页。241-269（1998）。L- H. Eriksson/Electronic Notes in Theoretical Computer Science 185（2007）7791[14] 张 洪 ， 佐 藤 ： 一 个 有 效 的 命 题 证 明 ， 在 McCune （ 编 辑 ） ： Proc. 14th International Conference onAutomated Deduction（CADE-14），Lecture Notes in Computer Science，Springer Verlag（1997）
我的内容管理
展开
