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.
展开▼
