Constructing verifiable test oracles for a family of automatic train control systems

A common problem encountered in model-based testing is the construction of a system model with explicit traceability to the requirements. We present an approach for automatically generating a system model for an arbitrary railroad track layout. The model will be built as a system of communicating automata. The approach consists of compositional techniques that allow us to easily construct system models for each possible track layout and to verify that the model has the following safety function: The railroad network is divided into blocks. No more than one train shall be allowed to enter a block of the railroad network at the same time. The automata are first constructed on an abstract level and brought into their final form, an UPPAAL automaton system, using a sequence of refinements, again facilitating traceability to the requirements and verification of the safety functions.