Formally verified architectural patterns of hybrid systems using proof and refinement with Event-B - IRIT - Institut de Recherche en Informatique de Toulouse Accéder directement au contenu
Article Dans Une Revue Science of Computer Programming Année : 2022

Formally verified architectural patterns of hybrid systems using proof and refinement with Event-B

Patrons architecturaux de systèmes hybrides formellement vérifiés à l'aide de la preuve et du raffinement en Event-B

Résumé

Cyber-Physical Systems (CPSs) are multi-component systems that interact with the real world. Their heterogeneous nature makes them particularly difficult to model and prove. Our work proposes a framework allowing to design complex hybrid systems based on decomposition using formally verified architectural patterns. It relies on a proof and refinement-based, correct-by-construction approach with Event-B. In particular, the generic model developed in our previous work is used as a base for defining different patterns, for modelling different architectures of systems. Three architectural patterns are presented, corresponding to simple, centralised and distributed control: one controller controlling one plant, one controller controlling several plants and several controllers controlling several plants. The progressive development of the proposed patterns and their application to specific hybrid systems allows to prove the required safety properties by introducing invariants, decomposing and balancing the proof effort at every step of the development. An assessment of the proposed architectural patterns is undertaken: different designs of the same case study are used to demonstrate the feasibility, reliability and extensibility of our approach to model and designing different classes of controllers.
Fichier principal
Vignette du fichier
SCP_SI_ABZ2020_preprint (1).pdf (520.34 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03513847 , version 1 (18-01-2022)

Identifiants

Citer

Guillaume Dupont, Yamine Aït-Ameur, Neeraj Kumar Singh, Marc Pantel. Formally verified architectural patterns of hybrid systems using proof and refinement with Event-B. Science of Computer Programming, 2022, 216, pp.102765. ⟨10.1016/j.scico.2021.102765⟩. ⟨hal-03513847⟩
229 Consultations
81 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More