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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
