Abstract: “This paper studies the abilities of the formal model of a Timed Extended Finite State Machine (TEFSM) to represent the safety properties of the European Train Control System (ETCS). The model is based on Finite State Machines augmented with continuous variables and time information, which allows representing the basic functioning of the units in this real-time system. In order to represent temporal requirements, timeouts are used for modeling some aspects of the (internal) critical behavior of the train control system. The model abilities to represent safety properties are evaluated using different testing scenarios for model implementations in IF, XML and JAVA languages. Tests are automatically generated using the tool TestGen-IF where corresponding safety properties are specified as test objectives. Based on the obtained experimental results the advantages and disadvantages of a developed model are briefly discussed.”

Keywords: European Train Control System, formal model, Timed Extended FSM, active testing, safety properties.