Mechanical Lung Ventilator (ABZ 2024)

This document presents the case study for ABZ 2024 conference. The case study introduces Mechanical Lung Ventilator (MLV). The MLV is intended to provide ventilation support for patients that require mechanical ventilation in two operative modes: Pressure Controlled Ventilation (PCV) and Pressure Support Ventilation (PSV). The former is used when patients are not able to start breathing on their own, while the latter support patients by partially taking over the work of breathing.

For a more detailed description of the case study, and the document reporting the requirements see here.

Publications

An Event-B Model of a Mechanical Lung Ventilator

Abstract 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.
Case Study Digital Printed Abstract View Cite Source

FRETting and Formal Modelling: A Mechanical Lung Ventilator

Abstract In this paper, we use NASA’s Formal Requirements Elicitation Tool (FRET) and the Event-B formal method to model and verify the requirements for the ABZ 2024 case study which is a mechanical lung ventilator.
Case Study Digital Printed Abstract View Cite Source

Modelling and Analysing a Mechanical Lung Ventilator in mCRL2

Abstract We model the Mechanical Lung Ventilator (MLV) in the process algebra mCRL2. The functional requirements of the MLV are formalised in the modal mu-calculus, and we use model checking to analyse whether these requirements hold true of our model.
Case Study Digital Printed Abstract View Cite Source

Modelling the mechanical lung ventilation system using TASTD

Abstract For the ABZ2024 conference, the proposed case study consists of modelling the adaptive outdoor mechanical lung ventilation system. The mechanical lung ventilator is intended to provide ventilation support for patients that are in intensive therapy and that require mechanical ventilation.
Case Study Digital Printed Abstract View Cite Source

Real-Time CCSL: Application to the Mechanical Lung Ventilator

Abstract This case-study paper reports on our experience in modelling the mechanical lung ventilator using the Clock Constraint Specification Language (CCSL). CCSL captures the causal and temporal behaviour of a system by specifying constraints on logical clocks.
Case Study Digital Printed Abstract View Cite Source
ABZ'24