author: Thijs ten Hoeve
title: Model Based Testing of a PLC Based Interlocking System
company: ProRail
keywords: mcrl2, interlockings, railways, testing, model based, PLC, test case generation
topics: Case studies and Applications , Testing
committee: Mariƫlle Stoelinga ,
Jaco van de Pol ,
Wendi Mennen
started: December 2011
end: November 2012
type: Master project (ProRail)


Interlocking systems control all wayside elements in a railway yard. These sys- tems are responsible for safe train operations and must prevent collisions and derailments from happening. It is absolutely essential that interlocking systems operate flawlessly, and as a result a lot of effort is put in their verification.

ProRail (the Dutch railway infrastructure manager) is developing a new type of interlocking system based on off-the-shelf PLC hardware, the PLC- Interlocking.

This report introduces a conformance testing methodology for PLC-Interlocking systems that is based around the JTorX test tool. The test method has been applied to the first instance of a PLC-Interlocking system, which is installed at the Santpoort Noord station.

To get an SUT that can be tested, the interlocking logic is integrated in a program that adds interfacing code and is then recompiled for a regular PC system. As a result, testing does not require access to the PLC hardware.

A number of test purpose models have been created to direct test case gen- eration. These test purpose models were implemented in Java, using a custom framework that creates an LTS representation of inputs and outputs and handles communication with JTorX

A partial specification model has been implemented in mCRL2. Because of the complexity of the requirements, and the limited available time, it was not possible to create a complete model.

The created test setup allows automated testing of the interlocking logic of PLC-Interlocking systems. The entire test setup can be run on a regular PC (if it is equipped with sufficient memory) and does not require PLC hardware. Of 73 automated test runs that were conducted, 36 ended with the observation of a failure. Four of these failures must be further investigated, but it seems likely that all failures were caused by faults in the model.

Creating a complete and correct model is the biggest obstacle to using this testing methodology more in the future.


Additional Resources

  1. The paper