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

铁路车站联锁系统集成自动认证的安全性需求设计 摘 要 铁路联锁系统（RIS）是一个嵌入式系统（即一个监控系统），该系统是为了保证一个火车站的安全运行。当然，RIS是一个故障-安全系统。 在本文中我们探讨在一个给定的行业系统即铁路联锁系统中设计集成自动形式化验证方法的可能性。 我们的工作主要的障碍是：选择一个正式的验证工具，有效地解决手头的问题和设计验证的成本有效的整合策略等工具。 最后，我们是能够设计出一个成功的整合策略以满足上述约束。而且这样做既不需要修改原设计也不用再培训人员。 我们专为新加坡地铁的做了这项验证实验。实验表明，我们的集成策略自动验证系统设计的确能适应现实的生产实际。 介 绍 铁路联锁系统（RIS）是一个嵌入式系统（即一个监控系统），以确保在火车站的设备能安全运行。如RIS确保不可能使（无论手动或通过一些其他的系统自动控制）可能会导致列车碰撞的道岔发生动作。图1显示了一个联锁系统的作用在铁路控制层次。结构 很明显，RIS是一个故障-安全系统。的确，RIS的客户（通常是铁路公司）越来越重视新设计的系统安全性的依据。权威机关和即将到来的标准（如CENELEC EN50128/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是若干个有限状态，通过模型自动验证是。 图1 联锁系统 通过模型检[ 2 ]这种手段，自动验证已经非常成功地用于硬件设计模型。事实上，一个考虑给定属性的系统模型它保证的状态空间。这增加了设计的信心正确性。在我们的RIS的实现一个有限状态编程语言语法和语义VCL [ 6 ]非常相似用于系统设计的编程语言。因此，我们而言，RIS的实现是一个有限状态程序定义。我们的目的是验证这些程序满足给定的规格。因为我们是直接验证RIS程序，我们没有任何建模活动因此没有建模误差（抽象）。在这方面我们相同的（安全要求）是由信专家给我们。我们在这里的任务是RIS程序使之具备这样的。因此，例如，如（即“我们的要求是正确的吗？”），过程的（）完整的设不属于我们的工作范围。这些问题已经由信专家其他方法。 一个程序PRIS和一个正式的安全求φ。输出是是当P满足φ当P不满足φ。 虽然模型检测是一个详尽的方法，在我们的是作为一种增加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为基础的）模型检查，有界模型