Techniques for modelling and verifying railway interlockings

P. James, F. Moller, Hoang Nga Nguyen, M. Roggenbach, S. Schneider, H. Treharne

Research output: Contribution to journalArticle

23 Citations (Scopus)
21 Downloads (Pure)

Abstract

We describe a novel framework for modelling railway interlockings which has been developed in conjunction with railway engineers. The modelling language used is CSP||B. Beyond the modelling we present a variety of abstraction techniques which make the analysis of medium- to large-scale networks feasible. The paper notably introduces a covering technique that allows railway scheme plans to be decomposed into a set of smaller scheme plans. The finitisation and topological abstraction techniques are extended from previous work and are given formal foundations. All three techniques are applicable to other modelling frameworks besides CSP||B. Being able to apply abstractions and simplifications on the domain model before performing model checking is the key strength of our approach. We demonstrate the use of the framework on a real-life, medium-size scheme plan.
Original languageEnglish
Pages (from-to)685-711
JournalInternational Journal on Software Tools for Technology Transfer
Volume16
Issue number6
DOIs
Publication statusPublished - Nov 2014
Externally publishedYes

Keywords

  • Railway verification
  • CSP
  • B
  • Model checking
  • Safety

Fingerprint Dive into the research topics of 'Techniques for modelling and verifying railway interlockings'. Together they form a unique fingerprint.

  • Cite this