Paper Info
Title
Modeling Railway Control Systems in Promela.
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 ERTMS/ETCS Control System, in order to show the feasibility and effectiveness of the generation of the Promela model on a real system.
Year
DOI
Venue
2015
10.1007/978-3-319-29510-7_7
Communications in Computer and Information Science
Keywords
Field
DocType
Model checking,Promela,SPIN,Dynamic state machine,CRYSTAL,Railway control systems,Test case generation
System under test,Notation,Model checking,Software engineering,Finite-state machine,Control engineering,Test case,Promela,Control system,Engineering,System model
Conference
Volume
ISSN
Citations 
596
1865-0929
7
PageRank 
References 
Authors
0.44
6
7
Name
Order
Citations
PageRank
Roberto Nardone110815.07
Ugo Gentile2366.52
Massimo Benerecetti328734.60
Adriano Peron438145.82
valeria vittorini533933.14
Stefano Marrone617425.49
Nicola Mazzocca767478.37