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.•Many examples that have been entirely proved with the Rodin Platform illustrate our approach.•Besides the formal development technique, we propose adding the usage of Matlab to verify systems.

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.