An Event-B Based Generic Framework for Hybrid Systems Formal Modelling - Assistance à la Certification d’Applications DIstribuées et Embarquées Accéder directement au contenu
Communication Dans Un Congrès Année : 2020

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

Résumé

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.
Fichier principal
Vignette du fichier
An Event-B Based Generic Framework for Hybrid Systems Formal Modelling.pdf (3.05 Mo) Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte

Dates et versions

hal-03265788 , version 1 (21-06-2021)

Identifiants

Citer

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⟩
65 Consultations
94 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More