No Cover Image

Journal article 482 views

Automated Verification of Signalling Principles in Railway Interlocking Systems / Karim Kanso; Faron Moller; Anton Setzer

Electronic Notes in Theoretical Computer Science, Volume: 250, Issue: 2, Pages: 19 - 31

Swansea University Author: Moller, Faron

Full text not available from this repository: check for access using links below.

Abstract

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 f...

Full description

Published in: Electronic Notes in Theoretical Computer Science
ISSN: 1571-0661
Published: Amsterdam Elsevier 2009
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa13713
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: 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.
Keywords: formal methods, satisfiability, railway verification
College: College of Science
Issue: 2
Start Page: 19
End Page: 31