Wietske will defend her Master Project thesis titled “Modelling a Mechanical Lung Ventilator in Stark”.

Abstract: In this Master Thesis a Stark model of a Mechanical Lung Ventilator (MLV) is presented. In particular, the specification document of the MLV from the ABZ 2024 case study is used.
Requirements from the case study have been transformed into DisTL (Distribution Temporal Logic) and RobTL (Robustness Temporal Logic) formulas and have been verified to show the robustness of the model against perturbations.
Additionally, a comparison with an already existing mCRL2 model of the MLV has been done, which showcased a difference in modeling the breathing dynamics.
Lastly, another comparison is done with a UPPAAL model of a general mechanical lung ventilator. This comparison highlighted that properties verifiable by UPPAAL, are, to some extent, also verifiable by the Stark tool.

The defence will take place on Monday 8 June, 15:00-16:00 in room MF 6.132.