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

兰州交通大学毕业设计 论文 1 铁路车站联锁系统集成自动认证的安全性需求设计铁路车站联锁系统集成自动认证的安全性需求设计 摘摘 要要 铁路联锁系统 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 验证必须通过模型检测 事实上 因为 兰州交通大学毕业设计 论文 2 RIS 是若干个有限状态组成的系统 所以通过模型穷举检测自动验证是符合实际的 图 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 在本文中 我们提出了一个案例研究 探索整合自动形式化验证方法在一个行业 系统的可能性 阿尔斯通就是这种情况 设计流程 在我们的工作中克服的主要障碍有 兰州交通大学毕业设计 论文 4 1 选择一个正式的验证工具 能有效解决典型的验证问题 2 在节约成本的情况下尽可能的集成所选中的所有系统 而且有新增功能时无需 使正在使用流程已经彻底的改变 3 保持低成本的安全要求的编写形式 事实上 安全的要求通常是由客户以非专 业的方式给出 而使用验证和安全验证流程必须是正式编程语言编写的 基本上这是 信号专家手工做的 而且最好避免再培训这些人学编程语言 我们能够设计出一个成功的整合策略以满足上述限制 据我们所知 在类似于我 们的设计流程的方案上的完全集成的自动验证还没有得到完全解决 到目前为止 这 是我们的主要成果 1 我们能够嵌入基于 SAT 的模型在我们的目标的设计流检测 这是通过嵌入模型 检查器 BMC 所做的 有界模型检查器 1 在设计流程 BMC 变换的有界模型检 测问题转化为可满足性问题 然后可以使用 SAT 求解器解决的 为此 我们使用了 SATO 8 这是一个非常有效的 SAT 求解器 2 我们可以将新的验证程序插入到设计流程里而不需要修改原设计流程 事实上 我们试图以现有的设计工具透明地管理互联模型核查 这样的互联接口 只需要一个 简单的格式翻译到 BMC 的输入格式 这就像从对设计者使用需求转化为网表来定义 RIS 一样 3 我们应避免产生重新培训信号专家使之掌握很多编程语言的这种不切实际的想 法 我们通过书面形式要求已经实现了使用同一种语言用来定义联锁逻辑 这允许信 号专家用他们非常熟悉的语言写正式的需求 从而避免再培训的人员 在我们的例子中使用的语言对 NE 的联锁逻辑参数关于火车站在考虑 由于安全 性要求的形式也在考虑参数关于火车站 需要注意的是 安全要求的重要取决于客户 的一般 安全 的规则和不考虑特定的火车站 这使我们能够重用同一客户相同的正 式规范 这是一个相当大的节省因为 RIS 设计客户 铁路公司 不会经常变化 4 为了表明我们的整合策略的确可以处理现实生活中的 RIS 设计 我们展示出了 新加坡地铁正在使用的一些安全需求验证联锁系统的实验结果 有限状态程序定义了 超过 2000 个 RIS 开关量 对于这样的系统的安全需求的确认时间在秒级以内 设计流程设计流程 下面将简短地介绍与我们设计相关的部分内容 车站平面布置图是从客户 即一个铁路公司 拿到的 一个站平面布置包括了轨 道绝缘节和信号机的位置等其他设施 通常车站布局是铁路公司以图纸的形式规定的 举例站场图在 29 兰州交通大学毕业设计 论文 5 但是进一步讨论 我们需要的是一个文本的表示法 那么 就要根据客户提供的 车站图纸来生成该站平面布置图的文本表示形式 这种文本表示使用 Prolog 编程语言 来翻译定义车站的布局 联锁关系由客户给出非编程语言的形式 这些规则的形式 通过信号专家使用像 prolog 编程语言来翻译 Prolog 的数据确定了车站布局和正式的联锁规则 这个规则作为输入到称之为 ADES2 阿尔斯通旗下的一个有专利的专家系统 ADES2 产生输出一个具有限状态 程序 这个程序就是我们需要的 RIS 图 2 更确切地说 ADES2 输出一系列布尔方 程明确了有限状态机 FSM 实现了对联锁系统的控制逻辑 ADES2 输出可以控制其他的工具 这些工具产生一个 EPROM 的执行命令来响应 ADES2 对 FSM 的操纵 我们的任务是验证由 ADES2 输出满足给定的安全要求 我们必须制定一个合理的 方式来定义安全要求以适应阿尔斯通信号专家 图 2 设计流程 验证的集成验证的集成 对我们来说 这个系统应当可以被 ADES2 识别而且作为 ADES2 的输出 这个输 出就是有限状态机实现联锁控制的规则 要注意的是 联锁规则并不是我们这里讨论 的安全需求 产品说明书是用自然语言来描述安全需求的清单 这种特性要求我们使用一种能 适应认证机构的标准化语言来编写 最后 符合系统规格需求和说明书的程序必须能在自动认证系统中可靠运行 而 且所得结果又应以工程师熟悉的格式给出 在接下来的论述中 我们将详细介绍如何将满足上述需求项目的设计流程以我们 的方式植入自动认证的集成系统里 我们的目标不是解释 ADES2 语法 因此 为了提高可读性和节省空间 在我们的 论述 下面我们将修改 ADES2 语法使它像 或多或少 已知的语言 兰州交通大学毕业设计 论文 6 结结 论论 我们所展示的案例旨在探索在像 RIS 这样的工业设计流程中建立一个集成的自动 验证系统方案的可行性 我们所克服的主要困难是 如何选择一