• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Refinement of Statemachines Using Event B Semantics

Colin Snook, Marina Waldén, Refinement of Statemachines Using Event B Semantics. In: Jacques Julliand, Olga Kouchnarenko (Eds.), B2007: Formal Specification and Development in B, 7th International Conference of B Users, Besancon, France, January 7-19, 2007, Proceedings, Lecture Notes in Computer Science 4355, 171–185, Springer Berlin / Heidelberg, 2007.

Abstract:

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.

BibTeX entry:

@INPROCEEDINGS{inpSnWa07a,
  title = {Refinement of Statemachines Using Event B Semantics},
  booktitle = {B2007: Formal Specification and Development in B, 7th International Conference of B Users, Besancon, France, January 7-19, 2007, Proceedings},
  author = {Snook, Colin and Waldén, Marina},
  volume = {4355},
  series = {Lecture Notes in Computer Science},
  editor = {Julliand, Jacques and Kouchnarenko, Olga},
  publisher = {Springer Berlin / Heidelberg},
  pages = {171–185},
  year = {2007},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Publication Forum rating of this publication: level 1

Edit publication