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

Becchi, Anna;Cavada, Roberto;Cimatti, Alessandro;Griggio, Alberto;Susi, Angelo;Tacchella, Alberto;
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
978-3-030-61466-9
978-3-030-61467-6
File in questo prodotto:
File Dimensione Formato  
main.pdf

non disponibili

Tipologia: Documento in Pre-print
Licenza: NON PUBBLICO - Accesso privato/ristretto
Dimensione 688.25 kB
Formato Adobe PDF
688.25 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/325572
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact