Search

We demonstrate diagrammatic EventB formal modelling of a hybrid, 'fixed virtual block' approach to train movement control for the emerging ERTMS level 3. We perform a full refinement-based formal development and verification of the key 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 iUMLB for EventB. We suggest enhancements to the existing iUML-B method that would have benefitted this development. The component and control flow architectures of the application and its environment and interacting systems emerge through the layered refinement process.

We propose a general approach based on abstraction and refinement for constructing and analysing security protocols using formal specification and verification. We use class diagrams to specify conceptual system entities and their relationships. We use state-machines to model the protocol execution involving the entities' interactions. Features of our approach include specifying security principles as invariants of some abstract model of the overall system. The specification is then refined to introduce implementable mechanisms for the protocol. A gluing invariant specifies why the protocol achieves the security principle. Security breaches arise as violations of the gluing invariant. We make use of both theorem proving and model checking techniques to analyse our formal model, in particular, to explore the source and consequence of the security attack. To demonstrate the use of our approach we explore the mechanism of a security attack in a network protocol.

State machines are hierarchical automata that are widely used to structure complex behavioural specifications.We develop two notions of refinement of state machines, node refinement and edge refinement.We compare the two notions by means of examples and argue that, by adopting simple conventions, they can be combined into one method of refinement.In the combined method, node refinement can be used to develop architectural aspects of a modeland edge refinement to develop algorithmic aspects.The two notions of refinement are grounded in previous work. Event-B is used as the foundation for our refinement theory and UML-B state machine refinement influences the style of node refinement.Hence we propose a method with direct proof of state machine refinement avoiding the detour via Event-B that is needed by UML-B.