Refinement of Statemachines using Event B semantics

Colin Snook; Marina Walden

Refinement of Statemachines using Event B semantics

Information Technology

Research output: Chapter in Book/Conference proceeding › Conference contribution › Scientific › peer-review

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.

Original language	English
Title of host publication	Proceedings of the 7th International B Conference (B2007)
Publisher	Springer
Pages	171-185
Volume	4355
Publication status	Published - 2007
MoE publication type	A4 Article in a conference publication

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	4355

Cite this

@inproceedings{1514b028326c4f0ead2c4e468a557688,

title = "Refinement of Statemachines using Event B semantics",

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 rulesthat 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.",

author = "Colin Snook and Marina Walden",

year = "2007",

language = "English",

volume = "4355",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "171--185",

booktitle = "Proceedings of the 7th International B Conference (B2007)",

}

TY - GEN

T1 - Refinement of Statemachines using Event B semantics

AU - Snook, Colin

AU - Walden, Marina

PY - 2007

Y1 - 2007

N2 - 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 rulesthat 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.

AB - 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 rulesthat 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.

M3 - Conference contribution

VL - 4355

T3 - Lecture Notes in Computer Science

SP - 171

EP - 185

BT - Proceedings of the 7th International B Conference (B2007)

PB - Springer

ER -

Refinement of Statemachines using Event B semantics

Abstract

Publication series

Fingerprint

Cite this