TY - GEN
T1 - An Event-B Model of a Mechanical Lung Ventilator
AU - Mammar, Amel
N1 - Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.
PY - 2024/1/1
Y1 - 2024/1/1
N2 - In this paper, we present a formal Event-B model of the Mechanical Lung Ventilator (MLV), the case study provided by the ABZ’24 conference. This system aims at helping patients maintain good breathing by providing mechanical ventilation. For this purpose, two modes are possible: Pressure Controlled Ventilation (PCV) and Pressure Support Ventilation (PSV). In the former mode, respiratory cycles are completely defined by the patient that is able to start breathing on its own. In the latter mode, the respiratory cycle is constant and controlled by the ventilator. Let us note that it is possible to move from a given mode to the other depending on the breathing capabilities of the patient under ventilation. In this paper, we illustrate the use of a correct-by-construction approach, the Event-B formal method and its refinement process, for the formal modeling and the verification of such a complex and critical system. The development of the formal models has been achieved under the Rodin platform that provides us with automatic and interactive provers used to verify the correctness of the models. We have also validated the built Event-B models using the ProB animator/model checker.
AB - In this paper, we present a formal Event-B model of the Mechanical Lung Ventilator (MLV), the case study provided by the ABZ’24 conference. This system aims at helping patients maintain good breathing by providing mechanical ventilation. For this purpose, two modes are possible: Pressure Controlled Ventilation (PCV) and Pressure Support Ventilation (PSV). In the former mode, respiratory cycles are completely defined by the patient that is able to start breathing on its own. In the latter mode, the respiratory cycle is constant and controlled by the ventilator. Let us note that it is possible to move from a given mode to the other depending on the breathing capabilities of the patient under ventilation. In this paper, we illustrate the use of a correct-by-construction approach, the Event-B formal method and its refinement process, for the formal modeling and the verification of such a complex and critical system. The development of the formal models has been achieved under the Rodin platform that provides us with automatic and interactive provers used to verify the correctness of the models. We have also validated the built Event-B models using the ProB animator/model checker.
KW - Event-B method
KW - Mechanical Lung Ventilator
KW - Refinement
KW - System modeling
KW - Verification
U2 - 10.1007/978-3-031-63790-2_25
DO - 10.1007/978-3-031-63790-2_25
M3 - Conference contribution
AN - SCOPUS:85199554191
SN - 9783031637896
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 307
EP - 323
BT - Rigorous State-Based Methods - 10th International Conference, ABZ 2024, Proceedings
A2 - Bonfanti, Silvia
A2 - Gargantini, Angelo
A2 - Scandurra, Patrizia
A2 - Leuschel, Michael
A2 - Riccobene, Elvinia
PB - Springer Science and Business Media Deutschland GmbH
T2 - 10th International Conference on Rigorous State-Based Methods, ABZ 2024
Y2 - 25 June 2024 through 28 June 2024
ER -