{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,27]],"date-time":"2025-06-27T04:19:15Z","timestamp":1750997955742,"version":"3.41.0"},"reference-count":48,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2018,6,1]],"date-time":"2018-06-01T00:00:00Z","timestamp":1527811200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2022,6,15]],"date-time":"2022-06-15T00:00:00Z","timestamp":1655251200000},"content-version":"vor","delay-in-days":1475,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2018,6]]},"DOI":"10.1016\/j.scico.2017.11.002","type":"journal-article","created":{"date-parts":[[2017,11,16]],"date-time":"2017-11-16T20:47:09Z","timestamp":1510865229000},"page":"122-147","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":3,"special_numbering":"C","title":["Validating and verifying the requirements and design of a haemodialysis machine using the Rodin toolset"],"prefix":"10.1016","volume":"158","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4095-0732","authenticated-orcid":false,"given":"Thai Son","family":"Hoang","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0210-0983","authenticated-orcid":false,"given":"Colin","family":"Snook","sequence":"additional","affiliation":[]},{"given":"Asieh","family":"Salehi","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Butler","sequence":"additional","affiliation":[]},{"given":"Lukas","family":"Ladenberger","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"author":"Mashkoor","key":"10.1016\/j.scico.2017.11.002_br0010"},{"year":"2010","series-title":"Modeling in Event-B: System and Software Engineering","author":"Abrial","key":"10.1016\/j.scico.2017.11.002_br0020"},{"issue":"2","key":"10.1016\/j.scico.2017.11.002_br0030","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","article-title":"ProB: an automated analysis toolset for the B method","volume":"10","author":"Leuschel","year":"2008","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"10.1016\/j.scico.2017.11.002_br0040","series-title":"Proceedings of the B2011","article-title":"Modelling control process and control mode with synchronising orthogonal statemachines","author":"Snook","year":"2011"},{"key":"10.1016\/j.scico.2017.11.002_br0050","series-title":"Rodin Workshop 2012, Fontainbleau","first-page":"31","article-title":"A framework for diagrammatic modelling extensions in Rodin","author":"Savicks","year":"2012"},{"key":"10.1016\/j.scico.2017.11.002_br0060","series-title":"Proceedings of the Rodin Workshop 2014","first-page":"29","article-title":"iUML-B statemachines","author":"Snook","year":"2014"},{"issue":"6","key":"10.1016\/j.scico.2017.11.002_br0070","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","article-title":"Rodin: an open toolset for modelling and reasoning in Event-B","volume":"12","author":"Abrial","year":"2010","journal-title":"Softw. Tools Technol. Transf."},{"year":"2012","series-title":"The ProR Approach: Traceability of Requirements and System Descriptions","author":"Jastram","key":"10.1016\/j.scico.2017.11.002_br0080"},{"key":"10.1016\/j.scico.2017.11.002_br0090","series-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z, in: Proceedings of the 5th International Conference","first-page":"360","article-title":"Validating the requirements and design of a hemodialysis machine using iUML-B, BMotion Studio, and co-simulation","volume":"vol. 9675","author":"Hoang","year":"2016"},{"author":"Object Management Group","key":"10.1016\/j.scico.2017.11.002_br0100"},{"key":"10.1016\/j.scico.2017.11.002_br0110","series-title":"Industrial Deployment of System Engineering Methods","first-page":"211","article-title":"An introduction to the Event-B modelling method","author":"Hoang","year":"2013"},{"key":"10.1016\/j.scico.2017.11.002_br0120","series-title":"Proceedings of FMICS 2009","first-page":"202","article-title":"Visualising Event-B models with B-Motion Studio","volume":"vol. 5825","author":"Ladenberger","year":"2009"},{"author":"Ladenberger","key":"10.1016\/j.scico.2017.11.002_br0130"},{"key":"10.1016\/j.scico.2017.11.002_br0150","series-title":"Proceedings of the 2014 Summer Simulation Multiconference","first-page":"37:1","article-title":"Co-simulating Event-B and continuous models via FMI","author":"Savicks","year":"2014"},{"author":"Sarshogh","key":"10.1016\/j.scico.2017.11.002_br0170"},{"issue":"2","key":"10.1016\/j.scico.2017.11.002_br0180","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","article-title":"Proving the correctness of multiprocess programs","volume":"3","author":"Lamport","year":"1977","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10.1016\/j.scico.2017.11.002_br0190","series-title":"Formal Methods and Software Engineering, in: Proceedings of the 13th International Conference on Formal Engineering Methods","first-page":"456","article-title":"Reasoning about liveness properties in Event-B","volume":"vol. 6991","author":"Hoang","year":"2011"},{"year":"2017","series-title":"ProB User Manual on LTL Model Checking","author":"Software Engineering and Programming Languages Group","key":"10.1016\/j.scico.2017.11.002_br0200"},{"issue":"12","key":"10.1016\/j.scico.2017.11.002_br0210","first-page":"143","article-title":"Council directive 93\/42\/EEC of 14 June 1993 concerning medical devices","volume":"169","author":"The Council of the European Union","year":"1993","journal-title":"Official J. L."},{"key":"10.1016\/j.scico.2017.11.002_br0220","unstructured":"The Council of the European Union. Directive 2007\/47\/EC of the European Parliament and of the council (September 2007)."},{"key":"10.1016\/j.scico.2017.11.002_br0230","series-title":"Killed by Code: Software Transparency in Implantable Medical Devices","first-page":"308","author":"Sandler","year":"2010"},{"issue":"4","key":"10.1016\/j.scico.2017.11.002_br0240","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1142\/S021853930100058X","article-title":"Failure modes in medical device software: an analysis of 15 years of recall data","volume":"8","author":"Wallace","year":"2001","journal-title":"Int. J. Reliab. Qual. Saf. Eng."},{"key":"10.1016\/j.scico.2017.11.002_br0250","unstructured":"ISO 13485: medical devices \u2013 quality management systems \u2013 requirements for regulatory purposes, 2003."},{"key":"10.1016\/j.scico.2017.11.002_br0260","unstructured":"IEC 606011:2005 medical electrical equipment part 1: general requirements for basic safety and essential performance, 2005."},{"key":"10.1016\/j.scico.2017.11.002_br0270","unstructured":"ISO 14971: medical devices \u2013 application of risk management to medical devices, 2007."},{"key":"10.1016\/j.scico.2017.11.002_br0280","doi-asserted-by":"crossref","unstructured":"IEC 62304 \u2013 medical device software \u2013 software lifecycle processes, 2006.","DOI":"10.1049\/ic:20060141"},{"key":"10.1016\/j.scico.2017.11.002_br0290","unstructured":"U.S. Food and Drug Administration (FDA). General principles of software validation; final guidance for industry and FDA staff, version 2.0. (January 2002)."},{"issue":"4","key":"10.1016\/j.scico.2017.11.002_br0300","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1109\/MC.2006.113","article-title":"A formal methods approach to medical device review","volume":"39","author":"Jetley","year":"2006","journal-title":"IEEE Comput."},{"year":"2013","series-title":"Using Event-B for Critical Device Software Systems","author":"Singh","key":"10.1016\/j.scico.2017.11.002_br0310"},{"key":"10.1016\/j.scico.2017.11.002_br0320","series-title":"Digital Human Modeling \u2013 Applications in Health, Safety, Ergonomics and Risk Management: Ergonomics and Health, in: Proceedings of the 6th International Conference","first-page":"374","article-title":"Formalizing the cardiac pacemaker resynchronization therapy","author":"Singh","year":"2015"},{"issue":"4","key":"10.1016\/j.scico.2017.11.002_br0330","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1109\/MC.2006.125","article-title":"Ensuring patient safety in wireless medical device networks","volume":"39","author":"Gehlot","year":"2006","journal-title":"IEEE Comput."},{"key":"10.1016\/j.scico.2017.11.002_br0340","series-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z, in: Proceedings of the 5th International Conference","first-page":"344","article-title":"How to assure correctness and safety of medical software: the hemodialysis machine case study","volume":"vol. 9675","author":"Arcaini","year":"2016"},{"key":"10.1016\/j.scico.2017.11.002_br0520","series-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z, in: Proceedings of the 5th International Conference","first-page":"376","article-title":"Hemodialysis machine in hybrid Event-B","volume":"vol. 9675","author":"Banach","year":"2016"},{"key":"10.1016\/j.scico.2017.11.002_br0360","series-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z, in: Proceedings of the 5th International Conference","first-page":"394","article-title":"Modelling a hemodialysis machine using algebraic state-transition diagrams and B-like methods","volume":"vol. 9675","author":"Fayolle","year":"2016"},{"key":"10.1016\/j.scico.2017.11.002_br0370","series-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z, in: Proceedings of the 5th International Conference","first-page":"409","article-title":"Modelling the haemodialysis machine with circus","volume":"vol. 9675","author":"Gomes","year":"2016"},{"key":"10.1016\/j.scico.2017.11.002_br0380","series-title":"Formal Methods for the Design of Real-Time Systems, International School on Formal Methods for the Design of Computer, Communication and Software Systems","first-page":"200","article-title":"A tutorial on uppaal","volume":"vol. 3185","author":"Behrmann","year":"2004"},{"key":"10.1016\/j.scico.2017.11.002_br0390","series-title":"7th ACM\/IEEE International Conference on Cyber-Physical Systems, ICCPS","first-page":"34:1","article-title":"Transforming medical best practice guidelines to executable and verifiable statechart models","author":"Guo","year":"2016"},{"issue":"1","key":"10.1016\/j.scico.2017.11.002_br0400","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/s11548-013-0919-2","article-title":"Formal verification of software-based medical devices considering medical guidelines","volume":"9","author":"Daw","year":"2014","journal-title":"Int. J. Comput. Assisted Radiol. Surg."},{"key":"10.1016\/j.scico.2017.11.002_br0410","series-title":"Verification and Evaluation of Computer and Communication Systems, in: Proceedings of the 11th International Conference","first-page":"189","article-title":"Uppaal vs Event-B for modelling optimised link state routing","volume":"vol. 10466","author":"Kamali","year":"2017"},{"key":"10.1016\/j.scico.2017.11.002_br0420","series-title":"Abstract State Machines, Alloy, B, VDM, and Z, in: Third International Conference","first-page":"178","article-title":"Formalizing hybrid systems with Event-B","volume":"vol. 7316","author":"Abrial","year":"2012"},{"key":"10.1016\/j.scico.2017.11.002_br0430","series-title":"Integrated Formal Methods, Proceedings of the 9th International Conference","first-page":"69","article-title":"Refinement-based development of timed systems","author":"Berthing","year":"2012"},{"key":"10.1016\/j.scico.2017.11.002_br0440","series-title":"21st International Conference on Engineering of Complex Computer Systems, ICECCS","first-page":"126","article-title":"Developing multi-view contracts using Event-B and UPPAAL timed automata","author":"Vain","year":"2016"},{"key":"10.1016\/j.scico.2017.11.002_br0450","series-title":"Proceedings of the 25th Nordic Workshop on Programming Theory, NWPT '13","first-page":"13","article-title":"Modelling critical systems with time constraints in Event-B","author":"Siavashi","year":"2013"},{"key":"10.1016\/j.scico.2017.11.002_br0460","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1016\/j.scico.2014.04.012","article-title":"Integrating SMT solvers in Rodin","volume":"94","author":"D\u00e9harbe","year":"2014","journal-title":"Sci. Comput. Program."},{"year":"2002","series-title":"Specifying Systems, the TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport","key":"10.1016\/j.scico.2017.11.002_br0470"},{"issue":"4","key":"10.1016\/j.scico.2017.11.002_br0480","doi-asserted-by":"crossref","first-page":"1091","DOI":"10.1007\/s10270-015-0456-2","article-title":"The Unit-B method \u2013 refinement guided by progress concerns","volume":"15","author":"Hudon","year":"2016","journal-title":"Softw. Syst. Model."},{"key":"10.1016\/j.scico.2017.11.002_br0490","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/j.scico.2016.04.014","article-title":"Translating B to TLA+ for validation with TLC","volume":"131","author":"Hansen","year":"2016","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.scico.2017.11.002_br0500","series-title":"Integrated Formal Methods, in: Proceedings of the 10th International Conference","first-page":"208","article-title":"Formal modelling and verification of population protocols","volume":"vol. 7940","author":"M\u00e9ry","year":"2013"}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642317302381?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642317302381?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,6,27]],"date-time":"2025-06-27T02:53:14Z","timestamp":1750992794000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642317302381"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6]]},"references-count":48,"alternative-id":["S0167642317302381"],"URL":"https:\/\/doi.org\/10.1016\/j.scico.2017.11.002","relation":{},"ISSN":["0167-6423"],"issn-type":[{"type":"print","value":"0167-6423"}],"subject":[],"published":{"date-parts":[[2018,6]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Validating and verifying the requirements and design of a haemodialysis machine using the Rodin toolset","name":"articletitle","label":"Article Title"},{"value":"Science of Computer Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.scico.2017.11.002","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2017 Elsevier B.V.","name":"copyright","label":"Copyright"}]}}