Handling Continuous Functions in Hybrid Systems Reconfigurations: A Formal Event-B Development

ISSN: 0302-9743 ; ISBN: 978-3-319-33599-5International audienceThis paper presents a substitution mechanism for systems having a continuous behavior. It shall preserve the safety property stating that the output of both systems remain in a safety envelope. The whole approach is formalized using Event-B, and relies on the Rodin tools and a theory of Reals provided by the Rodin Theory Plug-in to check the internal consistency with respect to safety properties, invariants and events