SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Sun 22 Oct 2023 14:30 - 15:00 at Room IV - Paper presentations 2 Chair(s): Kyungmin Bae

Mechanical ventilators are increasingly used for life support of critically ill patients. In this sense, despite recent technological advances, the accurate specification of their properties remains challenging, and the use of formal tools is limited. This work focuses on verifying the properties of the architecture of a mechanical ventilator using UPPAAL as a modeling tool. As a result, the system requirements and specification of a functional prototype were verified and improved using the formal model of a mechanical ventilator. This approach provides a valuable means of ensuring the correctness and reliability of mechanical ventilator systems.

Sun 22 Oct

Displayed time zone: Lisbon change

14:00 - 15:30
Paper presentations 2FTSCS at Room IV
Chair(s): Kyungmin Bae POSTECH
14:00
30m
Talk
Does Rust SPARK Joy? Safe Bindings from Rust to SPARK, Applied to the BBQueue Library
FTSCS
Aïssata Maiga , Cyrille Artho KTH Royal Institute of Technology, Sweden, Florian Gilcher , Yannick Moy AdaCore
14:30
30m
Talk
Formal Verification of a Mechanical Ventilator using UPPAALRemote
FTSCS
Jaime Cuartas Universidad del Valle, David Cortés , Joan S Betancourt , Jesus Aranda Universidad del Valle, Jose Garcia , Andres Valencia , James Ortiz Université de Namur
15:00
30m
Talk
Discussions, Closing
FTSCS
Peter Ölveczky University of Oslo, Cyrille Artho KTH Royal Institute of Technology, Sweden