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

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.