-
Article
A method of refinement in UML-B
UML-B is a ‘UML-like’ graphical front-end for Event-B that provides support for object-oriented and state machine modelling concepts, which are not available in Event-B. In particular, UML-B includes class dia...
-
Article
Open AccessFormalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B
We demonstrate refinement-based formal development of the hybrid, ‘fixed virtual block’ approach to train movement control for the emerging European Rail Traffic Management System (ERTMS) level 3. Our approach us...
-
Article
Open AccessSystematic hierarchical analysis of requirements for critical systems
Safety and security are key considerations in the design of critical systems. Requirements analysis methods rely on the expertise and experience of human intervention to make critical judgements. While human j...
