铁路信号原理的自动验证

理论计算机科学电子笔记250（2009）19-31www.elsevier.com/locate/entcs铁路联锁系统中信号原理的自动验证1Faron Moller3 Anton Setzer4部斯旺西大学SwanseaUniversity Swansea，UK摘要在本文中，我们提出了一个验证策略的信号原理控制的铁路联锁系统写在梯形逻辑。所有的翻译步骤都已经在一个铁路联锁系统的真实例子中实现和测试。 在这个翻译的步骤如下：1.铁路联锁系统数学模型的建立及梯形逻辑到该模型的转换。2.制定验证条件，保证安全条件的正确性。3.使用满意度求解器验证安全条件。 4.使用铁路站场的拓扑模型从信号原理生成安全条件关键词：梯形逻辑，铁路联锁系统，SAT求解器，验证，自动定理证明，信号原理，安全特性。1引言在本文中，我们总结了在一个小型案例研究中所做的工作，其中一些在[9]中报道。在这个项目的范围内，我们编写了软件，允许使用SAT求解器技术对铁路联锁系统进行全自动验证。该软件已应用于英国一个小型铁路站场的联锁系统。项目发起人西屋铁路系统公司目前对应用形式化方法开发控制铁路设备（即信号和道岔）的软件感兴趣。软件是使用梯形逻辑开发的，梯形逻辑是一种表示布尔值赋值的低级语言。这个软件是模拟的1本文所述的研究是由第一作者在第二和第三作者的监督下作为研究硕士（MRes）项目进行的，并得到了英国奇彭纳姆西屋铁路系统公司的支持。2电子邮件：cskarim@swansea.ac.uk3电子邮件：F.G. swansea.ac.uk4电子邮件：A.G. swansea.ac.uk1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.08.01520K. Kanso等人/理论计算机科学电子笔记250（2009）19由经验丰富的信号工程师来查找错误。工程师们将尝试许多场景，这些场景通常在信号书中列出。该技术通常用于工业，捕获软件中的许多错误，但不能保证实现信令原理的阶梯的正确性这项研究的委托，以确定它是否是可行的，适用于梯形逻辑的正式方法，并验证信号的原则，在梯形逻辑程序。研究的一部分是实现原型验证系统。该系统的输入是：要验证的梯形逻辑、铁路站场模型和签名的预验证文件;如果确定了反例，系统将提供一个LATEX文档，详细说明出现反例时系统的状态。使用LATEX，是为了简化系统打印文本的操作，这样，生成的反例可以优雅地格式化和呈现，让工程师更容易理解英国铁路行业的信号原则是用简单的英语写的。 研究的第二个组成部分是定义一种形式语言，以精确地表示信令原则。我们已经编写了一个程序，它采用这种语言定义的信号原理，并产生梯形逻辑将被验证的安全条件。概述本文件的结构如下。我们首先提供一些铁路和联锁系统的背景然后，我们讨论了本研究中使用的验证技术。然后讨论从信号原理产生安全条件。最后，我们对相关工作进行了总结，并对所进行的研究进行了总结2铁路在解释验证系统如何工作之前，我们将提供有关铁路领域的一些背景信息。铁路分为铁路站场-即火车站和车辆段-和连接站场的开放线路。图1中示出了示例铁路调车场。本研究的重点是联锁系统控制铁路站场。铁路站场由以下部分组成：跟踪分段。列车线路被分成多个区段，并且每个区段与轨道电路相关联，轨道电路可以检测列车是否在区段上信号. 信号被放置在轨道段之间，并且信号仅从一个方向可见。信号显示不同的方面;这些方面通知列车司机前方线路的状态点 点是一种特殊类型的轨迹线段，用于将两条线合并为一条线。如果火车已经锁定，即到达一个确定的位置，并且已经在物理上和虚拟上K. Kanso等人/理论计算机科学电子笔记250（2009）1921通过软件。当一组点被锁定时，它们的两个可能位置被称为正向和反向。正常位置是当点允许列车在点上直线行驶时，而反向位置是当点允许列车在线路上分支或进入线路时。5除了唯一的轨道段标识符外，铁路站场中的每组点都有一个唯一的标识符航线路线由一系列顺序连接的轨道段组成，这些轨道段可能通过一组点在信号处开始和结束。线路由设计铁路站场时创建的控制表定义。路由可以设置为指示列车正在使用信号平台图1.一、一个铁路调车场的例子，调车场的所有部分都被命名。右边的灰色方框是平台。左边的箭头指示列车应该沿着线路行驶的方向。右边的黑框是“行结束”标记。这些“棒棒糖”被命名为s1，s2，. ..，S6是信号。大箭头表示路线C，见表1。图1所示的航迹规划描述了这些组件如何在拓扑上进行配置。铁路站场中各种组件的操作使用控制表来定义这些信息包含有关何时可以设置路线、点的位置以及信号应显示的方面的信息控制表负责执行信令原则。表1给出了定义四个路由的示例控制表。控制表中的路线C在图中用大箭头表示1.一、路线C从信号s2开始，在s4结束，跨越轨道段ts4a、ts3a、ts2a、ts2b和ts1b。作为安全预防措施，在允许列车进入路线之前，还要求轨道区段ts0b未被占用轨道段ts 3a、ts 2a和ts 2b也是道岔;ts 3a必须锁定在正常位置，而ts 2a、ts 2b必须锁定在反向位置。 在这种情况下，点总是成对地一起移动，因此在允许列车进入路线之前，点ts3b也必须锁定在正常位置。5虽然在许多情况下，如图中的例子1、明确应该在哪个位置正常和反向，一般来说，这是一个关于如何作出这一决定的惯例问题（例如，在主线分叉成两条线的情况下ts0aTS1ATS2aTS3ATS4ATS5ATS6APT1Pt2S1S2S3S4S5S6PT3TS1BTS2bTS4BTS5BTS6B轨道段点TS3Bts0bPT422K. Kanso等人/理论计算机科学电子笔记250（2009）19|W||/x|（z）|y|G =绿色，R =红色条件轨道段一S1S3G路由集ts1a、ts2a、ts3a、ts4a、ts5a、ts6ats2*，ts3*R路由未设置BS1S6G路由集ts1a、ts2a、ts3a、ts3b、ts4b、ts5b、ts6bTS 2*TS 3*R路由未设置CS2S4G路由集ts4a、ts3a、ts2a、ts2b、ts1b、ts0bTS 3*TS 2*R路由未设置DS5S4G路由集ts4b、ts3b、ts2b、ts1b、ts0bts2*，ts3*R路由未设置表1用于图1的铁路站场的不完全控制表。“起点”和“出口”列表示路线开始和结束的信号;“轨道段”列显示列车进入路线必须空闲的轨道段。两个 tsn* 是tsna和tsnb的缩写。 路线C如图所示。1.一、3联锁系统铁路联锁系统的设计是为了实现控制表中的约束。本研究所关注的联锁系统是使用梯形逻辑编程的，梯形逻辑是布尔赋值序列的图形表示x1：=101;···xn：=10n其中，每一个RPMI是一个命题公式，其变量取自输入、输出和中间命题变量（锁存器）的集合。布尔值赋值z：=（wx）y，如梯形逻辑所示，如图2所示。变量w，x，y和z图二. 用梯形逻辑表示锁存器（命题变量），/x是否定，K. Kanso等人/理论计算机科学电子笔记250（2009）1923z表示它是结果。系列中的文字，如图中的wx2表示合取，平行的文字表示析取。该图对微芯片进行编程梯形图由以下形式return;while（true）{return;return（）;x1：=1;.xn：=n}在初始化阶段，一些变量被设置为初始值，而其他变量则保持未定义。然后进入永久循环，其中执行以下步骤输入变量被设置为输入（来自控制面板的按钮、来自轨道段的传感器、来自点的传感器等的状态）;并且执行阶梯。请注意，在执行赋值时，输出变量不会修改;因此，仅在每次执行阶梯结束时才需要正确性。(The系统不需要在初始化之后立即是安全的，因为系统将仅在梯子已经被执行给定次数（例如n次）之后才被列车使用。我们要求系统在至少一次执行后是正确的但是在至少n步之后要求正确性就足够了4验证在梯形逻辑定义的系统中，安全属性的验证可以通过多种不同的方式实现。梯形逻辑在概念上很容易转化为命题逻辑;这被用来允许在命题逻辑的框架内进行验证因此，要验证的安全条件也在命题逻辑中定义。安全条件是一个命题公式，其中原子命题的范围在梯子内的原子命题上。本文中，安全条件是用来表示安全条件或安全条件的合取为了证明一个安全条件的正确性，我们需要证明在对每一个n≥1执行阶梯n次之后，安全条件成立。请注意，当n= 0时，不需要保持，因为允许初始状态违反安全条件。在我们的系统中，我们通过归纳证明了这一点：我们表明，在初始化和执行一次阶梯之后，如果在执行梯子，也是后来才有的。这种技术是对Fokkink在[8]中介绍的第一种方法的加强;关于两种方法的详细比较，请参见我们的第724K. Kanso等人/理论计算机科学电子笔记250（2009）19我更正式地说，我们定义了一个命题公式I，它定义了系统的初始状态（梯形逻辑程序并没有给初始状态中的所有变量赋值）。例如，如果变量x，y，z最初设置为值a，b，c，则<$I=（xParticipa）<$（yParticipb）<$（zParticipc）。此外，我们还定义了一个公式，它模拟了阶梯的执行为简单起见，假设xi都是不同的，表示变量在执行阶梯，则RNL具有形式（xJ参与者J）··（xJ参与者J）1 1n n这里，xJ是表示变量执行后的状态的新变量并且是替换x1，...，xi−1乘xJ，.，xJ在阿瓜里。 第一个证据i1i−1公式，对应于基本情况，具有以下形式ψI∧ϕL →ψJ其中，XIJ是将Xij中的每个原子命题x替换为xJ的结果。它表示在梯子的第一次迭代之后，联锁系统处于安全状态。第二个公式是归纳步骤，并证明了从安全条件不成立的任意状态，在执行梯子后，安全条件仍然成立。ψ∧ϕL→ψJ这两个公式应始终成立，以证明梯子安全条件的正确性当使用SAT求解器时，两个公式都被否定;因此，如果安全条件成立，则两个公式都不应满足。实施例1如果• 初始化将变量x设置为true：• 安全条件是y参与：：=yParticix和• 阶梯有一个赋值，表示x：=y：L：=xJ参与然后我们得到公式和. （xParticiptrue）xJParticipy→yParticipxJ.（yParticex）xJParticey→yParticexJ在这个简单的例子中，是可以证明的为了验证，我们使用SAT求解器来搜索一个令人满意的分配，该分配会证伪上述两个公式中的一个限制上面描述的证明系统支持这样的问题，即当试图验证安全条件时，我们可能获得假阳性，即反例K. Kanso等人/理论计算机科学电子笔记250（2009）1925这实际上是不可能发生的。可能存在安全条件成立的状态，但是使得在阶梯的执行之后违反安全条件;然而，原始状态可能是不可达的。为了确定反例是否真实，有必要找到从初始状态到已识别反例的踪迹。这并不是直接与我们的归纳证明系统6。为了减轻误报的识别，放松了归纳语句收件人：（LInv）→J其中，ninv是阶梯的不变量。我们使用了两种正交技术来识别这样的不变量Ninv：1) 并非所有输入变量的选择都对应于物理上可能的状态。一个示例是具有3个位置A、B、C的3路开关（例如“从中央面板控制”、“由本地站控制”和“由应急面板控制”）。这样一个开关的输出将由3个变量表示，一个表示是否选择A，一个表示B，一个表示C。在任何时候，最多选择A、B或C中的一个（可能不选择这些中的任何一个，例如，如果开关在位置之间）。因此，我们得到了不变量A→（C）B→（C）C→（B）2) 某些变量的组合是不可访问的。当仔细观察假阳性时，通常会发现一些变量处于不应该到达的状态，通常是当两个变量彼此相关例如如果一个信号灯在这种情况下，我们将获得不变量信号i是红色参与信号i是绿色。当发现这样一个可能的不变量时，我们试图证明它实际上是一个不变量，即它总是成立：（一） 公司简介JInv和（公司简介JInv如果这是可证明的，那么我们可以假设这个不变量在执行阶梯之前保持不变。唉，有效地自动识别不变量是一个主要的研究领域。6用于产生误差迹线的解决方案是已知的，但在本研究中尚未探索一个这样解决方案是使用Fokkink在[8]中介绍的时间副本，或者应用模型检查技术，连续识别从初始状态到反例的可达状态集，产生计算路径[1，4]。）→）→26K. Kanso等人/理论计算机科学电子笔记250（2009）195将信号原理转化为安全条件本研究中使用的信号原理直接涉及铁路行业。它们被设计师用作语法，通常尽可能精确地用自然语言编写。研究的一个目的是定义一种正式的明确的语言，用它来制定信令原则。典型的信令原理是：“Points in a railway yard should not be set正常和反向位置同时进行。正向和反向是一组锁定点的两个可能位置信号原则并不直接涉及任何特定的铁路站场或其中的实体。具有一般谓词的一阶逻辑是形式化表达这些原则的理想逻辑;上述原则可以翻译为：点：<$[normal（pt） 反向（pt）]这些一阶公式需要转化为一个命题公式（安全条件）;为此，我们建立了一个铁路站场的拓扑模型，联锁系统是为这个站场设计的。Prolog数据库用于该拓扑模型。铁路站场中的实体被命名，并且关系被用于对地形方面进行建模。 例如，两个连接的轨道段将使用连接的二元谓词进行关联。 在这项研究中，跟踪计划和控制表（手动）转换成Prolog数据库。然后，可以自动查询该数据库，以帮助翻译信令原理。转换有两个步骤：第一步是删除量化，第二步是将谓词解析为来自阶梯的文字或取决于上下文的常量布尔值信号原理中的变量在有限域中变化，因为所有的铁路站场都是有限的。因此，普遍的量化可以用有限的合取来代替，存在的量化可以用有限的分解来代替。拓扑模型将被查询一组有限的量化值。例如，在示例信号原理中引入的变量pt的范围在铁路站场中的所有点的域其次，将谓词分解为文字。 这是通过指定一个谓词列表以及如何减少谓词来完成的。此列表对于每个铁路站场都是唯一的，因为不同的铁路站场遵循不同的命名约定。例如，在示例信令原理中使用的谓词normal（pt）将通过字符串连接操作被简化为文字未在铁路站场指定列表中指定的谓词使用Prolog和拓扑模型解析为常量布尔值（参见下面的示例2因此，第二类谓词极大地简化了信号原则的表述，因为安全条件可以被赋予保护。K. Kanso等人/理论计算机科学电子笔记250（2009）1927实施例2考虑一个信令原理，例如“All points that are part of a route must be locked if the route is这被形式化为pt ∈ Points：的 谓词 集合（rt） 和 锁定（pt） 是 简化为文字;以及如果点pt是路线rt的一部分，则（pt，rt）的点部分被简化为真，拓扑模型，否则将失败。在这种情况下，验证包括证明set（rt）→locked（pt）对于点pt是路线rt的一部分的所有情况都成立。实施例3考虑一个简单的铁路站场，只有两个点pta和ptb和一个信号原理：点：<$[normal（pt） 反向（pt）]删除量化和等同器械后，产生以下安全条件<$[pta.Normal ∧pta.Reverse] ∧正常 反向]为了更精确地识别可能的反例的原因，安全条件-6执行为这项研究而实现的软件将信号原理、联锁系统的梯形逻辑和拓扑模型作为输入一般情况下，您需要创建并启动虚拟化。如果确定了反例，则提供LATEX数据。用于该项目的SAT求解器称为OKSolver，由Kullmann [12，10]编写，是OKlibrary [11]的一部分。的验证的联锁系统有331个赋值和599个变量。为了便于说明，已经验证了两个信令原则;表2包含有关条款验证的信息。表中的第一部分验证了联锁系统在同一个执行周期内永远不能将点移动到正常位置和反向位置。第二部分表明，在试图验证如果一个点被占用，那么它就被锁定在位置上时，已经确定了反例。这第二个信号原理仅用于演示目的，并不意味着铁路是不安全的，因为证明系统允许火车神奇地出现和消失。因此，如果一个点没有被锁定，那么SAT解算器将在该点上放置一列火车，从而创建一个反例。有趣的是，第一个信号原理，当子句集都是unsat- is fiable时，在验证子句集时具有非常快的运行时间第二28K. Kanso等人/理论计算机科学电子笔记250（2009）19子句集部分条文许多变量OKSolver运行时间（秒）点非正常和反向01471340760.06pointsNotNormalAndReverse0.ind1291635590.06点非正常和反向11471340760.13pointsNotNormalAndReverse1.ind1291635590.14已占用点数已锁定01471340760.25occupiedPointsLocked0.ind1293035601.34已占用点数已锁定11471340760.21occupiedPointsLocked1.ind1293035601.33已占用点数已锁定21471640760.25occupiedPointsLocked2.ind1293035601.37已占用点数已锁定31471340760.27occupiedPointsLocked3.ind1293035601.3表2条款集和验证时间，斜体的条款集是满意的。 子句设置以ind是验证的归纳步骤，没有的是基本情况。信令原则，当子句集都满足时，具有更大的平均运行时间，特别是通过归纳步骤。7相关工作已经有许多尝试将形式化方法应用于铁路及其相关的联锁系统。事实上，这是Dines Bjørner提出的“大挑战”的主题[3]。Eriksson在十多年的时间里成功地将形式化方法应用于该问题，特别是代表Banverket（瑞典国家铁路管理局）[5，6，7]。这种方法通过创建两个数学模型来工作：第一个是联锁系统的数学模型，由规则组成，第二个是联锁系统设计的铁路站场的拓扑方面。通过证明信号原理适用于铁路站场拓扑模型中的联锁系统模型验证使用了Prover7公司生产的NP-Tools软件[5]。NP工具是与证明引擎打包在一起的工具集合;这些工具将各种问题转换为证明引擎可接受的格式进行处理。的7www.prover.comK. Kanso等人/理论计算机科学电子笔记250（2009）1929NP-Tools实现的证明系统记录在[15]中。NP-Tools已被许多其他公司用于关键系统的正式验证，如ADTranz，Saab和Volvo。Morley将形式化方法应用于英国铁路固态联锁（SSI），专注于SSI之间的安全属性和通信协议我们的方法有点不同，因为我们专注于低层次的布尔逻辑，而SSIFokkink演示了如何使用梯形逻辑编程的联锁系统可以自动验证，以确保它正确执行控制表[8]。这项工作不包括直接验证信号原理;只验证从控制表中得出的安全条件。本文讨论了两种验证技术。第一个证明了安全条件是执行梯子的逻辑结果。 让我们把它当作梯子的模型在命题逻辑中，它是一个安全要求。 使用的证明义务福金克群岛L→如果该义务成立，则证明在梯子的任何执行之后，安全要求将始终成立，即使在执行梯子之前系统处于不可达状态请注意，我们的方法只要求，如果在执行梯子之前，系统处于初始状态或处于安全要求也成立的状态，则该义务成立。因此，我们的方法，限制了安全条件所需的状态的数量，以保持一个较小的状态子集，其中包含所有可到达的状态，并可能有一些无法到达的状态。通过添加不变量，我们进一步减少了要考虑的不可达状态的数量，从而减少了误报的数量。Fokkink介绍的第二种技术创建了梯子的比例模型的时间副本。他引入变量xi（j），表示在阶梯8的j次执行之后变量xi的状态。一个时间副本<$i（i）将与<$i相同，但<$i中的所有原子命题x都被x（i）取代这种技术并没有表明，在任何梯子的执行后，安全要求将保持不变，但只有在有限数量的梯子执行后。举证责任是中文（简体） ∧ ϕ (k) → ψ (k)这种技术可用于证明时间安全要求，但不推荐使用，因为这种安全条件仅在有限次迭代中得到验证;对于安全要求是否保持超过阶梯的k次然而，如果找到了反例，那么反例是可达的，并且从伪造的赋值中，我们获得了从初始状态到它的迹[8]所以在我们的记法中，xi表示xi（0），XJ表示xi（1）。我30K. Kanso等人/理论计算机科学电子笔记250（2009）19库存L8结论我们的方法被应用到一个由我们的工业赞助商提供的模型中，这个模型是一个温和而典型的铁路站场，有331个任务和599个变量，代表一个有两个站台的车站和一条有两条轨道的铁路线。SAT求解器本身的运行时间从来不会超过几秒钟。我们能够证明各种各样的安全条件。我们发现了一些反例，这些反例是公司已经知道的，但被认为不是安全关键的，是间歇性的，只发生在梯子的一个循环中。为了证明这些反例实际上最多只发生一个周期，我们可以修改证明义务，证明如果系统处于安全条件不成立的状态，那么在执行一次梯子之后，它将证明公式是<$L→J我们可以将其限制为满足不变量的状态，即¬ψ ∧ ψ∧ϕ →J我们不知道我们的方法的规模有多大，因为我们只将其应用于一个普通的铁路站场。目前正在开发的联锁系统有3000多个任务。我们预计不会出现任何严重的问题，尽管满足性问题的性质意味着，当试图验证具有越来越多任务的联锁系统时，计算复杂性将呈指数级增长。该项目表明，铁路联锁系统的自动化验证，至少对于较小的例子，是可行的。我们的方法的主要优点是它的简单性，它在最低级别验证安全性引用[1] 拜尔角和I.Katoen，J.P.，[2] Biere，A.，M. Heule，H.van Maaren和T.Walsh，URLhttp://www.st.ewi.tudelft.nl/sat/handbook/toc.html[3] Bjørner ， D. ， TRAIN ： The Railway Domain ， in ： Building the Information Society ， IFIPInternational Federation for Information Processing156/2004（2004），pp. 607-611URLhttp://www.springerlink.com/content/527p7237102w5741/[4] 克拉克，E.，O. Grumberg和我。地方检察官佩莱德“Model checking,” Springer,[5] 埃里克森湖铁路联锁的正式验证，瑞典国家铁路管理局技术报告4（1997）。[6] 埃里克森湖《铁路联锁要求的正式化》，瑞典国家铁路管理局技术报告3（1997年）。[7] 埃里克松湖 和M. Fahl'en，An InterolockingSpecicatinLanguage，ASPECTIRSE99（1999）.[8] Fokkink，W.，P. Hollingshead，J. Groote，S. Luttik和J. van Wamel，联锁验证：从控制表到梯形逻辑图，工业关键系统形式化方法第三次研讨会论文集（FMICS'98）（1998），pp. 171-185.K. Kanso等人/理论计算机科学电子笔记250（2009）1931[9] Kanso ， K.，“Formal Verification of Ladder Logic,” Master’s thesis, Swansea University, Swansea,SA2 8PP, UK[10] Kullmann ， O. ， InvestigatingthebehaviorofaSATsolveronrandomformulas ， TechnicalReportCSR23-2002 ， SwanseaUniversity ， ComputerScienceReportSeries （ availablefromhttp://www-compsci.swan.ac.uk/reports/2002.html）（2002）.[11]Kullmann，O.，OKlibrary：一个生成研究平台（广义）SAT解决，技术报告CSR 1-2008，斯旺西大学，计算机科学报告系列（http://www-compsci.swan.ac.uk/reports/2008.html）的网站上进行了介绍。（2008年）。[12] Kullmann，O.，现在和未来的实际SAT解决，在：N。克雷乌山口Kolaitis和H.Vollmer，editors，Complexity of Constraints ， Lecture Notes in Computer Science （ LNCS ） 5250 ， Springer ，2008.283-319[13] Morley，M.，铁路信号数据安全：行为分析，计算机科学讲义（1994年），pp. 465-465[14] Morley，M.，铁路联锁安全级通信，计算机程序设计科学29（1997），pp. 147-170[15] Stéalmarck，G.和M. Sa Saugund，《计算机控制系统的安全性》（SAFECOMP90）（1990年），第100页。31比36