We present NORMA, a tool for the modeling and analysis of Relay-based Railways Interlocking Systems (RRIS). NORMA is the result of a research project funded by the Italian Railway Network, to support the reverse engineering and migration to computer-based technology of legacy RRIS. The frontend fully supports the graphical modeling of Italian RRIS, with a palette of over two hundred basic components, stubs to abstract RRIS subcircuits, and requirements in terms of formal properties. The internal component based representation is translated into highly optimized Timed NuXmv models, and supports various syntactic and semantic checks based on formal verification, simulation and test case generation. NORMA is experimentally evaluated, demonstrating the practical support for the modelers, and the effectiveness of the underlying optimizations.
NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems / Amendola, Arturo; Becchi, Anna; Cavada, Roberto; Cimatti, Alessandro; Ferrando, Andrea; Pilati, Lorenzo; Scaglione, Giuseppe; Tacchella, Alberto; Zamboni, Marco. - 13243:(2022), pp. 125-142. (Intervento presentato al convegno TACAS tenutosi a Munich, Germany nel 2nd April-7th April 2022) [10.1007/978-3-030-99524-9_7].
NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems
Anna Becchi;Roberto Cavada;Alessandro Cimatti;Alberto Tacchella;
2022-01-01
Abstract
We present NORMA, a tool for the modeling and analysis of Relay-based Railways Interlocking Systems (RRIS). NORMA is the result of a research project funded by the Italian Railway Network, to support the reverse engineering and migration to computer-based technology of legacy RRIS. The frontend fully supports the graphical modeling of Italian RRIS, with a palette of over two hundred basic components, stubs to abstract RRIS subcircuits, and requirements in terms of formal properties. The internal component based representation is translated into highly optimized Timed NuXmv models, and supports various syntactic and semantic checks based on formal verification, simulation and test case generation. NORMA is experimentally evaluated, demonstrating the practical support for the modelers, and the effectiveness of the underlying optimizations.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
