地铁控制软件开发中的自动验证阶段及其在质量提高上的应用

理论计算机科学电子笔记130（2005）323-343www.elsevier.com/locate/entcs地铁控制软件NelsonGuimarapouchesFerreiraandPauloS′ergioMunizSilva1，2DepartamentodeEngenhariadeComputacampaignoeSistemasDigitaisEcolaPolit′ecnicadaUniversidadeSapaulo loAv. Prof. LucianoGualberto，trav. 3，n. 15805508-900SaoPauloSPBrazil摘要本文提出在地铁控制软件开发过程中引入自动验证阶段，在该阶段中，有界模型检查（BMC）和归纳证明将用于预测错误发现并提高最终产品的质量。我们报告的测试，我们开发的一些安全规则的两个实际部分的地铁轨道和结果我们实现了。我们的结论是，该技术似乎是可行的问题域，但这个问题需要广泛的研究，让一个准确的理解使用BMC满足哪些要求，以及这种方法可能会给项目带来的实际好处。关键词：有界模型检验，安全需求模型检验，地铁控制软件模型检验。1介绍在过去的几年里，计算机控制系统有了很大的发展，因为软件错误可能会出现问题。当我们考虑到要控制的系统变得越来越复杂，而交付时间与以前一样，如果不是更短的话，这个问题就更加严重了虽然软件正确性对于非安全相关系统可能是非常重要的问题，但对于控制可能使人的生命以及昂贵的设备和安装处于危险中的设备的系统来说，这是至关重要的。1电子邮件：nelson. poli.usp.br2 电子邮件：paulo. poli.usp.br1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.03.017324N.G. Ferreira，P.S.Muniz Silva/Electron.注意Theor。Comput. Sci. 130（2005）323本文介绍了一种评估模型检查的可行性的软件控制的一个实际的地铁系统的一部分。地铁轨道可能足够大，以至于有必要将其划分为许多部分，并为每个部分分配一个运行其特定（安全相关）软件的控制器。一个区段通常包含少量的站，这意味着控制它的软件可能相对复杂。为了降低交付有错误的实现的风险，开发控制器的公司定义了一个验证和确认（V V）过程，并在定义明确的阶段进行检查和测试活动。我们认为，有一些坚实的理由为这种发展实施首先，众所周知的事实是，随着项目的进展，修复软件错误变得越来越昂贵。在软件准备好发布到检查阶段之后立即使用模型检查可以预期错误发现，从而产生节省。其次，它还有助于提高最终产品的质量，因为自动验证可能会发现否则无法发现的细微错误。第三，与开发过程中的其他活动相比，此处所述的验证活动可能减少了工时。最后，为第一个软件版本所做的大部分工作可能会在下一个版本的开发过程中重复使用。对铁路控制软件的自动验证进行了研究。一般来说，由于受控铁路及其相关软件可以容易地和自动地简化为有限状态机（FSM）， 模型检测和其他利用这种形式主义的技术被用来解决这个问题是很自然的。[8][7][6][9][11]和[12]。我们的方法接近[8]、[7]和[6]。所有作品之间的第一个共同点是问题域：用彼此接近的语言编写的铁路控制软件[8]描述了对相对简单的Dutch站的所使用 的工具是 St代数Marck 定理证明器。第二项工作使用基于二元决策图（BDD）的模型检查器来验证[8]验证的同一个站以及更复杂的一个。这两项工作都与我们有关，因为尽管他们使用的技术与我们不同，但他们打算使用详尽的状态空间探索来验证铁路控制软件的安全规则。另一个共同点是，他们使用的技术允许验证可能表现出非常普遍模式的规则。[6]使用有界模型检查（BMC）来验证一些安全不变量，并建议在开发的实现阶段结束时使用它N.G. Ferreira，P.S.Muniz Silva/Electron.注意Theor。Comput. Sci. 130（2005）323325过程。它还涉及实施核查阶段，对流程的影响较小，不需要人员培训。虽然我们打算验证比[6]更一般的模式，但我们的工作接近于它，主要有两个原因。首先，尽管有一些不同的观点，但这两部作品都关注开发过程和自动验证阶段造成的影响。其次，我们使用相同的技术（基于SAT的有界模型检查）。因此，我们认为，通过讨论在开发过程中使用验证阶段，我们对[8]和[7]做出了贡献，通过提出一种更通用的验证安全规则的方法，以及通过提出一些执行与自动验证阶段相关的活动的不同方法，我们对[6]做出了作为进一步的贡献，本文打算提请注意软件结构在待验证规范格式中的重要性。本文其余部分的结构如下：第2节描述了要验证的系统，并讨论了我们的建议，包括自动验证活动的好处第3节介绍了与BMC相关的形式主义第4节描述了我们开发的实验，并显示了他们的结果。第5节讨论了一些问题，并将我们的结果和建议与其他人进行了比较。最后，第6节总结了本文，并提出了一些未来的步骤。2系统描述待验证的软件实现了轨道区段的控制，图1中部分表示了该轨道区段。 该图显示了标记为1和2的两个轨道，可以通过标记为X99-1和X99-2的两个点合并。轨道被分成大约40个轨道段，称为轨道电路，每个轨道段被标记为1Lnn或2Lnn，这取决于它们所处的轨道。图1只显示了10个可用的轨道电路。除1L06和2L06外，每个轨道电路由两个发射机划界。每一个发送器都能够向占用由它限定的轨道电路之一的列车发送速度代码。速度代码通知列车它被允许在该轨道电路上移动的最大速度，并且通过在整个轨道上输出调制电流来发送速度代码 速度代码对应于10、35、50、60和68 km/h。不是所有的发射机都能发射所有的代码。通过构造，由一个发射器发射的信号不可能到达不受其限制的轨道电路。在轨道上运行的每辆列车都配备了前置天线。的326N.G. Ferreira，P.S.Muniz Silva/Electron.注意Theor。Comput. Sci. 130（2005）323信号变送器绝缘体1L081L07X99-B1L06X99-A1L05 1L04X99-2 X99-12L062L07X99-C2L06Fig. 1. 待验证2L05 2L04 X99-D天线捕获位于列车前方的发射机发送的电流，但无法接收位于列车后方的发射机发送的信号。这是因为火车轴使轨道短路，因此从火车后面传输的电流无法到达天线。列车还配备了一个内部的重要控制器，确保它永远不会以高于速度代码对应的速度运行，除非从较高的速度代码转换到较低的速度代码。在这些情况下，火车被迫遵循速度分布，以便在它移动固定的最大距离之前达到较低的速度每个轨道电路还能够检测是否有列车占用它。图1中未显示与此功能相关的硬件。轨道电路1L06和2L06由电绝缘体限定。其上的速度代码由安装在每个轨道电路末端的发射机发送，就像在任何其他轨道电路中一样。这里的不同之处在于，负责这些轨道电路中的每一个的速度代码的发射机是互连的，因此在实践中，无论列车运动的方向如何，所有发射机都图1还显示了1L06和2L06之间的两个点，这两个点负责使列车从轨道1移动到轨道2，反之亦然。每个点都可以处于正常（列车不移轨）或反向（列车移轨）位置。该设备具有数字输出，因此控制器能够检测它们的位置。还有从控制器到每个点的输出。输出旨在锁定该点，使其不会意外移动。最后，图1显示了标记为X99-A/D的四个信号。每一个信号都可以关闭或打开，在前一种情况下，列车必须停车。当它处于开启状态时，信号是绿色的，允许列车行驶（前提是速度代码也允许它这样做N.G. Ferreira，P.S.Muniz Silva/Electron.注意Theor。Comput. Sci. 130（2005）3233272.1控制软件控制软件在三模冗余（TMR）设备上运行，为每个受控设备或轨道电路实现所有必要的数字输入和输出。每个输入或输出都由自己的变量表示。该软件是作为一个列表的约480个任务，涉及数字输入，数字输出和内部状态布尔变量。大约有300个数字输入。 所有的赋值都是以Vi= f（v0，v1，...，vn），其中Vi是状态或输出变量，并且v0，v1，.，vn是三种类型中的任何一种的变量。函数f只接受三个二元运算符，即NOT（由“.”表示），AND（“*”）和OR（“+”）。在每个赋值的右边可能有几十个操作数。可以使用括号来更改默认的操作符优先级。不允许为某个输出或状态变量定义多个赋值。作为一个实现规则，变量的名称有一个前缀，表示与之相关的设备或轨道电路，以及一个后缀，表示其含义。控制铁路的设备具有负责管理设备必须执行的内部任务的执行软件。执行循环读取所有输入并将其值分配给相应的变量，允许执行分配列表，并最终将计算输出的值发送到与物理设备接口的硬件。数字输入、数字输出和状态变量之间的唯一区别是前者是其值仅由执行软件分配的变量。相反，其他变量在赋值列表的每个执行周期中总是作为一个新值它们的值在两个连续周期之间保持不变。从分配列表的角度来看，数字输出和状态变量之间没有区别。在本文中，我们感兴趣的是执行的分配列表。任何两个连续周期之间的时间间隔不一定是固定的。通常小于100 ms。表1显示了本文中我们感兴趣的变量的所有命名约定。在该表中，tc、tc1和tc2表示轨道电路名称，sc表示相应速度代码的速度，p表示点名称，而sgn表示信号名称。2.2拟议的发展进程当前的开发过程如图2所示。它首先发布了一个规范，该规范以自然语言说明了安全规则，并给出了通常如何实现分配的示例。的328N.G. Ferreira，P.S.Muniz Silva/Electron.注意Theor。Comput. Sci. 130（2005）323表1安全性验证的关注变量可变基团投入产出意义pNWCK我指示该点处于正常（1）或不处于正常（0）位置。示例：X99- 1 NWCK。pRWCK我指示该点处于反向（1）或不处于反向（0）位置。示例：X99- 1 RWCK。tcTP我指示轨道电路是占用（0）还是未占用（1）。示例：1L05TP。pLSO锁定（0）或解锁（1）点p.示例：X99- 1 LS。sgn-GO打开信号（1）或关闭信号（0）。示例：X99-AG。TC1-TC2-SCO强制在位于tc1和tc2之间的变送 器 中 传 输 相 应 的 速 度 代码。示例：1 L05 - 1 L04 - 35软件实现基于规范和图纸 每一节。图纸传达了有关轨道电路、点和信号的轨道组织信息，以及有关轨道速度的信息。在实施阶段之后，独立的专家工程师检查软件。最后一个阶段是平台测试，由与实现阶段没有直接关系的人员执行。图2显示了项目的自然流程，以及在后期阶段发现错误时的反馈。虽然非常可靠的实现可以（并且已经）通过该过程交付，但我们认为该项目可以从引入自动验证阶段中受益。我们认为可能实现的效益为：• 早期发现错误。众所周知，越早发现错误，其对项目进度和成本的影响就越小N.G. Ferreira，P.S.Muniz Silva/Electron.注意Theor。Comput. Sci. 130（2005）323329质量标准实施检查质量标准实施检查测试测试图二.目前的发展进程在实现阶段完成后立即插入自动验证活动，可以在代码被发送到昂贵的检查和测试阶段之前发现错误[9]引用了一些研究，这些研究得出结论，随着项目变得越来越复杂，错误发现从检查转移到测试虽然我们没有所研究项目的等效数据，但我们认为情况也是如此，因为有理由相信，人类核查员可以有效地实现小范围的核查，但他/她几乎无法在大范围内做到这• 提高整体素质。 该实现可能有一些非常微妙的错误，无法通过测试或预防来发现，但可以通过详尽的自动分析来检测• 在第一个版本中完成的大部分工作可以在子版本中重用。通常情况下，第二个或更高版本不会显著改变安全规则或软件的内部结构。在这种情况下，大多数（如果不是全部）用于验证第一个版本的模型可以重复使用。我们建议改变当前的开发过程，如图3所示。我们在实现阶段之后立即加入了一个自动验证阶段，使用模型检查作为验证技术。这样做的原因是因为模型检查很适合这个问题，正如我们将在第4节中看到的那样。另一个原因是现在很容易获得好的模型检查器。我们不能保证自动验证阶段会发现所有的实现错误。我们的目标是预测他们的发现。3系统验证在本节中，我们将介绍形式验证过程中使用的时态逻辑。我们还简要介绍了模型检查，并解释了330N.G. Ferreira，P.S.Muniz Silva/Electron.注意Theor。Comput. Sci. 130（2005）323自动产品规格执行情况Verification测试检查检查测试图三. 拟议的发展进程技术，我们打算用它来验证所研究的系统的属性。3.1LTL时态逻辑线性时态逻辑（LTL）公式使用原子命题，布尔运算符和时态运算符来定义所研究系统必须保持的属性。虽然可以定义许多LTL运算符，但最常用的是：Ff（公式f最终将有效），Gf（公式f全局有效，这意味着它现在有效，并且在任何未来状态下都有效），f1Uf2（f1有效，直到f2最终变得有效），f1Wf2（f1有效，直到f2变得有效）和Xf（f将在下一个状态有效在数学上，给定原子命题集合AP的LTL公式的语法根据以下规则定义[5]：• 一个原子命题p∈AP是一个LTL公式.• 如果f1和f2是LTL公式，则<$f1和f1<$f2是LTL公式。• 如果f1和f2是LTL公式，则Ff1，Gf1，f1Uf2，f1Wf2和Xf1是LTL公式。LTL的语义基于有限状态机（FSM）路径的概念。路径是状态π =（s0，s1，. . 其中s0是路径的第一个状态，不一定是FSM的初始状态。首先，我们需要为FSMM定义以下符号：• πi是以si为第一态的π• M，π| = f意味着f在s 0处成立。现在我们可以根据以下规则定义LTL公式的语义• M，π| = f i f在状态s 0上为真。• M，π |=<$f i <$f在s0处不成立。• M，π| = f1<$f2i <$（M，π| = f1）和（M，π| = f 2）。• M，π| = Xf i M，π1| = f。N.G. Ferreira，P.S.Muniz Silva/Electron.注意Theor。Comput. Sci. 130（2005）3233311 21• M，π|= fUf2i存在k≥ 0使得M，πk| = f和M，πi| = f，对于任意0≤i< k。作为缩写，我们可以写M|当路径的第一个状态是模型的初始状态之一时，它是隐含的。显然，其他常见的布尔运算符，如，→和←→可以从<$和定义。运算符F、G和W可以分别定义为Ff（trueUf）、Gf<$F <$f和f1Wf2（f1Uf2）<$Gf1。3.2模型检测模型检查是一组技术，用于通过详尽分析所有状态和转换来验证建模为FSM的系统的某些时序逻辑规范。我们通常有一个原子命题的集合AP，一个FSMM=（S，S0，R，L）和一个在某些时态逻辑中陈述的规范f其中S是有限状态集，S0<$S是初始状态集，R<$S×S是总转换关系（即，任何状态都至少有一个后继），并且L：S→2AP是一个函数，它用在该状态中为真的原子命题来标记每个状态[5]。模型检查器尝试验证M是否|= f，对于从模型的初始状态开始的所有路径，如果不是，它通常发布可用于调试系统的反例使用模型检查时最常见的挑战是处理由系统变量的所有可能值的组合所产生的状态爆炸问题。有时，为了能够用简化的模型来验证给定的规范，有必要抽象一些系统行为。这种方法有一些缺点，即它可能需要在过程中进行人工干预，并在验证中导致一些错误。如果可能的话，我们希望在尝试验证我们感兴趣的控制软件时避免任何类型的抽象。有许多模型检测技术，旨在用于不同类型的应用程序。它们可以分为两个主要的组：一组技术使用显式表示的状态的FSM和组使用符号表示。在第一组中，每个状态都被单独分析并存储到计算机主存储器中，而第二组使用描述状态集和转移关系的命题公式显式表示方法通常用于当系统可以由有限状态机建模时，其大小仅限于几百万个状态。这个限制通常是由现在使用的计算机上可用的主内存量给出的。由于我们处理的系统的状态数远远大于这个极限，显式表示技术将不是我们的第一选择。332N.G. Ferreira，P.S.Muniz Silva/Electron.注意Theor。Comput. Sci. 130（2005）323通常，符号模型检查器使用一种技术，通过这种技术，它们表示符合某些命题公式的状态集，而不是处理单个状态。最常用的方法之一是基于定点计算。在其基本形式中，基于这种技术的模型检查器从一个表示模型的所有状态或不表示状态的集合开始，这取决于分析的规范类型。该集合通过应用转移关系迭代地更新，直到最终到达定点。然后，模型检查器验证是否所有初始状态都属于该定点。如果是这种情况，则规范成立。大多数使用这种技术的模型检查器使用BDD [3]库来创建表示状态集和转换关系的布尔这种技术适用于一些只有几百个布尔变量的模型，但当模型大于这个值时就失败了。主要原因是当模型变大时，处理状态集和转换关系需要大量的内存和CPU时间。即使基于BDD的模型检查有效，有时也需要仔细设置模型检查器框架，因为一些参数（如变量排序和用于计算定点的算法）可能对该方法的成功至关重要。如果我们不考虑使用抽象的话，中大型模型的局限性和困难性并不能使基于BDD的模型检查器成为我们想要验证BDD解决方案的局限性以及近年来随着命题公式问题的可满足性（SAT）的快速算法的发明而取得的进展为引入有界模型检查创造了条件[2]。在BMC中，转移关系和状态集仍然由命题公式表示。最初，模型检查器建立一个公式，该公式是系统的初始状态和分析中的规范的否定的结合。该公式然后由SAT求解器进行分析，该求解器试图找到使其为真的估值。如果有这样的估值，它将被用作具体化的反例。如果没有这样的估值，那么就不能说规范的真实性，模型检查器开始一个新的周期。在新的循环中，要分析的公式是：初始状态的析取、转移关系和具体化的否定。模型检查器试图找到一个反例，考虑到初始状态以及它们的后继状态。同样，公式被发送到SAT求解器。这个过程继续下去，直到找到反例，达到最大迭代次数k，或者要分析的公式变得足够大，使其分析不可行。与经典的无界模型检测相比，BMC具有一些N.G. Ferreira，P.S.Muniz Silva/Electron.注意Theor。Comput. Sci. 130（2005）323333缺点和优点。主要的缺点是，一般来说，它不能说一些关于所需规范的真实性的事情，如果它成立或者反例足够大，可以由SAT求解器处理。因此，BMC主要是一个错误发现工具。BMC比无界模型检测有很多优点。首先，用户不需要手动设置环境通常情况下，默认参数将继续使用。其次，模型检查器能够处理数千个变量，而不是数百个，这样做，它使用更少的内存，花费更少的计算机时间。第三，保证生成的反例最小，简化了问题的分析第一个和第二个特征将对我们的验证过程具有重要价值。3.3鲁棒系统与归纳证明在[7]中，一个模型被定义为相对于一个指定f是鲁棒的，如果f成立对于模型的所有可能状态，即使它们从初始状态不可达。在数学上，FSM模型M=（S，S0，R，L）是鲁棒的，关于f，如果给定M J=（S，S，R，L），M |=Jf→M| = f。关于规格f的鲁棒模型具有有趣的特征，即如果f = f（p0，p1，..，Xp0，Xp1，.，Xkp0，Xkp1，. . ）对于从初始状态s0开始的所有k+1个状态的有限序列成立，则Gf也成立。换句话说，我们可以说，|= f → M |= Gf. 事实上，任何f成立的有限状态序列都在某个最终状态sk处结束，该最终状态s k本身属于修改后的模型MJ的初始状态集合。因此，状态sk是一个新的有限序列的初始状态，f也成立，并且归纳地M |= Gf. 我们将公式的深度定义为嵌套X运算符的最大数量k例如，在所考虑的地铁系统中，只要X99-1点处于反向，我们就可以预期信号X99-A 必须变为反向这个规则可以指定为G（X99- 1 RWCK→F（<$X99-AGW <$X99- 1 RWCK））。这个句子说，如果X99-1是反向的，那么它总是正确的（G），信号X99-A将最终（F）变为0，并保持在该状态，直到（W）X99-1不被反转。这种句子格式有两个缺点。首先，我们没有关于软件响应新条件所需的周期数的信息。这是一个明智的问题，因为如果我们保持LTL规范如上所述，我们理论上接受较长的响应时间，这可能会使实施无法快速响应紧急情况，使其不安全。此外，为了使用归纳证明方案，我们需要对软件周期的数量有一个界限k，并且如上所述，该句子不携带关于以下内容的任何信息：334N.G. Ferreira，P.S.Muniz Silva/Electron.注意Theor。Comput. Sci. 130（2005）323了我们通过分析源代码来解决这个问题，以确保证明的完整性。 与其尝试使用类似上面的句子，我们开始寻找可以表述为（X99- 1 RWCK）→Xk<$X99-AG），这意味着信号X99-AG被转换为0个周期在点X99-1之后是反向的。如果对于给定的k和一般的初始条件，这个句子可以被证明为真，那么如果k被认为足够小，我们感兴趣的安全规则将被验证。事实上，可以证明，如果该点在任何状态s i处是反向的，则该信号在任何后继状态s i + k处都是反向的。这也意味着信号将保持为零，而点保持其反向状态，因为如果点在si+1处仍处于反向状态，则信号将在si+k+1处为零，依此类推。在我们的示例中，我们在快速源代码分析后得出结论，要证明的规范是（X99- 1RWCK→XX <$X99-AG），并且一个界k= 2就足以证明它。4验证和实验在本节中，我们将描述我们使用的工具，我们想要验证的安全规则，它们到LTL的转换，以及我们从两个实验中获得的结果。4.1工具我们选择使用NuSMV [4]作为有界模型检查器。这是一个扩展了符号模型验证器（SMV）[10]的重新实现，在卡内基梅隆大学3被开发。NuSMV接受描述待验证系统模型的文件作为输入。 输入语言基本上与SMV定义的语言相同（“SMV语言”）。因此，我们需要一个程序来自动将原始源代码翻译我们实现的翻译器创建了一个单一的SMV输入文件，声明了原始源代码定义的所有变量和完整的赋值集。原始源代码中的赋值与SMV输入语言中的赋值之间存在一一对应关系。翻译人员负责以下任务：• 赋值、运算符and、or和not在两种语言中用不同的符号表示，因此原始表示必须是3我们使用NuSMV 2.1.2版，在C ygwin和Windows XP下运行。 该版本实现了基于有 界 和 无 界 BDD 的 模 型 检 查 ， 可 在 www.example.com 上 免 费 获 得http://nusmv.irst.itc.it/。N.G. Ferreira，P.S.Muniz Silva/Electron.注意Theor。Comput. Sci. 130（2005）323335根据SMV语言规则转换。• SMV语言不接受以数字作为第一个字符的变量，因此翻译器总是在每个变量的开头包含下划线（）。• SMV操作符接下来附加到左侧的任何变量 一个任务。在这样做时，我们指定被分配的变量的下一个状态值将是右侧公式的结果。• 翻译器必须决定如何翻译赋值右侧的任何变量var。它可以把它翻译成前一种情况用于从第一个赋值开始翻译时，var尚未在赋值的左侧使用。后一种情况用于其他情况。最后一个任务在将原始源代码翻译成SMV语言的过程中保留原始源代码的语义。在原始源代码中，赋值是从上到下顺序执行的。SMV语言具有不同的语义，因为它认为每个赋值都是并行执行的。图4显示了从一种语言到另一种语言原创节目：A = .B * D *（C +A）;B=. A*D;SMV翻译：next（A）：=！B& D&（C|A ）;下一个（B）：=！next（A）&D;4.2遵守安全规则我们选择检查与轨道的可观察行为相关的安全规则。该软件有大量的变量，这些变量在内部使用，必须遵守其内部规则。违反这些规则不一定会使系统处于不安全状态，因为内部变量不会直接改变轨道的当前状态。为了使用模型检查技术，我们定义了四类安全规则。该规则集并没有完全描述系统的所有安全相关需求，但有助于对此类系统使用模型检测的可行性我们将规则分为四组。我们还认识到，有一些规则描述了系统必须对某些输入条件做出响应的方式，还有一些规则必须独立于输入的状态而保持，并且可以被认为是系统的命题不变量。所有的规则都可以写下来336N.G. Ferreira，P.S.Muniz Silva/Electron.注意Theor。Comput. Sci. 130（2005）323在以下规格格式中：• G（→F（W <$）），用于依赖于输入的规则。这意味着，如果输入条件发生，那么最终将达到安全状态，并且系统将保持在安全状态直到输入条件被重置。严格地说，这些规则也可以被认为是系统的不变性质，因为任何Gf性质都可以被认为是不变的。然而，在本文中，我们将保留这个词不变的命题公式，必须保持没有任何显式的依赖于输入。• G（），用于必须始终保持并且不依赖于任何输入的规则。用于对规则进行分类的四组是：1. 当与发射机相关的两个轨道电路都被占用时，发射机不发射任何类型的速度代码。例如，我们必须预期1L05和1L04之间的发射机不发射如果1L05和1L04都被占用，则任何速度代码此规则具有以下条件/安全状态对：Condition：€1L05TP€ 1L04TP安全状态： 电话：+86-10- 8888888传真：+86-10 - 888888881 L04和1 L05之间的发射器只能发射对应于35、50和68 km/h的速度代码。与其他速度相关的变量在程序中没有定义。因此，它们不属于变送器安全状态定义。类似的条件/安全状态对适用于其他变送器。2. 点与信号之间的联锁。我们设计了以下涉及信号和点的规则：2.1. 无论何时打开任何信号，这两个点都被锁定一个接通信号使列车能够通过其点。因此，出于安全原因，必须将两个道岔锁定，以避免任何可能导致列车脱轨的意外道岔移动。该规则是独立于输入的，并且可以由以下不变量表示：不变量：X99-AG→ X99-BG→ X99-CG→ X99-DG→ <$X99- 1 LS→ < $X99 -2LS2.2. 不允许有一个以上的信号，如果至少有一分数是相反的。条件/安全状态对是：Condition：X99-1RWCKX99-2RWCK安全状态： <$（（X99-AG）<$X99-CG） X99-AG和 X99-DG （X99-BG） X99-CG ∨（X99-BG和 X99-DG））2.3. 如果两点都反向，所有信号灯必须关闭的这意味着甚至不允许从C到D或反之亦然的N.G. Ferreira，P.S.Muniz Silva/Electron.注意Theor。Comput. Sci. 130（2005）323337条件/安全状态对是：Condition：X99-1RWCKX99-2RWCK安全状态：€（X99-AG<$X99-BG<$X99-CG<$X99-DG）2.4. 当点1处于反向时，信号A和C必须变为0。同样地，只要点2处于反向，信号B和D也必须变为0。两个规则的条件/安全状态对是：条件1：X99- 1 RWCK安全状态1：<$（X99-AG） X99-CG）条件2：X99- 2 RWCK安全状态2：€（X99-BG和 X99-DG）2.5. 两个点必须在正常位置时，我们有一个每一个轨道上的信号 条件/安全状态对是：条件：€（X99- 1 NWCK<$X99-2NWCK）安全状态： <$（（X99-AG）<$X99-CG） X99-AG和 X99-DG （X99-BG） X99-CG ∨（X99-BG和 X99-DG））3. 相反的信号决不能同时打开。我们定义下面列出了该规则的两个不变量不变量1：<$（X99-AG<$X99-BG）不变量2：<$（X99-CG<$X99-DG）4. 当列车接近一个超速信号时，发送的速度代码应始终对应于低速。作为一个例子，我们必须预期速度代码被传送到正在接近的火车上。信号A不能对应于50或68 km/h。下面给出了示例的条件/安全对。其他信号也有相同的规则。不变量：<$X99-AG→ <$1L05 - 1 L06 -50<$1L05 - 1 L06 -684.3创建LTL规格为了使用上面描述的归纳过程来证明规则，我们必须为这些规则创建LTL规范。在分析软件的有限数量的循环之后，规范可以被证明为真我们已经给出了一个例子，在这个例子中，我们发现软件需要两个周期才能在点X99-1反向后将信号X99-A翻转。显然，我们可以预期至少需要一个周期，因为软件在响应任何输入更改之前至少需要执行一次。然而，我们没有任何方法可以先验地知道所需的循环数而不进行分析。很可能软件需要三到四个周期才能做出响应。在实践中，分析软件是一个观察序列的问题，338N.G. Ferreira，P.S.Muniz Silva/Electron.注意Theor。Comput. Sci. 130（2005）323要验证的规则所使用的变量的赋值，以及可能检验它们的中间变量的赋值。在分析之后，编写LTL公式并进行检查。如果模型检查器显示规格不成立，可能是因为LTL规格说明不正确，或者是因为软件有一些错误。在这两种情况下，我们都必须在模型检查器反例的帮助下重新分析程序。创建LTL规格的另一种方法是假设软件是正确的，并从暂定规格开始。如果模型检查器声明规范成立，则过程结束。否则，我们可以创建一个新的试探性规范，直到我们证明规则或放弃为止。并考虑分析源代码。虽然我们可能必须在达到有效规范之前运行一些试探性规范，但我们可以节省一些时间和排序，因为与分析源代码所需的时间相比，模型检查器的响应时间很短。在上面的例子中，我们可以从暂定规格开始（X99- 1 RWCK→X <$X99-AG）。以来模型检查器会说规范不成立，我们可以尝试（X99- 1 RWCK→XX <$X99-AG）。这一规范成立，所以我们可以成功地节省时间，并避免分析代码。简而言之，我们只花了几个小时就为手头的问题编写了正确的LTL规范。表2显示了这项工作的结果。第二列显示了用于检查规则的LTL规范，第三列给出了模型检查的界限，即软件必须运行的周期数，以便进入安全状态或符合不变量。一个有趣的点是在群2.1、3和4的指定开始时使用的X算子的起源。这些组负责检查独立于输入的不变量。这意味着LTL规格仅取决于软件计算的变量。根据我们使用的模型，这些变量的值在第一个软件周期之前完全因此，在第一次迭代之前，不可能保证关于它们的值的任何规则。公式前面的X运算符表示此参数。组2.1的LTL规格具有另一个X操作符位于→操作符的右侧。 它表达软件的编写方式是在分配信号（G变量）之前执行锁定命令（LS变量）的分配。因此，信号的状态将仅在下一个周期在锁定命令处被接收。N.G. Ferreira，P.S.Muniz Silva/Electron.注意Theor。Comput. Sci. 130（2005）323339表2规则组规则LTL规格K1（！ 1L05TP！ 1L04TP）-> XX（！ 1L05-1L04-35！ 1L05-1L04-50！1L05-1 L04 -68）和其他39个相同格式。22.1X（（X99-AG |X99-BG|公司简介|X99-DG）->X（！X99-1LS！X99-2LS））22.2（X99-1RWCK）|X99-2RWCK）->X！（（X99-AG& X99-CG）|（X99-AG& X99-DG）|（X99-BG&X99-CG）|（X99-BG&X99-DG））12.3（X99 - 2RWCK）->X！（X99-AG）|X99-BG|公司简介|X 9 9 -DG）12.4（X99-1RWCK -> X！（X99-AG）|X99-CG））（X99-2RWCK -> X！（X99-BG）|X99-DG））12.5！（X99-1NWCK）&X99-2NWCK）->X！（（X99-AG& X99-CG）|（X99-AG& X99-DG）|（X99-BG&X99-CG）|（X99-BG&X99-DG））13X！（X99-AG）&X99-BG）X！（X99-CG X99-DG）14X（（！X99-AG）->（！1L05-1L06-50！1L05-1L06-68））X（（！X99-BG）->（！1L07-1W06-35！1L07-1W06-50！1L07-1L06-68））X（（！X99-CG）->（！2L07-2W06-35！2L07-2W06-50！2L07-2L06-68））X（（！X99-DG）->（！2L05-2W06-50！ 2L05-2W06-68））14.4实验所有的规则都得到了有效的验证。表3显示了已验证的组（G）、该组中的属性数量（n）和规范的深度（k）。它还显示了NuSMV所需的内存（Mb）以及完成所有组属性验证所需的时间（秒）。我们使用了一台Athlon 2800+ CPU的计算机从表3中可以看出，所使用的技术避免了状态爆炸问题。此外，模型检查器实现了快速的验证时间。考虑到这是一个非常积极的结果，我们尝试在更大的部分验证相同类别的规则。新的实验室是一个更复杂的轨道部分，有大约800个数字输入，1150个状态变量，近60个轨道电路，7个点，和18个信号。340N.G. Ferreira，P.S.Muniz Silva/Electron.注意Theor。Comput. Sci. 130（2005）323我们花了大约四个小时来编写新的LTL规范。结果示于表4中。表3第一部分GnKMBt（秒）14023317.52.112250.82.2-2.551210.9321190.4441190.6表4第二部分GnKMBt（秒）14328342.12.122655.52.1337719.52.2-2.591545.4391503.94141504.75相关工作上述结果与文献[8]和[6]报道的成功结果一致后者实现了一个大约2000个变量的系统的几分之一秒的验证时间，k= 1。系统规模和验证时间都接近我们。[7]使用基于BDD的模型检查器成功验证了两个地铁站的控制软件，并证明了以与我们的格式接近的格式编写的规范，尽管这些规范是以而不是LTL。在我们的实验中，我们想知道我们是否也能够使用BDD来验证我们的属性。不幸的是，NuSMV无法验证任何规格，所以我们决定进行实验N.G. Ferreira，P.S.Muniz Silva/Electron.注意Theor。Comput. Sci. 130（2005）323341使用另一个容易获得的SMV实现称为Cadence SMV [1]，试图验证上面定义的四个组中的每个组的一个属性。简单部分的结果范围从25秒的执行时间和65MB的内存用于验证组1的属性到由于内存不足而导致的组4属性无法验证较大节段的规格。因此，尽管[7]使用基于BDD的模型检查报告了良好的结果，但我们得出结论，基于SAT的BMC似乎更有希望用于我们的领域。与我们一样，[6]无法使用BDD和拟议的BMC验证其系统。然而，它提出了一种不同的方法来验证安全属性：而不是使用时态逻辑编写规范，它提出了附加到程序末尾的新变量的定义。这些变量表示系统不变量，每个变量的值都是其他变量的当前值和下一个值的函数领域专家工程师应该根据他们对安全要求的解释创建不变量这种方法的基本原理是，作者认为使用专家领域工程师熟悉的语言对于他们的建议是有用的至关重要的。我们