{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T04:02:22Z","timestamp":1746244942300,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642548031"},{"type":"electronic","value":"9783642548048"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54804-8_14","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T09:59:16Z","timestamp":1395395956000},"page":"200-214","source":"Crossref","is-referenced-by-count":24,"title":["Formal Verification of Medical Device User Interfaces Using PVS"],"prefix":"10.1007","author":[{"given":"Paolo","family":"Masci","sequence":"first","affiliation":[]},{"given":"Yi","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Paul","family":"Jones","sequence":"additional","affiliation":[]},{"given":"Paul","family":"Curzon","sequence":"additional","affiliation":[]},{"given":"Harold","family":"Thimbleby","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"unstructured":"AAMI Medical Device Software Committee. Medical device software risk management. AAMI Tech. Rep. TIR32:2004 (2004)","key":"14_CR1"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-540-24730-2_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2004","unstructured":"Ball, T., Cook, B., Das, S., Rajamani, S.K.: Refining approximations in software predicate abstraction. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 388\u2013403. Springer, Heidelberg (2004)"},{"issue":"3","key":"14_CR3","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s11334-010-0129-9","volume":"6","author":"M.L. Bolton","year":"2010","unstructured":"Bolton, M.L., Bass, E.J.: Formally verifying human-automation interaction as part of a system model: Limitations and tradeoffs. Innovations in Systems and Software Engineering\u00a06(3), 219\u2013231 (2010)","journal-title":"Innovations in Systems and Software Engineering"},{"unstructured":"Campos, J.C., Harrison, M.D.: Modelling and analysing the interactive behaviour of an infusion pump. Electronic Communications of the EASST (2011)","key":"14_CR4"},{"doi-asserted-by":"crossref","unstructured":"Cauchi, A., Gimblett, A., Thimbleby, H., Curzon, P., Masci, P.: Safer 5-key number entry user interfaces using differential formal analysis. In: BCS-HCI (2012)","key":"14_CR5","DOI":"10.1145\/2305484.2305540"},{"unstructured":"Center for Devices and Radiological Health, US Food and Drug Administration. White Paper: Infusion Pump Improvement Initiative (2010)","key":"14_CR6"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Tkachuk, O., Visser, W., et al.: Analyzing interaction orderings with model checking. In: ASE 2004, pp. 154\u2013163. IEEE Computer Society (2004)","key":"14_CR8","DOI":"10.1109\/ASE.2004.1342733"},{"doi-asserted-by":"crossref","unstructured":"Gelman, G.E., Feigh, K.M., Rushby, J.: Example of a complementary use of model checking and agent-based simulation. In: SMC 2013. IEEE (2013)","key":"14_CR9","DOI":"10.1109\/SMC.2013.158"},{"doi-asserted-by":"crossref","unstructured":"Ginsburg, G.: Human factors engineering: A tool for medical device evaluation in hospital procurement decision-making. Journal of Bio. Informatics\u00a038(3) (2005)","key":"14_CR10","DOI":"10.1016\/j.jbi.2004.11.008"},{"doi-asserted-by":"crossref","unstructured":"Harrison, M.D., Campos, J.C., Masci, P.: Reusing models and properties in the analysis of similar interactive devices. Innovations in Systems and Software Engineering, 1\u201317 (2013)","key":"14_CR11","DOI":"10.1007\/s11334-013-0201-3"},{"unstructured":"Harrison, M.D., Masci, P., Campos, J.C., Curzon, P.: Automated theorem proving for the systematic analysis of interactive systems. In: FMIS 2013 (2013)","key":"14_CR12"},{"issue":"4","key":"14_CR13","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/MC.2006.113","volume":"39","author":"R. Jetley","year":"2006","unstructured":"Jetley, R., Purushothaman Iyer, S., Jones, P.L.: A formal methods approach to medical device review. Computer\u00a039(4), 61\u201367 (2006)","journal-title":"Computer"},{"doi-asserted-by":"crossref","unstructured":"Masci, P., Curzon, P., Harrison, M.D., Ayoub, A., 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)","key":"14_CR14","DOI":"10.1145\/2494603.2480302"},{"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. Electronic Communications of the EASST\u00a045 (2011)","key":"14_CR15"},{"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, 1\u201321 (2013)","key":"14_CR16","DOI":"10.1007\/s11334-013-0200-4"},{"unstructured":"Masci, P., Zhang, Y., Curzon, P., Harrison, M.D., Jones, P., Thimbleby, H.: Verification of software for medical devices in PVS. CHI+MED Tech. Rep. (2013), http:\/\/www.chi-med.ac.uk\/researchers\/bibdetail.php?docID=656","key":"14_CR17"},{"unstructured":"Munoz, C.: Rapid prototyping in PVS. National Institute of Aerospace, Hampton, VA, USA, Tech. Rep. NIA, 3 (2003)","key":"14_CR18"},{"unstructured":"Oladimeji, P., Masci, P., Curzon, P., Thimbleby, H.: PVSio-web: A tool for rapid prototyping device user interfaces in PVS. In: FMIS 2013 (2013)","key":"14_CR19"},{"key":"14_CR20","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.: 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)"},{"doi-asserted-by":"crossref","unstructured":"Ruk\u0161\u0117nas, R., Curzon, P., Blandford, A.E., Back, J.: Combining human error verification and timing analysis: A case study on an infusion pump. Formal Aspects of Computing (2013) (in press)","key":"14_CR21","DOI":"10.1007\/s00165-013-0288-1"},{"unstructured":"Ruk\u0161\u0117nas, R., Masci, P., Harrison, M.D., Curzon, P.: Developing and verifying user interface requirements for infusion pumps: A refinement approach. In: FMIS 2013 (2013)","key":"14_CR22"},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1007\/10722167_38","volume-title":"Computer Aided Verification","author":"J. Rushby","year":"2000","unstructured":"Rushby, J.: Verification diagrams revisited: Disjunctive invariants for easy verification. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 508\u2013520. Springer, Heidelberg (2000)"},{"issue":"2","key":"14_CR24","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/S0951-8320(01)00092-8","volume":"75","author":"J. Rushby","year":"2002","unstructured":"Rushby, J.: Using model checking to help discover mode confusions and other automation surprises. Reliability Engineering & System Safety\u00a075(2), 167\u2013177 (2002)","journal-title":"Reliability Engineering & System Safety"},{"key":"14_CR25","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":"14_CR26","series-title":"Computer Science Laboratory","first-page":"11","volume-title":"PVS prover guide","author":"N. Shankar","year":"2001","unstructured":"Shankar, N., Owre, S., Rushby, J., Stringer-Calvert, D.: PVS prover guide. Computer Science Laboratory, vol.\u00a01, pp. 11\u201312. SRI International, Menlo Park (2001)"},{"unstructured":"Story, M.F.: The FDA perspective on human factors in medical device software Development. In: IQPC Software Design for Medical Devices Europe (2012)","key":"14_CR27"},{"unstructured":"Thimbleby, H.: Press on: Principles of Interaction Programming. Mit Press (2007)","key":"14_CR28"},{"issue":"51","key":"14_CR29","doi-asserted-by":"publisher","first-page":"1429","DOI":"10.1098\/rsif.2010.0112","volume":"7","author":"H. Thimbleby","year":"2010","unstructured":"Thimbleby, H., Cairns, P.: Reducing number entry errors: solving a widespread, serious problem. Journal of the Royal Society Interface\u00a07(51), 1429\u20131439 (2010)","journal-title":"Journal of the Royal Society Interface"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54804-8_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T03:46:00Z","timestamp":1746157560000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54804-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548031","9783642548048"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54804-8_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}