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

5 Citations (Scopus)
106 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
Number of pages35
JournalScience of Computer Programming
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