• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

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

Andrew Edmunds, Marina Waldén, Modelling ‘Operation-Calls’ in Event-B with Shared-Event Composition. In: Leila Ribeiro, Thierry Lecomte (Eds.), Formal Methods: Foundations and Applications, Lecture Notes in Computer Science 10090, 97–111, Springer, 2016.

http://dx.doi.org/10.1007/978-3-319-49815-7

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 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 process for creating library components, composing them, and for specifying new properties (involving the composed elements). We introduced Event-B component interfaces and propose to use a diagrammatic representation of component instances. However, in that approach, the communication 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.

BibTeX entry:

@INPROCEEDINGS{inpEdWa16b,
  title = {Modelling ‘Operation-Calls’ in Event-B with Shared-Event Composition},
  booktitle = {Formal Methods: Foundations and Applications},
  author = {Edmunds, Andrew and Waldén, Marina},
  volume = {10090},
  series = {Lecture Notes in Computer Science},
  editor = {Ribeiro, Leila and Lecomte, Thierry},
  publisher = {Springer},
  pages = {97–111},
  year = {2016},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Edit publication