Dynamic state machines for formalizing railway control system specifications

activities regulated by international standards which explicitly recommend the usage of Finite State Machines (FSMs) to model the specification of the system under test. Despite the great number of work addressing the usage of FSMs and their extensions, actual model-driven verification processes still lacks concise and expressive enough notations, able to easily capture characteristic features of specific domains. This paper introduces DSTM4Rail, a hierarchical state machines formalism to be used in verification contexts, whose peculiarity mainly resides in the semantics of fork-and-join which allows dynamic (bounded) instantiation of machines (processes). The formalism described in this paper is industry driven, as it raises from real industrial needs in the context of an European project. Hence, the proposed semantics is motivated by illustrating concrete issues in modeling specific functionalities of the Radio Block Centre, the vital core of the ERTMS/ETCS Control System.