{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T08:41:18Z","timestamp":1773650478557,"version":"3.50.1"},"reference-count":44,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"6","license":[{"start":{"date-parts":[[2017,12,1]],"date-time":"2017-12-01T00:00:00Z","timestamp":1512086400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/3.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"publisher","award":["EP\/G059063\/1"],"award-info":[{"award-number":["EP\/G059063\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"name":"CHI+MED","award":["NORTE-01-0145-FEDER-000016"],"award-info":[{"award-number":["NORTE-01-0145-FEDER-000016"]}]},{"name":"North Portugal Regional Operational Programme","award":["NORTE 2020"],"award-info":[{"award-number":["NORTE 2020"]}]},{"name":"PORTUGAL 2020 Partnership Agreement"},{"DOI":"10.13039\/501100008530","name":"European Regional Development Fund","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100008530","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Human-Mach. Syst."],"published-print":{"date-parts":[[2017,12]]},"DOI":"10.1109\/thms.2017.2717910","type":"journal-article","created":{"date-parts":[[2017,7,26]],"date-time":"2017-07-26T18:48:47Z","timestamp":1501094927000},"page":"834-846","source":"Crossref","is-referenced-by-count":28,"title":["Verification of User Interface Software: The Example of Use-Related Safety Requirements and Programmable Medical Devices"],"prefix":"10.1109","volume":"47","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5567-9650","authenticated-orcid":false,"given":"Michael D.","family":"Harrison","sequence":"first","affiliation":[]},{"given":"Paolo","family":"Masci","sequence":"additional","affiliation":[]},{"given":"Jose Creissac","family":"Campos","sequence":"additional","affiliation":[]},{"given":"Paul","family":"Curzon","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","author":"harrison","year":"2015"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70569-7_6"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55602-8_217"},{"key":"ref32","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45657-0_29","article-title":"NuSMV 2: An open source tool for symbolic model checking","volume":"2404","author":"cimatti","year":"2002","journal-title":"Computer-Aided Verification"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-013-0201-3"},{"key":"ref30","article-title":"Alaris GP volumetric pump: directions for use","year":"2006"},{"key":"ref37","first-page":"470","author":"masci","year":"2015","journal-title":"PVSio-web 2 0 Joining PVS to HCI"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008615614281"},{"key":"ref35","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/THMS.2015.2421511"},{"key":"ref10","article-title":"SAL: Tutorial","author":"de moura","year":"2004"},{"key":"ref40","article-title":"Medical devices - Application of usability engineering to medical devices","year":"2010"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2002.1027801"},{"key":"ref12","article-title":"Analysis of erroneous actions in the design of critical systems","author":"fields","year":"2001"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/1061254.1061256"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/ASWEC.2015.30"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038667"},{"key":"ref16","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","article-title":"A tutorial on UPPAAL","author":"behrmann","year":"2004","journal-title":"Formal Methods for the Design of Real-Time Systems"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2013.50"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2014.2358224"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-COMPANION.2009.5070972"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2004.1347530"},{"key":"ref4","author":"rogers","year":"2011","journal-title":"Interaction Design Beyond Human Computer Interaction"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-008-0095-2"},{"key":"ref3","article-title":"General principles of software validation; Final guidance for industry and FDA staff","year":"2002"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/THMS.2014.2329476"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/2494603.2480302"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.113"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-010-0129-9"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/1570433.1570442"},{"key":"ref2","article-title":"Generic infusion pump hazard analysis and safety requirements","author":"arney","year":"2009"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/TSMC.2013.2256129"},{"key":"ref1","author":"leveson","year":"2011","journal-title":"Engineering a Safer World Systems Thinking Applied to Safety (Engineering Systems)"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/SEHC.2012.6227013"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/SMC.2013.158"},{"key":"ref21","first-page":"92","article-title":"Applying the SRC requirements method to a weapons control panel: An experience report","author":"heitmeyer","year":"0","journal-title":"2nd ACM Workshop on Formal Methods in Softwre Practice"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1097\/PTS.0b013e3182948a69"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-44902-9_12"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2383396"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/SMC.2014.6974507"},{"key":"ref44","first-page":"1","article-title":"A generic user interface architecture for analyzing use hazards in infusion pump software","volume":"36","author":"masci","year":"2014","journal-title":"Medical Cyber-physical Systems Workshop"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1145\/2527269.2527272"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40793-2_21"}],"container-title":["IEEE Transactions on Human-Machine Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6221037\/8105908\/07993052.pdf?arnumber=7993052","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T16:26:20Z","timestamp":1642004780000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/7993052\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12]]},"references-count":44,"journal-issue":{"issue":"6"},"URL":"https:\/\/doi.org\/10.1109\/thms.2017.2717910","relation":{},"ISSN":["2168-2291","2168-2305"],"issn-type":[{"value":"2168-2291","type":"print"},{"value":"2168-2305","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12]]}}}