Refinement of Statemachines using Event B semantics

Colin Snook, Marina Waldén

Research output: Chapter in Book/Conference proceedingConference contributionScientificpeer-review

10 Citations (Scopus)


While refinement gives a formal underpinning to the development of dependable control systems, such models are difficult to communicate and reason about in a non-formal sense, particularly for validation by non-specialist industrial partners. Here we present a visualisation of, and guidance for, event B refinement using a specialisation of UML statemachines. Furthermore, we introduce design patterns and process rules
that are aimed at assisting in the software development process leading to correct refinements. The specialisation will be incorporated into the UML-B notation to be integrated with the Event B platform developed by the RODIN project.
Original languageEnglish
Title of host publicationB 2007: Formal Specification and Development in B
Subtitle of host publication7th International Conference of B Users, Besancon, France, January 7-19, 2007, Proceedings
ISBN (Print)978-3-540-68760-3
Publication statusPublished - 2007
MoE publication typeA4 Article in a conference publication
EventInternational Conference of B Users -
Duration: 7 Nov 2007 → …

Publication series

NameLecture Notes in Computer Science


ConferenceInternational Conference of B Users
Period07/11/07 → …


Dive into the research topics of 'Refinement of Statemachines using Event B semantics'. Together they form a unique fingerprint.

Cite this