This paper presents an approach to systematically build Promela models with the aim of generating test cases within the system level testing process of railway control systems. The paper focuses on the encoding of the system model, of the aspects related to the representation of possible execution environments and their interaction with the system. The input for building a Promela model of the system under test is a state machine based specification. Indeed, state machines are one of the most common notations used in industrial settings to model critical systems and allow for easily obtaining the Promela model of the system by applying a well structured transformational approach; furthermore, state-based formalism are also highly recommended by CENELEC norms to model railway control systems. In our approach Dynamic State Machines (DSTMs) are used, a newly developed extension of hierarchical state machines which allow for modeling dynamic instantiation of processes. The approach is applied to a functionality of the Radio Block Centre, the vital core of the ERTM- S/ETCS Control System, in order to show the feasibility and effectiveness of the generation of the Promela model on a real system.

Modeling railway control systems in promela

MARRONE, Stefano;
2016

Abstract

This paper presents an approach to systematically build Promela models with the aim of generating test cases within the system level testing process of railway control systems. The paper focuses on the encoding of the system model, of the aspects related to the representation of possible execution environments and their interaction with the system. The input for building a Promela model of the system under test is a state machine based specification. Indeed, state machines are one of the most common notations used in industrial settings to model critical systems and allow for easily obtaining the Promela model of the system by applying a well structured transformational approach; furthermore, state-based formalism are also highly recommended by CENELEC norms to model railway control systems. In our approach Dynamic State Machines (DSTMs) are used, a newly developed extension of hierarchical state machines which allow for modeling dynamic instantiation of processes. The approach is applied to a functionality of the Radio Block Centre, the vital core of the ERTM- S/ETCS Control System, in order to show the feasibility and effectiveness of the generation of the Promela model on a real system.
2016
9783319295091
9783319295091
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/11591/365033
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 15
  • ???jsp.display-item.citation.isi??? 10
social impact