Skip to Main content Skip to Navigation
Conference papers

An Event-B Based Generic Framework for Hybrid Systems Formal Modelling

Abstract : Designing hybrid systems requires the handling of discrete and continuous behaviours. The formal verification of such systems revolves around the use of heavy mathematical features, and related proofs. This paper presents a generic and reusable framework with different patterns, aimed at easing the design and verification of hybrid systems. It relies on refinement and proofs using Event-B, and defines an easily extensible set of generic patterns in the form of theories and models that are proved once and for all. The model of any specific hybrid system is then produced by instantiating the corresponding patterns. The paper illustrates the use of this framework by proposing to realise a well-known case study of the inverted pendulum, which design uses the approximation pattern formally defined and verified in Event-B.
Document type :
Conference papers
Complete list of metadata
Contributor : Guillaume Dupont Connect in order to contact the contributor
Submitted on : Monday, June 21, 2021 - 12:22:08 PM
Last modification on : Wednesday, November 3, 2021 - 6:52:43 AM
Long-term archiving on: : Wednesday, September 22, 2021 - 6:30:39 PM


An Event-B Based Generic Frame...
Publisher files allowed on an open archive



Guillaume Dupont, Yamine Aït-Ameur, Marc Pantel, Neeraj Kumar Singh. An Event-B Based Generic Framework for Hybrid Systems Formal Modelling. 16th International Conference on Integrated Formal Methods (IFM 2020), Nov 2020, Lugano (virtual), Switzerland. pp.82-102, ⟨10.1007/978-3-030-63461-2_5⟩. ⟨hal-03265788⟩



Record views


Files downloads