Modelling and Analysing a Mechanical Lung Ventilator in mCRL2
摘要
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. Our formalisation of the MLV and its requirements reveal a few subtle imprecisions and unclarities in the informal document and we analyse their impact.