Two Simulink Models with Requirements for a Simple Controller of a Pacemaker Device

This paper proposes a benchmark for a controller of a pacemaker device developed as part of the course “SFWRENG 3MD3 - Safe Software-Intensive Medical Devices” pro- vided at McMaster University. The benchmark includes two alternative Simulink® models, developed by two different groups of students. Each model comes with a requirement for- malized in Signal Temporal Logic (STL). We also present the testing results obtained using S-TaLiRo, a …