{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,23]],"date-time":"2024-09-23T04:00:40Z","timestamp":1727064040709},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319631936"},{"type":"electronic","value":"9783319631943"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63194-3_14","type":"book-chapter","created":{"date-parts":[[2017,7,26]],"date-time":"2017-07-26T15:58:43Z","timestamp":1501084723000},"page":"214-221","source":"Crossref","is-referenced-by-count":3,"title":["Using PVSio-web to Demonstrate Software Issues in Medical User Interfaces"],"prefix":"10.1007","author":[{"given":"Paolo","family":"Masci","sequence":"first","affiliation":[]},{"given":"Patrick","family":"Oladimeji","sequence":"additional","affiliation":[]},{"given":"Paul","family":"Curzon","sequence":"additional","affiliation":[]},{"given":"Harold","family":"Thimbleby","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,27]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Cauchi, A., Gimblett, A., Thimbleby, H.W., Curzon, P., Masci, P.: Safer 5-key number entry user interfaces using differential formal analysis. In: 26th Annual BCS Interaction Specialist Group Conference on People and Computers (BCS-HCI), pp. 29\u201338. British Computer Society (2012)","DOI":"10.14236\/ewic\/HCI2012.8"},{"key":"14_CR2","unstructured":"Center for Devices and Radiological Health: US Food and Drug Administration. Infusion Pump Improvement Initiative, White Paper (2010)"},{"key":"14_CR3","unstructured":"Harrison, M.D., Campos, J.C., Masci, P.: Reusing models and properties in the analysis of similar interactive devices. In: Innovations in Systems and Software Engineering, pp. 1\u201317 (2013)"},{"key":"14_CR4","unstructured":"Harrison, M.D., Masci, P., Campos, J.C., Curzon, P.: Demonstrating that medical devices satisfy user related safety requirements. In: 4th International Symposium on Foundations of Healthcare Information Engineering and Systems (2014)"},{"key":"14_CR5","unstructured":"Institute for Safe Medication Practices (ISMP). List of error-prone abbreviations, symbols and dose designations (2006)"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Masci, P., Ayoub, A., Curzon, P., Harrison, M.D., Lee, I., Thimbleby, H.W.: Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example. In: 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS 2013). ACM Digital Library (2013)","DOI":"10.1145\/2494603.2480302"},{"key":"14_CR7","unstructured":"Masci, P., Ruk\u0161\u0117nas, R., Oladimeji, P., Cauchi, A., Gimblett, A., Li, Y., Curzon, P., Thimbleby, H.W.: On formalising interactive number entry on infusion pumps. ECEASST 45 (2011)"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Masci, P., Ruk\u0161\u0117nas, R., Oladimeji P., Cauchi, A., Gimblett, A., Li, Y., Curzon, P., Thimbleby, H.W.: The benefits of formalising design guidelines: a case study on the predictability of drug infusion pumps. In: Innovations in Systems and Software Engineering, pp. 1\u201321 (2013)","DOI":"10.1007\/s11334-013-0200-4"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-54804-8_14","volume-title":"Fundamental Approaches to Software Engineering","author":"P Masci","year":"2014","unstructured":"Masci, P., Zhang, Y., Jones, P., Curzon, P., Thimbleby, H.: Formal verification of medical device user interfaces using PVS. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol. 8411, pp. 200\u2013214. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54804-8_14"},{"key":"14_CR10","unstructured":"Medtronic. Device safety information: accidental misprogramming of insulin delivery (2014). http:\/\/www.medtronicdiabetes.com . Report # 930M12226-011"},{"key":"14_CR11","unstructured":"Munoz, C.: Rapid prototyping in PVS. National Institute of Aerospace, Hampton, VA, USA, Technical report NIA, 3 (2003)"},{"key":"14_CR12","unstructured":"Oladimeji, P., Masci, P., Curzon, P., Thimbleby, H.W.: PVSio-web: a tool for rapid prototyping device user interfaces in PVS. In: 5th International Workshop on Formal Methods for Interactive Systems (FMIS 2013) (2013). http:\/\/pvsioweb.org\/"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S Owre","year":"1996","unstructured":"Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.: PVS: combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 411\u2013414. Springer, Heidelberg (1996). doi: 10.1007\/3-540-61474-5_91"},{"issue":"9","key":"14_CR14","doi-asserted-by":"crossref","first-page":"709","DOI":"10.1109\/32.713327","volume":"24","author":"J Rushby","year":"1998","unstructured":"Rushby, J., Owre, S., Shankar, N.: Subtypes for specifications: predicate subtyping in PVS. IEEE Trans. Softw. Eng. 24(9), 709\u2013720 (1998)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-540-44616-3_3","volume-title":"Recent Trends in Algebraic Development Techniques","author":"N Shankar","year":"2000","unstructured":"Shankar, N., Owre, S.: Principles and pragmatics of subtyping in PVS. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 37\u201352. Springer, Heidelberg (2000). doi: 10.1007\/978-3-540-44616-3_3"},{"key":"14_CR16","doi-asserted-by":"publisher","unstructured":"Simone, L.K.: Software-related recalls: an analysis of records. Biomed. Instrum. Technol. 47(6), 514\u2013522 (2013). doi: 10.2345\/0899-8205-47.6.514","DOI":"10.2345\/0899-8205-47.6.514"}],"container-title":["Lecture Notes in Computer Science","Software Engineering in Health Care"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63194-3_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,13]],"date-time":"2020-10-13T14:07:10Z","timestamp":1602598030000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63194-3_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319631936","9783319631943"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63194-3_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}