Formally verified architectural patterns of hybrid systems using proof and refinement with Event-B - Archive ouverte HAL Access content directly
Journal Articles Science of Computer Programming Year : 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

(1, 2) , (1, 2) , (1, 2) , (1, 2)
1
2

Abstract

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
Origin : Files produced by the author(s)

Dates and versions

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

Identifiers

Cite

Guillaume Dupont, Yamine Ait-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⟩
138 View
39 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More