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
N1 - Publisher Copyright:
© 2022 IEEE.
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 -
