Automated Verification of Signalling Principles in Railway Interlocking Systems

被引：30

作者：

Kanso, Karim ^{[1
]}

Moller, Faron ^{[1
]}

Setzer, Anton ^{[1
]}

机构：

[1] Swansea Univ, Dept Comp Sci, Swansea, W Glam, Wales

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2009年 / 250卷 / 02期

基金：

英国工程与自然科学研究理事会;

关键词：

ladder logic; railway interlocking systems; SAT solvers; verification; automated theorem proving; signalling principles; safety properties;

D O I：

10.1016/j.entcs.2009.08.015

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

In this paper we present a verification strategy for signalling principles for the control of a railway interlocking system written in ladder logic. All translation steps have been implemented and tested on a real-world example of a railway interlocking system. The steps in this translation are as follows: 1. The development of a mathematical model of a railway interlocking system and the translation from ladder logic into this model. 2. The development of verification conditions guaranteeing the correctness of safety conditions. 3. The verification of safety conditions using a satisfiability solver. 4. The generation of safety conditions from signalling principles using a topological model of a railway yard.

引用

页码：19 / 31

页数：13

共 15 条

[1]

Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1

[2]

Biere A., 2008, HDB SATISFI IN PRESS

[3]

Bjorner D, 2004, INT FED INFO PROC, V156, P607

[4]

Clarke EM, 1999, MODEL CHECKING, P1

[5]

Eriksson L., 1997, 3 SWED NAT RAIL ADM

[6]

Eriksson L., 1997, 4 SWED NAT RAIL ADM

[7]

Eriksson L., 1999, 99 ASPECT IRSE

[8]

Fokkink W., 1998, P FMICS, V98, P171

[9]

Kanso K, 2008, THESIS

[10]

Kullmann Oliver, 2008, Complexity of Constraints. An Overview of Current Research Themes, P283, DOI 10.1007/978-3-540-92800-3_11

← 1 2 →