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.
|Titolo:||A Model-Based Approach to the Design, Verification and Deployment of Railway Interlocking System|
|Data di pubblicazione:||2020|
|Appare nelle tipologie:||4.1 Contributo in Atti di convegno|