{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T15:41:50Z","timestamp":1784302910792,"version":"3.55.0"},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>This paper proposes a benchmark for a controller of a pacemaker device developed as part of the course \u201cSFWRENG 3MD3 - Safe Software-Intensive Medical Devices\u201d pro- vided at McMaster University. The benchmark includes two alternative Simulink\u00ae 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 well-known testing framework for Simulink\u00ae models.<\/jats:p>","DOI":"10.29007\/f57w","type":"proceedings-article","created":{"date-parts":[[2022,12,13]],"date-time":"2022-12-13T23:10:12Z","timestamp":1670973012000},"page":"18-9","source":"Crossref","is-referenced-by-count":5,"title":["Two Simulink Models with Requirements for a Simple Controller of a Pacemaker Device"],"prefix":"10.29007","volume":"90","author":[{"given":"Mostafa","family":"Ayesh","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Namya","family":"Mehan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ethan","family":"Dhanraj","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Abdul","family":"El-Rahwan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Simon Emil","family":"Opalka","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tony","family":"Fan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Akil","family":"Hamilton","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Akshay Mathews","family":"Jacob","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rahul Anthony","family":"Sundarrajan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bryan","family":"Widjaja","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Claudio","family":"Menghi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"11545","event":{"name":"Proceedings of 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22)"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2022,12,13]],"date-time":"2022-12-13T23:10:13Z","timestamp":1670973013000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/QZcD"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/f57w","relation":{},"ISSN":["2398-7340"],"issn-type":[{"value":"2398-7340","type":"print"}],"subject":[]}}