{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,11,19]],"date-time":"2024-11-19T17:03:59Z","timestamp":1732035839332,"version":"3.28.0"},"reference-count":33,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015,9]]},"DOI":"10.1109\/memcod.2015.7340473","type":"proceedings-article","created":{"date-parts":[[2015,12,3]],"date-time":"2015-12-03T16:13:03Z","timestamp":1449159183000},"page":"80-89","source":"Crossref","is-referenced-by-count":18,"title":["Formal validation and verification of a medical software critical component"],"prefix":"10.1109","author":[{"given":"Paolo","family":"Arcaini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvia","family":"Bonfanti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Angelo","family":"Gargantini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Atif","family":"Mashkoor","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Elvinia","family":"Riccobene","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87603-8_5"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-13251-8_8"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73210-5_25"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/2494603.2480314"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1002\/spe.1019"},{"key":"ref11","first-page":"1949","article-title":"A Metamodel-based Language and a Simulation Engine for Abstract State Machines","volume":"14","author":"gargantini","year":"2008","journal-title":"J UCS"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87603-8_7"},{"key":"ref13","first-page":"4","article-title":"Automatic Review of Abstract State Machines by Meta Property Verification","author":"arcaini","year":"2010","journal-title":"Proceedings of the Second NASA Formal Methods Symposium (NFM 2010)"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11811-1_6"},{"key":"ref15","first-page":"263","article-title":"Using Spin to Generate Tests from ASM Specifications","volume":"2589","author":"gargantini","year":"2003","journal-title":"SAT 2003 Ser LNCS"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29860-8_17"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-4758-9_8"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.4108\/icst.pervasivehealth.2014.255333"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/ICSTW.2013.29"},{"key":"ref28","article-title":"Modelling and analysing the interactive behaviour of an infusion pump","volume":"45","author":"campos","year":"2011","journal-title":"ECEASST"},{"journal-title":"Official Journal of the European Union","article-title":"EU, “Directive 2007\/47\/EC of the European Parliament and of the Council","year":"2007","key":"ref4"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/HCMDSS-MDPnP.2007.36"},{"year":"2005","key":"ref3"},{"year":"2002","key":"ref6","article-title":"U.S. Food and Drug Administration (FDA) “General principles of software validation; final guidance for industry and fda staff, version 2.0"},{"key":"ref29","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/978-3-540-70569-7_6","article-title":"Systematic analysis of control panel interfaces using formal tools","volume":"5136","author":"campos","year":"2008","journal-title":"Interactive Systems Design Specification and Verification ser LNCS"},{"year":"2006","key":"ref5"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18216-7"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.113"},{"year":"2007","key":"ref2"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0394-x"},{"year":"2003","key":"ref1"},{"key":"ref20","first-page":"49","article-title":"Incorporating formal techniques into industrial practice: an experience report,” Electronic Notes in Theoretical Computer Science","volume":"295","author":"osaiweran","year":"2013","journal-title":"proceedings the 9th Int Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA)"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/1921081.1921115"},{"key":"ref21","doi-asserted-by":"crossref","first-page":"548","DOI":"10.1007\/11526841_39","article-title":"ASD case notes: Costs and benefits of applying formal methods to industrial control software","volume":"3582","author":"broadfoot","year":"2005","journal-title":"FM 2005 Formal Methods ser LNCS"},{"key":"ref24","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/978-3-540-88479-8_22","article-title":"Model checking CSP revisited: Introducing a process analysis toolkit","volume":"17","author":"sun","year":"2008","journal-title":"Leveraging Applications of Formal Methods Verification and Validation ser CCIS"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/SSIRI.2010.28"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_14"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/2406336.2406351"}],"event":{"name":"2015 ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)","start":{"date-parts":[[2015,9,21]]},"location":"Austin, TX, USA","end":{"date-parts":[[2015,9,23]]}},"container-title":["2015 ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7329076\/7340456\/07340473.pdf?arnumber=7340473","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,23]],"date-time":"2017-06-23T20:59:36Z","timestamp":1498251576000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7340473\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9]]},"references-count":33,"URL":"https:\/\/doi.org\/10.1109\/memcod.2015.7340473","relation":{},"subject":[],"published":{"date-parts":[[2015,9]]}}}