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.
Author supplied keywords
Cite
CITATION STYLE
Amendola, A., Becchi, A., Cavada, R., Cimatti, A., Griggio, A., Scaglione, G., … Tessi, M. (2020). A Model-Based Approach to the Design, Verification and Deployment of Railway Interlocking System. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12478 LNCS, pp. 240–254). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-61467-6_16
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
