{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T15:25:01Z","timestamp":1744039501734},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642407925"},{"type":"electronic","value":"9783642407932"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40793-2_21","type":"book-chapter","created":{"date-parts":[[2013,8,26]],"date-time":"2013-08-26T22:10:59Z","timestamp":1377555059000},"page":"228-240","source":"Crossref","is-referenced-by-count":21,"title":["Model-Based Development of the Generic PCA Infusion Pump User Interface Prototype in PVS"],"prefix":"10.1007","author":[{"given":"Paolo","family":"Masci","sequence":"first","affiliation":[]},{"given":"Anaheed","family":"Ayoub","sequence":"additional","affiliation":[]},{"given":"Paul","family":"Curzon","sequence":"additional","affiliation":[]},{"given":"Insup","family":"Lee","sequence":"additional","affiliation":[]},{"given":"Oleg","family":"Sokolsky","sequence":"additional","affiliation":[]},{"given":"Harold","family":"Thimbleby","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","unstructured":"GPCA Hazards and Safety Requirements, \n                    \n                      http:\/\/rtg.cis.upenn.edu\/gip.php3"},{"key":"21_CR2","unstructured":"The GPCA-UI Prototype, \n                    \n                      http:\/\/tinyurl.com\/QMUL-GPCA-UI"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Babamir, S.: Constructing a model-based software monitor for the insulin pump behavior. Journal of Medical Systems\u00a036 (2012)","DOI":"10.1007\/s10916-010-9547-3"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Cauchi, A., Gimblett, A., Thimbleby, H., Curzon, P., Masci, P.: Safer \u201c5-key\u201d number entry user interfaces using differential formal analysis. In: BCS-HCI 2012 (2012)","DOI":"10.1145\/2305484.2305540"},{"key":"21_CR5","unstructured":"Center for Devices and Radiological Health, U.S. Food and Drug Administration. White Paper: Infusion Pump Improvement Initiative (2010)"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Harrison, M.D., Campos, J., Masci, P.: Reusing models and properties in the analysis of similar interactive devices. Innovations in Systems and Software Engineering (2013)","DOI":"10.1007\/s11334-013-0201-3"},{"key":"21_CR7","unstructured":"Institute for Safe Medication Practices (ISMP). Guidelines for standard order sets, \n                    \n                      http:\/\/www.ismp.org\/tools\/guidelines"},{"issue":"4","key":"21_CR8","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/s10009-003-0137-2","volume":"5","author":"R. Jetley","year":"2004","unstructured":"Jetley, R., Carlos, C., Purushothaman Iyer, S.: A case study on applying formal methods to medical devices. International Journal on Software Tools for Technology Transfer\u00a05(4), 320\u2013330 (2004)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"21_CR9","unstructured":"Jetley, R., Jones, P.: Safety requirements based analysis of infusion pump software. In: IEEE RTSS\/SMDS (2007)"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Kim, B., Ayoub, A., Sokolsky, O., Lee, I., Jones, P., Zhang, Y., Jetley, R.: Safety-assured development of the GPCA infusion pump software. In: ACM International Conference on Embedded software, EMSOFT 2011. ACM (2011)","DOI":"10.1145\/2038642.2038667"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-642-28891-3_30","volume-title":"NASA Formal Methods","author":"L. Lensink","year":"2012","unstructured":"Lensink, L., Smetsers, S., van Eekelen, M.: Generating Verifiable Java Code from Verified PVS Specifications. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol.\u00a07226, pp. 310\u2013325. Springer, Heidelberg (2012)"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Masci, P., Ayoub, A., Curzon, P., Harrison, M.D., Lee, I., Thimbleby, H.: Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example. In: EICS 2013. ACM Digital Library (2013)","DOI":"10.1145\/2494603.2480302"},{"key":"21_CR13","unstructured":"Masci, P., Ruk\u0161\u0117nas, R., Oladimeji, P., Cauchi, A., Gimblett, A., Li, Y., Curzon, P., Thimbleby, H.: On formalising interactive number entry on infusion pumps. ECEASST\u00a045 (2011)"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Masci, P., Ruk\u0161\u0117nas, R., Oladimeji, P., Cauchi, A., Gimblett, A., Li, Y., Curzon, P., Thimbleby, H.: The benefits of formalising design guidelines: A case study on the predictability of drug infusion pumps. Innovations in Systems and Software Engineering (2013)","DOI":"10.1007\/s11334-013-0200-4"},{"key":"21_CR15","unstructured":"Mu\u00f1oz, C.: Rapid prototyping in PVS. Technical Report NIA Report No. 2003-03, NASA\/CR-2003-212418, National Institute of Aerospace (2003)"},{"key":"21_CR16","unstructured":"Oladimeji, P., Masci, P., Curzon, P., Thimbleby, H.: PVSio-web: a tool for rapid prototyping device user interfaces in PVS. To appear in FMIS 2013 (2013)"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-23768-3_15","volume-title":"Human-Computer Interaction \u2013 INTERACT 2011","author":"P. Oladimeji","year":"2011","unstructured":"Oladimeji, P., Thimbleby, H., Cox, A.: Number entry interfaces and their effects on error detection. In: Campos, P., Graham, N., Jorge, J., Nunes, N., Palanque, P., Winckler, M. (eds.) INTERACT 2011, Part IV. LNCS, vol.\u00a06949, pp. 178\u2013185. Springer, Heidelberg (2011)"},{"key":"21_CR18","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., Shankar, N., Srivas, M.K.: PVS: Combining Specification, Proof Checking, and Model Checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 411\u2013414. Springer, Heidelberg (1996)"},{"key":"21_CR19","unstructured":"Owre, S., Shankar, N.: Theory Interpretations in PVS. Technical Report SRI-CSL-01-01, Computer Science Lab, SRI International, Menlo Park, CA (2001)"},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-540-71067-7_5","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Owre","year":"2008","unstructured":"Owre, S., Shankar, N.: A brief overview of PVS. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 22\u201327. Springer, Heidelberg (2008)"},{"issue":"6","key":"21_CR21","doi-asserted-by":"publisher","first-page":"507","DOI":"10.2345\/0899-8205-44.6.507","volume":"44","author":"A. Ray","year":"2010","unstructured":"Ray, A., Jetley, R., Jones, P., Zhang, Y.: Model-based engineering for medical-device software. Biomedical Instrumentation & Technology\u00a044(6), 507\u2013518 (2010)","journal-title":"Biomedical Instrumentation & Technology"},{"key":"21_CR22","unstructured":"Ruk\u0161\u0117nas, R., Masci, P., Harrison, M.D., Curzon, P.: Developing and verifying user interface requirements for infusion pumps: a refinement approach. To appear in FMIS 2013 (2013)"},{"key":"21_CR23","unstructured":"Shankar, N.: Efficiently Executing PVS. Technical report, Computer Science Laboratory, SRI International, Menlo Park (1999)"},{"key":"21_CR24","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.\u00a01827, pp. 37\u201352. Springer, Heidelberg (2000)"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Thimbleby, H., Cairns, H.: Reducing number entry errors: Solving a widespread, serious problem. Journal Royal Society Interface\u00a07(51) (2010)","DOI":"10.1098\/rsif.2010.0112"},{"key":"21_CR26","unstructured":"UK National Patient Safety Agency. Design for patient safety: A guide to the design of electronic infusion devices (2010)"},{"key":"21_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-642-32355-3_10","volume-title":"Foundations of Health Informatics Engineering and Systems","author":"H. Xu","year":"2012","unstructured":"Xu, H., Maibaum, T.: An Event-B Approach to Timing Issues Applied to the Generic Insulin Infusion Pump. In: Liu, Z., Wassyng, A. (eds.) FHIES 2011. LNCS, vol.\u00a07151, pp. 160\u2013176. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Computer Safety, Reliability, and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40793-2_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T19:54:27Z","timestamp":1558036467000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40793-2_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642407925","9783642407932"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40793-2_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}