Building correct hybrid systems using Event-B and sagemath: Illustration by the hybrid smart heating system case study - Institut Polytechnique de Paris
Conference Papers Year : 2022

Building correct hybrid systems using Event-B and sagemath: Illustration by the hybrid smart heating system case study

Abstract

Cyber-physical systems allow interactions with the physical world using a network of sensors and actuators. They also form basis of future technologies via engaging in innovating within many crucial fields: health, transport, smart grid, etc. Modeling cyber-physical systems requires handling the evolution of continuous measurements. Generally this evolution is repre-sented by ordinary differential equations where the unknown variable denotes a set of functions that depend on a single independent variable. The aim of our work is to propose a correct-by-construction formal approach, based on the refinement technique of the Event-B method, to model and verify such systems. However, Event-B does not handle the resolution of ordinary differential equations. To overcome this limit, we suggest to combine Event-B with the differential equation solver SageMath. This paper presents our approach by means of the hybrid smart heating system case study.
No file

Dates and versions

hal-03916803 , version 1 (31-12-2022)

Identifiers

Cite

Meryem Afendi, Amel Mammar, Régine Laleau. Building correct hybrid systems using Event-B and sagemath: Illustration by the hybrid smart heating system case study. 2022 26th International Conference on Engineering of Complex Computer Systems (ICECCS), Mar 2022, Hiroshima, Japan. ⟨10.1109/ICECCS54210.2022.00019⟩. ⟨hal-03916803⟩
34 View
0 Download

Altmetric

Share

More