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

Anna Becchi
;
Roberto Cavada
;
Alessandro Cimatti
;
Andrea Ferrando;Lorenzo Pilati;Alberto Tacchella;Marco Zamboni
2022

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.
978-3-030-99523-2
978-3-030-99524-9
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/11582/333667
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact