{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:01:45Z","timestamp":1762459305509,"version":"3.41.0"},"publisher-location":"Cham","reference-count":51,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319216898"},{"type":"electronic","value":"9783319216904"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21690-4_30","type":"book-chapter","created":{"date-parts":[[2015,7,15]],"date-time":"2015-07-15T06:08:27Z","timestamp":1436940507000},"page":"470-478","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["PVSio-web 2.0: Joining PVS to HCI"],"prefix":"10.1007","author":[{"given":"Paolo","family":"Masci","sequence":"first","affiliation":[]},{"given":"Patrick","family":"Oladimeji","sequence":"additional","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","published-online":{"date-parts":[[2015,7,16]]},"reference":[{"issue":"6","key":"30_CR1","doi-asserted-by":"publisher","first-page":"514","DOI":"10.2345\/0899-8205-47.6.514","volume":"47","author":"L Simone","year":"2013","unstructured":"Simone, L.: Software-related recalls: an analysis of records. Biomed. Instrum. Technol. 47(6), 514\u2013522 (2013)","journal-title":"Biomed. Instrum. Technol."},{"key":"30_CR2","unstructured":"US Food and Drug Administration (FDA), Manufacturer and User Facility Device Experience Database (MAUDE). http:\/\/www.fda.gov\/MedicalDevices\/DeviceRegulationandGuidance\/PostmarketRequirements\/ReportingAdverseEvents\/ucm127891.htm"},{"issue":"5","key":"30_CR3","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1109\/THMS.2014.2331034","volume":"44","author":"G Gelman","year":"2014","unstructured":"Gelman, G., Feigh, K., Rushby, J.: Example of a complementary use of model checking and human-performance simulation. IEEE Trans. Hum. Mach. Syst. 44(5), 576\u2013590 (2014)","journal-title":"IEEE Trans. Hum. Mach. Syst."},{"key":"30_CR4","volume-title":"Software for Dependable Systems: Sufficient Evidence?","author":"L Millett","year":"2007","unstructured":"Millett, L., Thomas, M., Jackson, D., et al.: Software for Dependable Systems: Sufficient Evidence?. National Academies Press, Washington, DC (2007)"},{"key":"30_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"30_CR6","unstructured":"PVS Specification and Verification System \u2013 GitHub repository. https:\/\/github.com\/samowre\/PVS"},{"key":"30_CR7","unstructured":"PVSio-web - Interactive human-computer systems modelling and prototyping tool. http:\/\/www.pvsioweb.org"},{"key":"30_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/BFb0028775","volume-title":"Computer Aided Verification","author":"C Heitmeyer","year":"1998","unstructured":"Heitmeyer, C., Kirby, J., Labaw, B., Bharadwaj, R.: SCR: a toolset for specifying and analyzing software requirements. In: Vardi, M.Y., Hu, A.J. (eds.) CAV 1998. LNCS, vol. 1427, pp. 526\u2013531. Springer, Heidelberg (1998)"},{"key":"30_CR9","unstructured":"Mathworks Simulink. http:\/\/www.mathworks.com\/products\/simulink"},{"key":"30_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"501","DOI":"10.1007\/978-3-540-92698-6_30","volume-title":"Engineering Interactive Systems, EIS 2007","author":"H Thimbleby","year":"2008","unstructured":"Thimbleby, H., Gow, J.: Applying graph theory to interaction design. In: Gulliksen, J., Harning, M.B., van der Veer, G.C., Wesson, J. (eds.) EIS 2007. LNCS, vol. 4940, pp. 501\u2013519. Springer, Heidelberg (2008)"},{"key":"30_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"667","DOI":"10.1007\/978-3-642-02574-7_75","volume-title":"Human-Computer Interaction","author":"P Palanque","year":"2009","unstructured":"Palanque, P., Ladry, J.-F., Navarre, D., Barboni, E.: High-Fidelity Prototyping of Interactive Systems Can Be Formal Too. In: Jacko, J.A. (ed.) HCI International 2009, Part I. LNCS, vol. 5610, pp. 667\u2013676. Springer, Heidelberg (2009)"},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"Campos, J., Harrison, M.: Interaction engineering using the IVY tool. In: Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS09), pp. 35\u201344. ACM (2009)","DOI":"10.1145\/1570433.1570442"},{"key":"30_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-36377-7_9","volume-title":"The Essence of Computation","author":"J Hatcliff","year":"2002","unstructured":"Hatcliff, J., Dwyer, M.B., P\u0103s\u0103reanu, C.S.: Foundations of the Bandera abstraction tools. In: Mogensen, T.\u00c6., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 172\u2013203. Springer, Heidelberg (2002)"},{"key":"30_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-319-21215-9_6","volume-title":"Tests and Proofs","author":"AM Dutle","year":"2015","unstructured":"Dutle, A.M., Mu\u00f1oz, C.A., Narkawicz, A.J., Butler, R.W.: Software validation via model animation. In: Blanchette, J.C., Kosmatov, N. (eds.) TAP 2015. LNCS, vol. 9154, pp. 92\u2013108. Springer, Heidelberg (2015)"},{"key":"30_CR15","unstructured":"Mu\u00f1oz, C.: Rapid prototyping in PVS, Technical report NIA Report No. 2003\u201303, NASA\/CR-2003-212418. National Institute of Aerospace (2003)"},{"key":"30_CR16","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 (ETAPS). LNCS, vol. 8411, pp. 200\u2013214. Springer, Heidelberg (2014)"},{"key":"30_CR17","unstructured":"Masci, P., Oladimeji, P., Curzon, P., Thimbleby, H.: Tool demo: Using PVSio-web to demonstrate software issues in medical user interfaces. In: 4th International Symposium on Foundations of Healthcare Information Engineering and Systems (FHIES 2014) (2014)"},{"key":"30_CR18","doi-asserted-by":"crossref","unstructured":"Masci, P., Ayoub, A., Curzon, P., Harrison, M., Lee, I., Thimbleby, H.: Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example. In: EICS2013, 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems. ACM Digital Library (2013)","DOI":"10.1145\/2494603.2480302"},{"key":"30_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-40793-2_21","volume-title":"Computer Safety, Reliability, and Security","author":"P Masci","year":"2013","unstructured":"Masci, P., Ayoub, A., Curzon, P., Lee, I., Sokolsky, O., Thimbleby, H.: Model-based development of the generic PCA infusion pump user interface prototype in PVS. In: Bitsch, F., Guiochet, J., Ka\u00e2niche, M. (eds.) SAFECOMP. LNCS, vol. 8153, pp. 228\u2013240. Springer, Heidelberg (2013)"},{"issue":"2","key":"30_CR20","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s11334-013-0200-4","volume":"11","author":"P Masci","year":"2013","unstructured":"Masci, P., Ruk\u0161\u0117nas, R., Oladimeji, P., Cauchi, P., 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 Syst. Softw. Eng. 11(2), 73\u201393 (2013)","journal-title":"Innovations Syst. Softw. Eng."},{"key":"30_CR21","unstructured":"Harrison, M., Masci, P., Campos, J., Curzon, P.: Demonstrating that medical devices satisfy user related safety requirements. In: 4th International Symposium on Foundations of Healthcare Information Engineering and Systems (FHIES 2014) (2014)"},{"key":"30_CR22","unstructured":"Masci, P.: Design issues in medical user interfaces. https:\/\/www.youtube.com\/watch?v=T0QmUe0bwL8"},{"key":"30_CR23","unstructured":"Masci, P.: Data entry issues in medical devices. Seminar given within the Washington Adventist Hospital\u2019s Continuing Medical Education (CME) Program (2014)"},{"issue":"3","key":"30_CR24","first-page":"26","volume":"1","author":"G Krasner","year":"1988","unstructured":"Krasner, G., Pope, S.: A description of the model-view-controller user interface paradigm in the Smalltalk-80 system. J. Object Oriented Program. 1(3), 26\u201349 (1988)","journal-title":"J. Object Oriented Program."},{"key":"30_CR25","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8, 231\u2013274 (1987)","journal-title":"Sci. Comput. Program."},{"key":"30_CR26","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)"},{"key":"30_CR27","volume-title":"Design Patterns: Elements of Reusable Object-oriented Software","author":"E Gamma","year":"1994","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-oriented Software. Pearson Education, Upper Saddle River (1994)"},{"key":"30_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-319-06200-6_16","volume-title":"NASA Formal Methods","author":"P Masci","year":"2014","unstructured":"Masci, P., Zhang, Y., Jones, P., Oladimeji, P., D\u2019Urso, E., Bernardeschi, C., Curzon, P., Thimbleby, H.: Combining PVSio with Stateflow. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 209\u2013214. Springer, Heidelberg (2014)"},{"key":"30_CR29","unstructured":"Bernardeschi, C., Domenici, A., Masci, P.: Integrated simulation of implantable cardiac pacemaker software and heart models. In: 2nd International Conference on Cardiovascular Technologies (CARDIOTECHNIX 2014). ScitePress Digital Library (2014). http:\/\/www.scitepress.org"},{"key":"30_CR30","unstructured":"Node.js. http:\/\/nodejs.org"},{"key":"30_CR31","unstructured":"Jison - JavaScript Parser Generator. http:\/\/jison.org"},{"key":"30_CR32","unstructured":"Handlebars Semantic Templates. http:\/\/handlebarsjs.com"},{"key":"30_CR33","doi-asserted-by":"crossref","unstructured":"Bowen, J., Reeves, S.: Modelling safety properties of interactive medical systems. In: Proceedings of the 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, EICS 2013, pp. 91\u2013100. ACM (2013)","DOI":"10.1145\/2494603.2480314"},{"key":"30_CR34","unstructured":"Masci, P., Couto, L., Larsen, P., Curzon, P.: Integrating the PVSio-web modelling and prototyping environment with Overture. In: 13th Overture Workshop, Satellite Event of FM 2015 (2015)"},{"key":"30_CR35","unstructured":"CodeMirror text editor for web browsers. http:\/\/codemirror.net"},{"key":"30_CR36","unstructured":"D3.js JavaScript library for dynamic creation and control of graphical elements. http:\/\/d3js.org"},{"key":"30_CR37","unstructured":"Oladimeji, P., Masci, P., Curzon, P., Thimbleby, H.: 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:\/\/www.pvsioweb.org"},{"key":"30_CR38","unstructured":"JSLint - JavaScript Code Quality Tool. http:\/\/www.jslint.com"},{"key":"30_CR39","unstructured":"Jasmine - JavaScript Testing Tool. http:\/\/jasmine.github.io"},{"key":"30_CR40","unstructured":"Download statistics for package pvsio-web. http:\/\/npm-stat.com\/charts.html?package=pvsio-web"},{"key":"30_CR41","volume-title":"Formal Specification and Verification of Human Interactive Interfaces Incorporating Voice Control","author":"B Hall","year":"2013","unstructured":"Hall, B., Bhatt, D.: Formal Specification and Verification of Human Interactive Interfaces Incorporating Voice Control. Project Proposal, Honeywell (2013)"},{"key":"30_CR42","unstructured":"Medical devices and HCI. Full day tutorial at NordiCHI (2014). http:\/\/cs.swan.ac.uk\/~cspo\/2014\/nordichi\/"},{"key":"30_CR43","unstructured":"Masci, P.: Design and analysis of software for interactive medical devices. Ph.D. module at University of Pisa (2014). http:\/\/phd.dii.unipi.it\/formazione\/item\/85-dr-paolo-masci"},{"key":"30_CR44","volume-title":"Exploring Aspects of Automated Test Generation on Models","author":"N Robb","year":"2015","unstructured":"Robb, N.: Exploring Aspects of Automated Test Generation on Models. Waikato University, New Zealand, Honour Project (2015)"},{"key":"30_CR45","volume-title":"Usability study of a system that models interactive systems","author":"I Pascoe","year":"2015","unstructured":"Pascoe, I.: Usability study of a system that models interactive systems. Waikato University, New Zealand, Honour Project (2015)"},{"key":"30_CR46","unstructured":"D\u2019Urso, E.: Emulink: a graphical modelling environment for PVS, Master\u2019s thesis. University of Pisa, Italy (2014)"},{"key":"30_CR47","unstructured":"Faria, C.: Web-base user interface prototyping and simulation, Master\u2019s thesis. University of Minho, Portugal (2014)"},{"key":"30_CR48","unstructured":"Proof Explorer. https:\/\/github.com\/thehogfather\/ProofExplorer"},{"key":"30_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-540-27813-9_45","volume-title":"Computer Aided Verification","author":"L Moura de","year":"2004","unstructured":"de Moura, L., Owre, S., Rue\u00df, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 496\u2013500. Springer, Heidelberg (2004)"},{"key":"30_CR50","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","volume-title":"Automated Reasoning","author":"A Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171\u2013178. Springer, Heidelberg (2008)"},{"key":"30_CR51","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K., Hakansson, J., Petterson, P., Yi, W., Hendriks, M.: Uppaal 4.0. In: Third International Conference on Quantitative Evaluation of Systems. QEST 2006, pp. 125\u2013126. IEEE (2006)","DOI":"10.1109\/QEST.2006.59"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21690-4_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T06:30:28Z","timestamp":1748500228000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21690-4_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216898","9783319216904"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21690-4_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}