Author(s)

A. Svendsen, B. Møller-Pedersen, Ø. Haugen, J. Endresen & E. Carlson

Abstract

The Train Control Language (TCL) is a domain-specific language that allows automation of the production of interlocking source code. From a graphical editor a model of a train station is created. This model can then be transformed to other representations, e.g. an interlocking table and functional blocks, keeping the representations internally consistent. Formal methods are mathematical techniques for precisely expressing a system, contributing to the reliability and robustness of the system through analysis. Traditionally, applying formal methods involves a high cost. This paper presents a formalization of TCL, including its behavior expressed in the constraint solving language Alloy. We show how analysis of station models can be performed automatically. Analysis, such as simulation of a station, searching for dangerous train movements and deadlocks, is used to illustrate the approach. Keywords: interlocking, domain specific language (DSL), model analysis, alloy, Train Control Language (TCL). 1 Introduction An interlocking system prevents dangerous train movement on a train station by giving a \“clear” signal to a train only if the requested route is safe. The interlocking system ensures that the route is safe by reading the status of the elements in the route (e.g. tracks, switches, signals) to see if they comply with the logic of the interlocking system. This logic is depicted by an interlocking table, and realized by the interlocking source code, in the form of functional

Keywords

interlocking, domain specific language (DSL), model analysis, alloy, Train Control Language (TCL)