Modelling ‘Operation-Calls’ in Event-B with Shared-Event Composition

A4 Konferenspublikationer

Interna författare/redaktörer

Publikationens författare: Andrew Edmunds, Marina Waldén
Redaktörer: Ribeiro L, Lecomte T
Förläggare: Springer
Publiceringsår: 2016
Förläggare: Springer
Moderpublikationens namn: Formal Methods: Foundations and Applications. 19th Brazilian Symposium, SBMF 2016, Natal, Brazil, November 23-25, 2016, Proceedings
Seriens namn: Lecture Notes in Computer Science
Volym: 10090
Artikelns första sida, sidnummer: 97
Artikelns sista sida, sidnummer: 111
ISBN: 978-3-319-49814-0
eISBN: 978-3-319-49815-7
ISSN: 0302-9743


Efficient reuse is a goal of many software engineering strate- gies 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 previous work, we outlined a component-based reuse methodology for Event-B. The methodology provides a means for bottom-up scalability, and can also be used with the existing top-down approach. We developed a pro- cess for creating library components, composing them, and for specify- ing new properties (involving the composed elements). We introduced Event-B component interfaces and propose to use a diagrammatic repre- sentation of component instances. However, in that approach, the com- munication between components is modelled in an abstract manner. In this paper, we describe a more concrete specification approach which includes interfaces with ‘callable’ interface events. These events model operations, and additional syntactic constructs model their invocation.

Senast uppdaterad 2020-03-04 vid 06:16