Verification and Validation of railway controllers is the most critical and time-consuming phase in a system development life-cycle. It is regulated by international standards, which explicitly recommend the usage of state machines to model the specification of the system under test. Despite the great deal of works addressing the usage of state machines and their extensions, model-based verification and validation processes still lack concise and expressive-enough notations able to easily capture peculiar features of the specific domain of multi-process control systems, on which proper tool chains can be implemented in order to realize effective and automated environments. This paper introduces a novel class of hierarchical state machines, called Dynamic STate Machines (DSTMs), and proposes an approach for modelling and validating railway control systems, based on the new specification language. Key features of DSTM are recursive execution, parallelism, parameter passing, abortion transition, and communication through global variables and channels, but its main peculiarity resides in the semantics of fork and join operators which allows for dynamic instantiation of machines (processes). The formal semantics of DSTM allows for the definition of verification and validation methodologies supported by automated tools. The paper also describes how DSTM specifications may be mapped to Promela models in order to achieve automated generation of test cases by model checking and Spin. The work presented in this paper was carried out in the context of an European project and is strongly driven by the industrial necessity of tackling issues concerning the automation of functional system-level testing of modern railway signalling systems. Hence, the language and the proposed approach are illustrated and motivated by applying them to a specific functionality of the Radio Block Centre, the vital core of the ERTMS/ETCS Control System.

Dynamic state machines for modelling railway control systems

NARDONE, ROBERTO
;
2017-01-01

Abstract

Verification and Validation of railway controllers is the most critical and time-consuming phase in a system development life-cycle. It is regulated by international standards, which explicitly recommend the usage of state machines to model the specification of the system under test. Despite the great deal of works addressing the usage of state machines and their extensions, model-based verification and validation processes still lack concise and expressive-enough notations able to easily capture peculiar features of the specific domain of multi-process control systems, on which proper tool chains can be implemented in order to realize effective and automated environments. This paper introduces a novel class of hierarchical state machines, called Dynamic STate Machines (DSTMs), and proposes an approach for modelling and validating railway control systems, based on the new specification language. Key features of DSTM are recursive execution, parallelism, parameter passing, abortion transition, and communication through global variables and channels, but its main peculiarity resides in the semantics of fork and join operators which allows for dynamic instantiation of machines (processes). The formal semantics of DSTM allows for the definition of verification and validation methodologies supported by automated tools. The paper also describes how DSTM specifications may be mapped to Promela models in order to achieve automated generation of test cases by model checking and Spin. The work presented in this paper was carried out in the context of an European project and is strongly driven by the industrial necessity of tackling issues concerning the automation of functional system-level testing of modern railway signalling systems. Hence, the language and the proposed approach are illustrated and motivated by applying them to a specific functionality of the Radio Block Centre, the vital core of the ERTMS/ETCS Control System.
Control system, Dynamic STate machines, ERTMS/ETCS, Promela model, Verification and validation
File in questo prodotto:
File Dimensione Formato  
Benerecetti_2017_j.scico_Dynamic_Editor.pdf

non disponibili

Tipologia: Versione Editoriale (PDF)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 2.52 MB
Formato Adobe PDF
2.52 MB Adobe PDF   Visualizza/Apri   Richiedi una copia
Benerecetti_2017_j.scico_Dynamic_Pre.pdf

accesso aperto

Descrizione: Versione PRE-PRINT
Tipologia: Altro materiale allegato
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 4.48 MB
Formato Adobe PDF
4.48 MB Adobe PDF Visualizza/Apri

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/47286
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 14
  • ???jsp.display-item.citation.isi??? 10
social impact