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) |
Abstract
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.