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

https://hal.archives-ouvertes.fr/hal-03265788
Contributor : Guillaume Dupont Connect in order to contact the contributor
Submitted on : Monday, June 21, 2021 - 12:22:08 PM
Last modification on : Tuesday, October 19, 2021 - 2:23:30 PM
Long-term archiving on: : Wednesday, September 22, 2021 - 6:30:39 PM

File

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

Identifiers

Citation

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⟩

Share

Metrics

Record views

41

Files downloads

46