Refinement of Statemachines using Event B semantics

Colin Snook; Marina Waldén

doi:10.1007/11955757_15

Refinement of Statemachines using Event B semantics

Informaatioteknologia

Tutkimustuotos: Artikkeli kirjassa/raportissa/konferenssijulkaisussa › Konferenssiartikkeli › Tieteellinen › vertaisarvioitu

12 Sitaatiot (Scopus)

Abstrakti

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.

Alkuperäiskieli	Englanti
Otsikko	B 2007: Formal Specification and Development in B
Alaotsikko	7th International Conference of B Users, Besancon, France, January 7-19, 2007, Proceedings
Kustantaja	Springer
Sivut	171-185
ISBN (painettu)	978-3-540-68760-3
DOI - pysyväislinkit	https://doi.org/10.1007/11955757_15
Tila	Julkaistu - 2007
OKM-julkaisutyyppi	A4 Artikkeli konferenssijulkaisuussa
Tapahtuma	International Conference of B Users - Kesto: 7 marrask. 2007 → …

Julkaisusarja

Nimi	Lecture Notes in Computer Science
Kustantaja	Springer
Vuosikerta	4355

Konferenssi

Konferenssi	International Conference of B Users
Ajanjakso	07/11/07 → …

Pääsy asiakirjaan

10.1007/11955757_15

Viittausmuodot

@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. julkaisussa 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, Vuosikerta 4355, Springer, Sivut 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. s. 171-185 (Lecture Notes in Computer Science; Vuosikerta 4355).

Tutkimustuotos: Artikkeli kirjassa/raportissa/konferenssijulkaisussa › Konferenssiartikkeli › Tieteellinen › vertaisarvioitu

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 - Conference contribution

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

Abstrakti

Julkaisusarja

Konferenssi

Pääsy asiakirjaan

Sormenjälki

Viittausmuodot