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” provided at McMaster University. The benchmark includes two alternative Simulink® models, developed by two different groups of students. Each model comes with a requirement formalized in Signal Temporal Logic (STL). We also present the testing results obtained using S-TaLiRo, a well-known testing framework for Simulink® models.