Abstract: “This paper presents test generation scenarios for a train implementation based on the requirements for European Train Control System (ETCS). The formal model used for the test derivation is the model of a Timed Extended Finite State Machine (TEFSM) given in the IF language. This language allows to capture some important properties such as safety properties that should be checked for train implementations represented as corresponding test objectives. The tool TestGen-IF is then used for automatic generation of test cases.”

Keywords: Timed Extended FSM, ETCS, IF language, TestGen-IF tool. I.