铁路车站联锁系统集成安全需求自动验证的设计

兰州交通大学毕业设计（论文）-1-铁路车站联锁系统集成自动认证的安全性需求设计摘要铁路联锁系统（RIS）是一个嵌入式系统（即一个监控系统），该系统是为了保证一个火车站的安全运行。当然，RIS是一个故障-安全系统。在本文中我们探讨在一个给定的行业系统即铁路联锁系统中设计集成自动形式化验证方法的可能性。我们的工作主要的障碍是：选择一个正式的验证工具，有效地解决手头的问题和设计验证的成本有效的整合策略等工具。最后，我们是能够设计出一个成功的整合策略以满足上述约束。而且这样做既不需要修改原设计也不用再培训人员。我们专为新加坡地铁的做了这项验证实验。实验表明，我们的集成策略自动验证系统设计的确能适应现实的生产实际。介绍铁路联锁系统（RIS）是一个嵌入式系统（即一个监控系统），以确保在火车站的设备能安全运行。如RIS确保不可能使（无论手动或通过一些其他的系统自动控制）可能会导致列车碰撞的道岔发生动作。图1显示了一个联锁系统的作用在铁路控制层次。结构很明显，RIS是一个故障-安全系统。的确，RIS的客户（通常是铁路公司）越来越重视新设计的系统安全性的依据。权威机关和即将到来的标准（如CENELECEN50128/129欧洲[4,5]）也要求越来越强烈地意识到每个新设计的RIS的安全性。因此，当要设计一个风险很大的项目而且需要付出极大精力去规范其正确性。不用说，这往往会增加生产成本以及上市时间,而这是由于RIS不断加深的复杂性。在这种情况下，增加系统设计的正确性（关于给定的规格）和减少可能的生产时间和成本成了开发新系统所必须要考虑的。人们研究了很多方法来解决上面的问题。例如参考书目[6，9，14，15，16，17，18，19，20，21，22，23，24，25，26]。我们工作的目标是在一个给定的工业设计流程中有效地整合RIS实现自动验证在一个给定的工业设计流程。给出的例子很接近我们的论文：[6，7]。请注意，我们目前研究的是在一个给定的工业设计流程一体化的自动验证而不是验证研究一个给定的火车站的案例，案例研究（例如在[7]）。由于我们是研究自动验证，所以对RIS验证必须通过模型检测。事实上，因为RIS兰州交通大学毕业设计（论文）-2-是若干个有限状态组成的系统，所以通过模型穷举检测自动验证是符合实际的。图1联锁系统通过模型检测[2]这种手段，自动验证已经非常成功地用于硬件设计模型。事实上，在一个需要考虑给定属性的系统模型里，它保证能取到所有的状态空间样本。这种方法增加了设计者的自信心和设计产品正确性。在我们的论文中，RIS的实现需要使用一个有限状态编程语言，它的语法和语义和VCL[6]非常相似，它就是用于RIS系统设计的编程语言。因此，对我们而言，RIS的实现就是对一个有限状态程序的定义。我们的目的是验证这些程序满足给定的规格。因为我们是直接地把自动验证程序应用于RIS程序，而且我们没有任何建模活动，因此就没有建模误差（抽象）。在这方面我们与一开始就有来自网络表格的硬件电路认证的设计方案面临着相同的实际情况。产品所能完成的功能（安全要求）是由信号方面专家给我们的。我们在这里的任务只是马上编写RIS程序使之具备这样的功能。因此，例如，如需求上的确认（即“我们的要求是正确的吗？”），编程过程中的准确性（例如，信号人员人工完成的工作）还有如RIS一系列完整的功能需求的设计则不属于我们的工作范围。这些问题已经由信号专家用其他方法得以解决。输入我们设计程序的是一个程序P，P规定为RIS和一个正式的安全需求程序φ。而输出是标准是判断当P满足φ时，转向YES，当P不满足φ时，则转向NO。虽然模型检测是一个详尽的方法，但这个方法在我们的论文中是作为一种增加RIS设计自信心的工具。事实上，即使与模型检查器检查正确，许多问题可能仍然是存在的。例如，模型检验的正确性通常是通过非正式方法得以证明的，所以说它只是依赖于测试。通常用以判断正确性的软件同样只有在与相适应的模型检查器互联之后才能适应生产兰州交通大学毕业设计（论文）-3-流程。我们的目标不是来解决这些问题。这就是我们的目的不是证明（不管那意味着什么）RIS的正确性。在考虑到成本和效益的问题上，我们还没有那种能力既要求成本又要求做到尽可能的集成，模型检查在给定的设计流程，以增加RIS设计信心。这意味着我们接受使用的工具（如模型检查器，接口的软件）没有正式的评价认证。然而，模型检查器是广泛使用的工具。因此，他们已经经过许多独立的用户的多次测试。此外，软件界面很简单。它通常包括从一个格式翻译到另一个。因此，通常地测试就足以发现错误。所有的模型检查器的核心（SMV[10],Mur[27],SPIN[28])的可实现性分析，即所有的状态可从给定的初始状态集开始计算。可实现性分析可以以多种方式实现。这是每一个有效的特定类别的系统所共同具备的。有序二元决策图（OBDDs）已成功地用于实现数字电路的模型检查器（例如[2，10]）。OBDDs提供了一个紧凑表示布尔函数，换句话说，是用来表示系统状态转换关系进行验证，以及可实现状态集。然而，以OBDD为基础的方法来验证硬件设计比较成功，但往往是低效率的，在RIS中产生的布尔开关量往往非常多（通常在数千以上）。一个典型的（往往是成功的）RIS的自动验证的方法是使用基于SAT求解器（即工具，解决SAT问题是能力的布尔函数）或同义反复检查（即该工具检查一个布尔函数是否全为1）。这些方法，例如在[6，9]。当使用SAT求解器的验证问题转化为可满足性问题的布尔函数。这是通过计算可实现状态集，即可以到达的状态的步骤从初始状态集。这意味着，当我们使用基于SAT的模型检查我们的视野是有限的，而当使用OBDDs我们计算状态从初始状态到全套。出于这个原因，基于SAT的模型检查也被称为有界模型检测。虽然比少的表现（OBDD为基础的）模型检查，有界模型检测（即基于SAT的）通常足以处理典型的安全要求在RIS域发生。事实上，在RIS设计中通常注重是检查不开关量。这个要求就是任何系统处于的所有状态数据都要保存。不开关量可以以系统的所有状态的集合作为初始状态集，通过计算一组可到达状态检查。这个问题可以很容易地变成一个令人满意的布尔函数问题。有人可能会问，为什么在RIS域检查通常基于SAT的模型检查而不是基于OBDD模型。直观地这是因为RIS（不同于数字电路）都建立了弱耦合的子系统。在讨论这一点，我们读者参考[6，9]。在本文中，我们提出了一个案例研究，探索整合自动形式化验证方法在一个行业系统的可能性（阿尔斯通就是这种情况）设计流程。在我们的工作中克服的主要障碍有：1.选择一个正式的验证工具，能有效解决典型的验证问题。2.在节约成本的情况下尽可能的集成所选中的所有系统，而且有新增功能时无需使兰州交通大学毕业设计（论文）-4-正在使用流程已经彻底的改变。3.保持低成本的安全要求的编写形式。事实上，安全的要求通常是由客户以非专业的方式给出，而使用验证和安全验证流程必须是正式编程语言编写的。基本上这是信号专家手工做的。而且最好避免再培训这些人学编程语言。我们能够设计出一个成功的整合策略以满足上述限制。据我们所知，在类似于我们的设计流程的方案上的完全集成的自动验证还没有得到完全解决，到目前为止，这是我们的主要成果。1.我们能够嵌入基于SAT的模型在我们的目标的设计流检测。这是通过嵌入模型检查器BMC所做的（有界模型检查器，[1]）在设计流程。BMC变换的有界模型检测问题转化为可满足性问题，然后可以使用SAT求解器解决的。为此，我们使用了SATO[8]这是一个非常有效的SAT求解器。2.我们可以将新的验证程序插入到设计流程里而不需要修改原设计流程。事实上，我们试图以现有的设计工具透明地管理互联模型核查。这样的互联接口，只需要一个简单的格式翻译到BMC的输入格式，这就像从对设计者使用需求转化为网表来定义RIS一样。3.我们应避免产生重新培训信号专家使之掌握很多编程语言的这种不切实际的想法。我们通过书面形式要求已经实现了使用同一种语言用来定义联锁逻辑。这允许信号专家用他们非常熟悉的语言写正式的需求，从而避免再培训的人员。在我们的例子中使用的语言对NE的联锁逻辑参数关于火车站在考虑。由于安全性要求的形式也在考虑参数关于火车站。需要注意的是，安全要求的重要取决于客户的一般（安全）的规则和不考虑特定的火车站。这使我们能够重用同一客户相同的正式规范。这是一个相当大的节省因为RIS设计客户（铁路公司）不会经常变化。4.为了表明我们的整合策略的确可以处理现实生活中的RIS设计，我们展示出了新加坡地铁正在使用的一些安全需求验证联锁系统的实验结果。有限状态程序定义了超过2000个RIS开关量。对于这样的系统的安全需求的确认时间在秒级以内。设计流程下面将简短地介绍与我们设计相关的部分内容。车站平面布置图是从客户（即一个铁路公司）拿到的。一个站平面布置包括了轨道绝缘节和信号机的位置等其他设施。通常车站布局是铁路公司以图纸的形式规定的。举例站场图在[29]。但是进一步讨论，我们需要的是一个文本的表示法。那么，就要根据客户提供的车站图纸来生成该站平面布置图的文本表示形式。这种文本表示使用Prolog编程语言来翻兰州交通大学毕业设计（论文）-5-译定义车站的布局。联锁关系由客户给出非编程语言的形式。这些规则的形式，通过信号专家使用像prolog编程语言来翻译。Prolog的数据确定了车站布局和正式的联锁规则，这个规则作为输入到称之为ADES2——阿尔斯通旗下的一个有专利的专家系统，ADES2产生输出一个具有限状态程序，这个程序就是我们需要的RIS（图2）。更确切地说ADES2输出一系列布尔方程明确了有限状态机（FSM）实现了对联锁系统的控制逻辑。ADES2输出可以控制其他的工具，这些工具产生一个EPROM的执行命令来响应ADES2对FSM的操纵。我们的任务是验证由ADES2输出满足给定的安全要求。我们必须制定一个合理的方式来定义安全要求以适应阿尔斯通信号专家。图2设计流程验证的集成对我们来说，这个系统应当可以被ADES2识别而且作为ADES2的输出，这个输出就是有限状态机实现联锁控制的规则。要注意的是，联锁规则并不是我们这里讨论的安全需求。产品说明书是用自然语言来描述安全需求的清单，这种特性要求我们使用一种能适应认证机构的标准化语言来编写。最后，符合系统规格需求和说明书的程序必须能在自动认证系统中可靠运行，而且所得结果又应以工程师熟悉的格式给出。在接下来的论述中，我们将详细介绍如何将满足上述需求项目的设计流程以我们的方式植入自动认证的集成系统里。我们的目标不是解释ADES2语法。因此，为了提高可读性和节省空间，在我们的论述，下面我们将修改ADES2语法使它像（或多或少）已知的语言。兰州交通大学毕业设计（论文）-6-结论我们所展示的案例旨在探索在像RIS这样的工业设计流程中建立一个集成的自动验证系统方案的可行性。我们所克服的主要困难是：如何选择一个高效有力的认证工具来快速处理认证上的问题。我们能够有效地整合基于SAT的有界模型在我们的目标设计流检测。我们实现了这一既不需要在既有设计流程上大幅修改也不需要再培训的人员的技术难题。此外，我们设计了一个架构，即允许的正式规范在不同的车站重复使用只要产品需求说明书没有变化（即只要RIS的客户不会改变）。为了评估我们设计的RIS在现场的效率，我们已经在新加坡地铁中得到了一些RIS的试验结果，这样的系统有2000多个开关量，而在我们的机器中每项功能的验证只花了不到0.5秒。