This paper describes a model-based flow for the development of Interlocking Systems. The flow starts from a set of specifications in Controlled Natural Language (CNL), that are close to the jargon adopted in by domain experts, but fully formal. From the CNL, a complete SysML specification is extracted, leveraging various forms of diagrams, and enabling automated code generation. Several formal verification methods are supported. A complementary part of the flow supports the extraction of formal properties from legacy Interlocking Systems designed as Relay circuits. The flow is implemented in a comprehensive toolset, and is currently used by railway experts.

A Model-Based Approach to the Design, Verification and Deployment of Railway Interlocking System / Amendola, Arturo; Becchi, Anna; Cavada, Roberto; Cimatti, Alessandro; Griggio, Alberto; Scaglione, Giuseppe; Susi, Angelo; Tacchella, Alberto; Tessi, Matteo. - 12478:(2020), pp. 240-254. (Intervento presentato al convegno 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020 tenutosi a Rhodes, Greece nel October 20-30, 2020) [10.1007/978-3-030-61467-6_16].

A Model-Based Approach to the Design, Verification and Deployment of Railway Interlocking System

Becchi, Anna;Cavada, Roberto;Cimatti, Alessandro;Griggio, Alberto;Scaglione, Giuseppe;Susi, Angelo;
2020-01-01

Abstract

This paper describes a model-based flow for the development of Interlocking Systems. The flow starts from a set of specifications in Controlled Natural Language (CNL), that are close to the jargon adopted in by domain experts, but fully formal. From the CNL, a complete SysML specification is extracted, leveraging various forms of diagrams, and enabling automated code generation. Several formal verification methods are supported. A complementary part of the flow supports the extraction of formal properties from legacy Interlocking Systems designed as Relay circuits. The flow is implemented in a comprehensive toolset, and is currently used by railway experts.
2020
Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020
Cham, Switzerland
Springer
978-3-030-61466-9
Amendola, Arturo; Becchi, Anna; Cavada, Roberto; Cimatti, Alessandro; Griggio, Alberto; Scaglione, Giuseppe; Susi, Angelo; Tacchella, Alberto; Tessi, ...espandi
A Model-Based Approach to the Design, Verification and Deployment of Railway Interlocking System / Amendola, Arturo; Becchi, Anna; Cavada, Roberto; Cimatti, Alessandro; Griggio, Alberto; Scaglione, Giuseppe; Susi, Angelo; Tacchella, Alberto; Tessi, Matteo. - 12478:(2020), pp. 240-254. (Intervento presentato al convegno 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020 tenutosi a Rhodes, Greece nel October 20-30, 2020) [10.1007/978-3-030-61467-6_16].
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/11572/342979
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? ND
social impact