Refinement of Statemachines using Event B semantics

Colin Snook; Marina Waldén

doi:10.1007/11955757_15

Refinement of Statemachines using Event B semantics

Colin Snook, Marina Waldén

Information Technology

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

11 Citations (Scopus)

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	B 2007: Formal Specification and Development in B
Subtitle of host publication	7th International Conference of B Users, Besancon, France, January 7-19, 2007, Proceedings
Publisher	Springer
Pages	171-185
ISBN (Print)	978-3-540-68760-3
DOIs	https://doi.org/10.1007/11955757_15
Publication status	Published - 2007
MoE publication type	A4 Article in a conference publication
Event	International Conference of B Users - Duration: 7 Nov 2007 → …

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	4355

Conference

Conference	International Conference of B Users
Period	07/11/07 → …

Access to Document

10.1007/11955757_15

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 Wald{\'e}n",

year = "2007",

doi = "10.1007/11955757_15",

language = "English",

isbn = "978-3-540-68760-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "171--185",

booktitle = "B 2007: Formal Specification and Development in B",

note = "International Conference of B Users ; Conference date: 07-11-2007",

}

Snook, C & Waldén, M 2007, Refinement of Statemachines using Event B semantics. in B 2007: Formal Specification and Development in B: 7th International Conference of B Users, Besancon, France, January 7-19, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4355, Springer, pp. 171-185, International Conference of B Users, 07/11/07. https://doi.org/10.1007/11955757_15

Refinement of Statemachines using Event B semantics. / Snook, Colin; Waldén, Marina.
B 2007: Formal Specification and Development in B: 7th International Conference of B Users, Besancon, France, January 7-19, 2007, Proceedings. Springer, 2007. p. 171-185 (Lecture Notes in Computer Science; Vol. 4355).

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

TY - GEN

T1 - Refinement of Statemachines using Event B semantics

AU - Snook, Colin

AU - Waldén, 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.

U2 - 10.1007/11955757_15

DO - 10.1007/11955757_15

M3 - Published conference proceeding

SN - 978-3-540-68760-3

T3 - Lecture Notes in Computer Science

SP - 171

EP - 185

BT - B 2007: Formal Specification and Development in B

PB - Springer

T2 - International Conference of B Users

Y2 - 7 November 2007

ER -

Refinement of Statemachines using Event B semantics

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this