Test Case Generation for a Level Crossing Controller

Abstract

Formal methods (FM) can be used for the precise specification, property-ensuring development and exhaustive property verification of systems. Thus they are especially suited for highly safety or mission critical applications. Railway signaling systems clearly belong to these applications, and there are indeed several industrial projects where FM have been successfully applied; especially to core interlocking and communication-based train control (CBTC) systems. But despite their potential, FM are not very wide-spread in the sector. Work Package 5 of the X2Rail-2 project seeks to foster the use of FM in railway signaling by providing an introduction and overview of formal methods and demonstrating their use and benefit. For the latter, four different formal and one classical development methods are applied by different project partners to a level crossing (LX) controller specified by the Swedish railway infrastructure manager Trafikverket. For all of these developments, the safety properties from the LX specification are planned to be formally verified afterwards using the High Level Language (HLL). Since that means proving them exhaustively, they are of less interest for testing.

However, there are further non-safety functional requirements in the specification which remain for testing. The extended abstract at hand reports on an automatic test case generation (TCG) approach of a test suite testing these requirements. In fact, this approach is based on formal methods as well, since the test case generator applies symbolic execution and theorem solving techniques: given a behavioral model of the system under test (SUT), the former method finds feasible paths through the model, while the latter completes the test case by determining suitable test data. This way, the test design task is partly automated, ensures a structural coverage of the model and the modeling process usually leads to a high test suite quality. The different LX controller implementations are tested as black box systems, each one with the same generated test cases. In order to simplify the integration of the different implementations with the test environment, a common test interface has been drawn up.