Formalizing hybrid systems with Event-B and the Rodin Platform

This paper contains the development of hybrid systems with Event-B and the Rodin Platform. It follows the seminal approach introduced at the turn of the century in Action Systems. Many examples that have been entirely proved with the Rodin Platform illustrate our approach. We propose to complement the Event-B/Rodin Platform approach with the usage of Matlab, either to simulate examples with some correct as well as incorrect set of parameters, or to use the analytical power of Matlab to complement the usage of Event-B.