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.

Dynamic State Machines for Formalizing Railway Control System Specifications

NARDONE, ROBERTO;
2015-01-01

Abstract

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.
9783319175805
CRYSTAL; Dynamic instantiation; Metamodel; Model driven; Railway control system; State machine; System testing; Computer Science (all)
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.12318/47266
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 16
  • ???jsp.display-item.citation.isi??? 12
social impact