Building Correct Hybrid Systems using Event-B and Sagemath: Illustration by the Hybrid Smart Heating System Case Study

Meryem Afendi; Amel Mammar; Regine Laleau

doi:10.1109/ICECCS54210.2022.00019

Building Correct Hybrid Systems using Event-B and Sagemath: Illustration by the Hybrid Smart Heating System Case Study

Meryem Afendi
, Amel Mammar
, Regine Laleau

Université de PARIS XII

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Proceedings - 2022 26th International Conference on Engineering of Complex Computer Systems, ICECCS 2022
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	91-96
Number of pages	6
ISBN (Electronic)	9781665401623
DOIs	https://doi.org/10.1109/ICECCS54210.2022.00019
Publication status	Published - 1 Jan 2022
Event	26th International Conference on Engineering of Complex Computer Systems, ICECCS 2022 - Hiroshima, Japan Duration: 26 Mar 2022 → 30 Mar 2022

Publication series

Name	Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS
Volume	2022-March
ISSN (Print)	2770-8527
ISSN (Electronic)	2770-8535

Conference

Conference	26th International Conference on Engineering of Complex Computer Systems, ICECCS 2022
Country/Territory	Japan
City	Hiroshima
Period	26/03/22 → 30/03/22

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

SDG 7 Affordable and Clean Energy

Keywords

Cyber-Physical System
Differential Equation Solver
Event-B
Hybrid Smart Heating System
Ordinary Differential Equation
Sagemath

Access to Document

10.1109/ICECCS54210.2022.00019

Cite this

Afendi, M., Mammar, A., & Laleau, R. (2022). Building Correct Hybrid Systems using Event-B and Sagemath: Illustration by the Hybrid Smart Heating System Case Study. In Proceedings - 2022 26th International Conference on Engineering of Complex Computer Systems, ICECCS 2022 (pp. 91-96). (Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS; Vol. 2022-March). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/ICECCS54210.2022.00019

Afendi, Meryem ; Mammar, Amel ; Laleau, Regine. / Building Correct Hybrid Systems using Event-B and Sagemath : Illustration by the Hybrid Smart Heating System Case Study. Proceedings - 2022 26th International Conference on Engineering of Complex Computer Systems, ICECCS 2022. Institute of Electrical and Electronics Engineers Inc., 2022. pp. 91-96 (Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS).

@inproceedings{6d9feb23cff14344bd456308e0762e09,

title = "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.",

keywords = "Cyber-Physical System, Differential Equation Solver, Event-B, Hybrid Smart Heating System, Ordinary Differential Equation, Sagemath",

author = "Meryem Afendi and Amel Mammar and Regine Laleau",

note = "Publisher Copyright: {\textcopyright} 2022 IEEE.; 26th International Conference on Engineering of Complex Computer Systems, ICECCS 2022 ; Conference date: 26-03-2022 Through 30-03-2022",

year = "2022",

month = jan,

day = "1",

doi = "10.1109/ICECCS54210.2022.00019",

language = "English",

series = "Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "91--96",

booktitle = "Proceedings - 2022 26th International Conference on Engineering of Complex Computer Systems, ICECCS 2022",

}

Afendi, M, Mammar, A & Laleau, R 2022, Building Correct Hybrid Systems using Event-B and Sagemath: Illustration by the Hybrid Smart Heating System Case Study. in Proceedings - 2022 26th International Conference on Engineering of Complex Computer Systems, ICECCS 2022. Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS, vol. 2022-March, Institute of Electrical and Electronics Engineers Inc., pp. 91-96, 26th International Conference on Engineering of Complex Computer Systems, ICECCS 2022, Hiroshima, Japan, 26/03/22. https://doi.org/10.1109/ICECCS54210.2022.00019

Building Correct Hybrid Systems using Event-B and Sagemath: Illustration by the Hybrid Smart Heating System Case Study. / Afendi, Meryem; Mammar, Amel; Laleau, Regine.
Proceedings - 2022 26th International Conference on Engineering of Complex Computer Systems, ICECCS 2022. Institute of Electrical and Electronics Engineers Inc., 2022. p. 91-96 (Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS; Vol. 2022-March).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Building Correct Hybrid Systems using Event-B and Sagemath

T2 - 26th International Conference on Engineering of Complex Computer Systems, ICECCS 2022

AU - Afendi, Meryem

AU - Mammar, Amel

AU - Laleau, Regine

PY - 2022/1/1

Y1 - 2022/1/1

N2 - 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.

AB - 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.

KW - Cyber-Physical System

KW - Differential Equation Solver

KW - Event-B

KW - Hybrid Smart Heating System

KW - Ordinary Differential Equation

KW - Sagemath

U2 - 10.1109/ICECCS54210.2022.00019

DO - 10.1109/ICECCS54210.2022.00019

M3 - Conference contribution

AN - SCOPUS:85130090823

T3 - Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS

SP - 91

EP - 96

BT - Proceedings - 2022 26th International Conference on Engineering of Complex Computer Systems, ICECCS 2022

PB - Institute of Electrical and Electronics Engineers Inc.

Y2 - 26 March 2022 through 30 March 2022

ER -

Afendi M, Mammar A, Laleau R. Building Correct Hybrid Systems using Event-B and Sagemath: Illustration by the Hybrid Smart Heating System Case Study. In Proceedings - 2022 26th International Conference on Engineering of Complex Computer Systems, ICECCS 2022. Institute of Electrical and Electronics Engineers Inc. 2022. p. 91-96. (Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS). doi: 10.1109/ICECCS54210.2022.00019

Building Correct Hybrid Systems using Event-B and Sagemath: Illustration by the Hybrid Smart Heating System Case Study

Abstract

Publication series

Conference

UN SDGs

Keywords

Access to Document

Fingerprint

Cite this