Refinement of Statemachines using Hierarchical States, Choice Points and Joins

Colin Snook, Marina Walden

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


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 event B refinement using a specialisation of UML statemachines. The specialisation will be incorporated into the UML-B notation that
is being re-developed within the Rodin project to improve integration with the Event B platform, which is also being developed by the Rodin project.
Original languageEnglish
Title of host publicationProceedings of the EPSRC RefineNet workshop
Place of PublicationManchester
PublisherUniversity of Manchester
Publication statusPublished - 2005
MoE publication typeA4 Article in a conference publication


Dive into the research topics of 'Refinement of Statemachines using Hierarchical States, Choice Points and Joins'. Together they form a unique fingerprint.

Cite this