On Component-Based Reuse for Event-B

Andrew Edmunds; Colin Snook; Marina Walden

doi:10.1007/978-3-319-33600-8_9

On Component-Based Reuse for Event-B

Andrew Edmunds, Colin Snook, Marina Walden

Information Technology

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

2 Citations (Scopus)

Abstract

Efficient reuse is a goal of many software engineering strategies and is useful in the safety-critical domain where formal development is required. Event-B can be used to develop safety-critical systems, but could be improved by a component-based reuse strategy. In this paper, we outline a component-based reuse methodology for Event-B. It provides a means for bottom-up scalability, and can also be used with the existing top-down approach. We describe the process of creating library components, their composition, and specification of new properties (involving the composed elements). We introduce Event- B component interfaces and propose to use a diagrammatic representation of component instances (based on iUML-B) which can be used to describe the relationships between the composed elements. We also discuss the specification of communication flow across component boundaries and describe the additional proof obligations that are required.

Original language	Undefined/Unknown
Title of host publication	Abstract State Machines, Alloy, B, TLA, VDM, and Z. 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings
Editors	M Butler, K Schewe, A Mashkoor, M Biro
Publisher	Springer
Pages	151–166
ISBN (Electronic)	978-3-319-33600-8
ISBN (Print)	978-3-319-33599-5
DOIs	https://doi.org/10.1007/978-3-319-33600-8_9
Publication status	Published - 2016
MoE publication type	A4 Article in a conference publication
Event	ABZ - ABZ 2016 Duration: 23 May 2016 → 27 May 2016

Conference

Conference	ABZ
Period	23/05/16 → 27/05/16

Access to Document

10.1007/978-3-319-33600-8_9

ADVICeS: Adaptive Integrated Formal Design of Safety-Critical Systems (Academy of Finland)
Walden, M., Olszewska, M., Edmunds, A., Ostroumov, S., Petre, L., Boström, P. & Neovius, M.
01/09/13 → 31/08/17
Project: Research Council of Finland/Other Research Councils

Cite this

@inproceedings{c81e25ee55be41b69dc3778c1834b81a,

title = "On Component-Based Reuse for Event-B",

abstract = "Efficient reuse is a goal of many software engineering strategies and is useful in the safety-critical domain where formal development is required. Event-B can be used to develop safety-critical systems, but could be improved by a component-based reuse strategy. In this paper, we outline a component-based reuse methodology for Event-B. It provides a means for bottom-up scalability, and can also be used with the existing top-down approach. We describe the process of creating library components, their composition, and specification of new properties (involving the composed elements). We introduce Event- B component interfaces and propose to use a diagrammatic representation of component instances (based on iUML-B) which can be used to describe the relationships between the composed elements. We also discuss the specification of communication flow across component boundaries and describe the additional proof obligations that are required. ",

author = "Andrew Edmunds and Colin Snook and Marina Walden",

year = "2016",

doi = "10.1007/978-3-319-33600-8_9",

language = "Odefinierat/ok{\"a}nt",

isbn = "978-3-319-33599-5",

pages = "151–166",

editor = "M Butler and K Schewe and A Mashkoor and M Biro",

booktitle = "Abstract State Machines, Alloy, B, TLA, VDM, and Z. 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings",

publisher = "Springer",

note = "ABZ ; Conference date: 23-05-2016 Through 27-05-2016",

}

On Component-Based Reuse for Event-B. / Edmunds, Andrew; Snook, Colin; Walden, Marina.
Abstract State Machines, Alloy, B, TLA, VDM, and Z. 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings. ed. / M Butler; K Schewe; A Mashkoor; M Biro. Springer, 2016. p. 151–166.

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

TY - GEN

T1 - On Component-Based Reuse for Event-B

AU - Edmunds, Andrew

AU - Snook, Colin

AU - Walden, Marina

PY - 2016

Y1 - 2016

N2 - Efficient reuse is a goal of many software engineering strategies and is useful in the safety-critical domain where formal development is required. Event-B can be used to develop safety-critical systems, but could be improved by a component-based reuse strategy. In this paper, we outline a component-based reuse methodology for Event-B. It provides a means for bottom-up scalability, and can also be used with the existing top-down approach. We describe the process of creating library components, their composition, and specification of new properties (involving the composed elements). We introduce Event- B component interfaces and propose to use a diagrammatic representation of component instances (based on iUML-B) which can be used to describe the relationships between the composed elements. We also discuss the specification of communication flow across component boundaries and describe the additional proof obligations that are required.

AB - Efficient reuse is a goal of many software engineering strategies and is useful in the safety-critical domain where formal development is required. Event-B can be used to develop safety-critical systems, but could be improved by a component-based reuse strategy. In this paper, we outline a component-based reuse methodology for Event-B. It provides a means for bottom-up scalability, and can also be used with the existing top-down approach. We describe the process of creating library components, their composition, and specification of new properties (involving the composed elements). We introduce Event- B component interfaces and propose to use a diagrammatic representation of component instances (based on iUML-B) which can be used to describe the relationships between the composed elements. We also discuss the specification of communication flow across component boundaries and describe the additional proof obligations that are required.

U2 - 10.1007/978-3-319-33600-8_9

DO - 10.1007/978-3-319-33600-8_9

M3 - Konferensbidrag

SN - 978-3-319-33599-5

SP - 151

EP - 166

BT - Abstract State Machines, Alloy, B, TLA, VDM, and Z. 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings

A2 - Butler, M

A2 - Schewe, K

A2 - Mashkoor, A

A2 - Biro, M

PB - Springer

T2 - ABZ

Y2 - 23 May 2016 through 27 May 2016

ER -

On Component-Based Reuse for Event-B

Abstract

Conference

Access to Document

Projects

ADVICeS: Adaptive Integrated Formal Design of Safety-Critical Systems (Academy of Finland)

Cite this