Core Hybrid Event-B I: Single Hybrid Event-B machines

Richard Banach, Michael Butler, Shengchao Qin, Nitika Verma, Huibiao Zhu

Research output: Contribution to journalArticle

126 Downloads (Pure)

Abstract

Faced with the increasing need for correctly designed hybrid and cyber-physical systems today, the problem of including provision for continuously varying behaviour as well as the usual discrete changes of state is considered in the context of Event-B. An extension of Event-B called Hybrid Event-B is presented, that accommodates continuous behaviours (called pliant events) in between familiar discrete transitions (called mode events in this context). The continuous state change can be specif ed by a combination of indirect specif cation via ordinary differential equations, or direct specif cation via assignment of variables to values that depend on time, or indirect specif cation by demanding that behaviour obeys a time dependent predicate. The syntactic elements of the extension are discussed, and the semantics is described in terms of the properties of time dependent valuations of variables. Ref nement is examined in detail, with reference to the notion of ref nement inherited from discrete Event-B. A full suite of proof obligations is presented, covering all aspects of the new framework. A selection of examples and case studies is presented. A particular challenge —bearing in mind the desirability of conforming to existing intuitions about discrete Event-B, and the impact on tool support (as embodied in tools for discrete Event-B like Rodin)— is to design the whole framework so as to disturb as little as possible the existing structures for handling discrete Event-B.
Original languageEnglish
Pages (from-to)92-123
JournalScience of Computer Programming
Volume105
DOIs
Publication statusPublished - 2015

Fingerprint Dive into the research topics of 'Core Hybrid Event-B I: Single Hybrid Event-B machines'. Together they form a unique fingerprint.

  • Profiles

    Cite this