Modelling and Refining Hybrid Systems in Event-B and Rodin

Abstract. We outline an approach to modelling and reasoning about hybrid systems with the Event-B method supported by the Rodin toolset. The approach uses continuous functions over real intervals to model the evolution of continuous values over time. Nondeterministic interval events are used to specify how continuous variables evolve within an operating mode. Refinement is used to constrain the choice of continuous functions and to decompose a …