In this paper, we present Hybrid Event B, a formal language for modeling hybrid systems. Specifically, Hybrid Event B is an extension of Event B associating with differential dynamic logic. The main contribution of this paper is that we give the definition of a differential event in Hybrid Event B, which makes it possible using differential dynamic logic in modeling continuous dynamical systems and discrete dynamical systems. In addition, we show the proof obligations of each refinements on differential events, which supports the stepwise devel...
