Anzeige
Erschienen in:
2016 | OriginalPaper | Buchkapitel
Modelling ‘Operation-Calls’ in Event-B with Shared-Event Composition
verfasst von : Andrew Edmunds, Marina Waldén
Erschienen in: Formal Methods: Foundations and Applications
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.