Skip to Main content Skip to Navigation
New interface
Journal articles

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

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.
Document type :
Journal articles
Complete list of metadata
Contributor : Guillaume DUPONT Connect in order to contact the contributor
Submitted on : Tuesday, January 18, 2022 - 3:52:19 PM
Last modification on : Monday, July 4, 2022 - 9:59:20 AM


SCP_SI_ABZ2020_preprint (1).pd...
Files produced by the author(s)



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⟩



Record views


Files downloads