Formalization and validation of a subset of the European Train Control System