首页> 外文会议>Conference on Formal Methods in Computer Aided Design >Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks
【24h】

Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks

机译:通过基于SMT的交换式多域Kirchhoff网络模型检查对继电器联锁系统进行分析

获取原文

摘要

Relay Interlocking Systems (RIS) are analog electromechanical networks traditionally applied in the safety-critical domain of railway signaling. RIS consist of networks of interconnected components such as power supplies, contacts, resistances, and electrically-controlled contacts (i.e. the relays). Due to cost and flexibility needs, RIS are progressively being replaced by equivalent computer-based systems. Unfortunately, RIS are often legacy systems, hard to understand at an abstract level, hence the valuable information they encoded in them is not available.In this paper, we propose a methodology and a tool chain to analyze and understand legacy RIS. A RIS is reduced to a Switched Multi-Domain Kirchhoff Network (SMDKN), which is in turn compiled into hybrid automata. SMT-based model checking supports various forms of formal analyses for SMDKN. The approach is based on the modeling of the RIS analog signals (i.e. currents and voltages) over continuous time, and their mapping in terms of railways control actions. Starting from the diagram representation, we overcome a key limitation of previous approaches based on purely Boolean models, i.e. the presence of spurious behaviors. The evaluation of the tool chain on a set of industrial-size railway RIS demonstrates practical scalability.
机译:中继互锁系统(RIS)是传统上应用于铁路信号安全关键领域的模拟机电网络。 RIS由相互连接的组件网络组成,例如电源,触点,电阻和电控触点(即继电器)。由于成本和灵活性的需求,RIS正逐渐被等效的基于计算机的系统取代。不幸的是,RIS通常是遗留系统,很难抽象地理解,因此无法获得在它们中编码的有价值的信息。在本文中,我们提出了一种方法和工具链来分析和理解遗留RIS。 RIS被简化为交换多域Kirchhoff网络(SMDKN),该网络又被编译为混合自动机。基于SMT的模型检查支持SMDKN的各种形式的形式分析。该方法基于连续时间上的RIS模拟信号(即电流和电压)的建模以及它们在铁路控制动作方面的映射。从图表示开始,我们克服了以前基于纯布尔模型的方法的主要局限性,即存在虚假行为。对一组工业规模铁路RIS上的工具链的评估证明了实际的可扩展性。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号