Formal Verification of a Mechanical Ventilator using UPPAAL
summary
Presents a formal UPPAAL model of a bare‑bones mechanical ventilator architecture, builds a timed‑automata network and checks 40 models against 14 properties (symbolic 1–9, SMC 10–14) using UPPAAL SMC with ~500 runs for some queries; verifies safety and liveness properties and compares simulated flow per cycle to a physical prototype, finding delta T reduces relative error from 5% to 3% which equals about 10 ml difference in delivered volume; artifacts and models are available and use UPPAAL SMC for probabilistic estimates.
AI-written summary · about
chapters (19)
- 0:00Introduction
- 1:31Formal modeling for ventilators
- 4:21Critical systems and real-time
- 7:59Ventilator architecture overview
- 10:33Mathematical model
- 12:01Research objectives and choices
- 12:43Time automata with inputs and outputs
- 14:51UPPAAL model components
- 16:16Verification and validation results
- 18:03Comparison with plant data
- 19:48Conclusions and future work
- 21:13Q&A
- 21:33Case study potential
- 22:37Realism of ventilator model
- 23:41Environment and patient lungs
- 24:43Statistical model checking in UPPAAL
- 27:19Physical model origins
- 28:45Extending models with bidirectional properties
- 30:14UPPAAL SMC distributions
related talks
28mProject MakAir: How and Why to Build an Open Source Ventilator
30mInput-based Three-Valued Abstraction Refinement
13mVerification of the PULPino SoC Platform Using UVM
20mFormal Analysis of Networked PLC Controllers Interacting with Physical Environments
21mDeductive Verification of Parameterized Embedded Systems modeled in SystemC
30mOSVVM: Methodology, Library, and Models
19mVPR device models generation from Verilog with V2X
37mAndroid Industrial: Real-time data visualization