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

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

Résumé

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.

langue originale	Anglais
titre	Proceedings - 2022 26th International Conference on Engineering of Complex Computer Systems, ICECCS 2022
Editeur	Institute of Electrical and Electronics Engineers Inc.
Pages	91-96
Nombre de pages	6
ISBN (Electronique)	9781665401623
Les DOIs	https://doi.org/10.1109/ICECCS54210.2022.00019
état	Publié - 1 janv. 2022
Evénement	26th International Conference on Engineering of Complex Computer Systems, ICECCS 2022 - Hiroshima, Japon Durée: 26 mars 2022 → 30 mars 2022

Série de publications

Nom	Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS
Volume	2022-March
ISSN (imprimé)	2770-8527
ISSN (Electronique)	2770-8535

Une conférence

Une conférence	26th International Conference on Engineering of Complex Computer Systems, ICECCS 2022
Pays/Territoire	Japon
La ville	Hiroshima
période	26/03/22 → 30/03/22

SDG des Nations Unies

Ce résultat contribue à ou aux Objectifs de développement durable suivants

SDG 7 Énergie abordable et propre

Accès au document

10.1109/ICECCS54210.2022.00019

Autres fichiers et liens

Lien vers la publication dans Scopus

Contient cette citation

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. Dans Proceedings - 2022 26th International Conference on Engineering of Complex Computer Systems, ICECCS 2022 (p. 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. p. 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. Dans 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., p. 91-96, 26th International Conference on Engineering of Complex Computer Systems, ICECCS 2022, Hiroshima, Japon, 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).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

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

UR - https://www.scopus.com/pages/publications/85130090823

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

Résumé

Série de publications

Une conférence

SDG des Nations Unies

Accès au document

Autres fichiers et liens

Empreinte digitale

Contient cette citation