Core Hybrid Event-B II: Multiple cooperating Hybrid Event-B machines

Richard Banach, Michael Butler, Shengchao Qin, Huibiao Zhu

    Research output: Contribution to journalArticlepeer-review

    110 Downloads (Pure)


    Hybrid Event-B, initially introduced for single machines to add continuously varying behaviour to discrete change of state in Event-B, is extended to cater for multiple cooperating machines. Multiple machine working is mediated by INTERFACE and PROJECT constructs. The former encapsulates a set of variables, their invariants and initialisations, in a form that several machines can exploit simultaneously. The latter organises the set of cooperating machines and interfaces into a coherent system. Machine instantiation and composition via interfaces are discussed. Machine decomposition is explored in this framework. Multi-machine refinement is described. A hypergraph project architecture is proposed. Two small case studies, on power switching and on the European Train Control System (the latter treated earlier within the single machine formalism), illustrate these mechanisms. The semantics of interacting
    multi-machine systems is described, and proof obligations that ensure correctness are covered.
    Original languageEnglish
    Pages (from-to)1-35
    JournalScience of Computer Programming
    Early online date15 Mar 2017
    Publication statusPublished - 1 Jun 2017


    Dive into the research topics of 'Core Hybrid Event-B II: Multiple cooperating Hybrid Event-B machines'. Together they form a unique fingerprint.

    Cite this