Abstract
We demonstrate diagrammatic Event-B formal modelling of a hybrid, ‘fixed virtual block’ approach to train movement control for the emerging European Rail Traffic Management System (ERTMS) level 3. We perform a refinement-based formal development and verification of the no-collision safety requirement. The development reveals limitations in the specification and identifies assumptions on the environment. We reflect on our team-based approach to finding useful modelling abstractions and demonstrate a systematic modelling method using the UML-like state and class diagrams of iUML-B. We suggest enhancements to the existing iUML-B method that would have benefitted this development.
Cite
CITATION STYLE
Dghaym, D., Poppleton, M., & Snook, C. (2018). Diagram-led formal modelling using iUML-B for hybrid ERTMS level 3. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10817 LNCS, pp. 338–352). Springer Verlag. https://doi.org/10.1007/978-3-319-91271-4_23
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
