{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:12:56Z","timestamp":1762459976002},"reference-count":28,"publisher":"Oxford University Press (OUP)","issue":"1","license":[{"start":{"date-parts":[[2021,4,21]],"date-time":"2021-04-21T00:00:00Z","timestamp":1618963200000},"content-version":"vor","delay-in-days":110,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"North Portugal Regional Operational Programme","award":["NORTE-01-0145-FEDER-000016"],"award-info":[{"award-number":["NORTE-01-0145-FEDER-000016"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,1,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>This paper explores the role of formal methods as part of the user-centred design of interactive systems. An iterative process is described, developing prototypes incrementally, proving user-centred requirements while at the same time evaluating the prototypes that are executable forms of the developed models using \u2018traditional\u2019 techniques for user evaluation. A formal analysis complements user evaluations. This approach enriches user-centred design that typically focuses understanding on context and producing sketch designs. These sketches are often non-functional (e.g. paper) prototypes. They provide a means of exploring candidate design possibilities using techniques such as cooperative evaluation. This paper describes a further step in the process using formal analysis techniques. The use of formal methods provides a systematic approach to checking plausibility and consistency during early design stages, while at the same time enabling the generation of executable prototypes. The technique is illustrated through an example based on a pill dispenser.<\/jats:p>","DOI":"10.1093\/iwcomp\/iwab012","type":"journal-article","created":{"date-parts":[[2021,4,22]],"date-time":"2021-04-22T17:52:39Z","timestamp":1619113959000},"page":"55-72","source":"Crossref","is-referenced-by-count":2,"title":["Balancing the formal and the informal in user-centred design"],"prefix":"10.1093","volume":"33","author":[{"given":"Michael D","family":"Harrison","sequence":"first","affiliation":[{"name":"School of Computing, Newcastle University, Urban Sciences Building, Newcastle upon Tyne, NE4 5TG, UK"}]},{"given":"Paolo","family":"Masci","sequence":"additional","affiliation":[{"name":"National Institute of Aerospace, 100 Exploration Way, Hampton, VA 23666, USA"}]},{"given":"Jos\u00e9 Creissac","family":"Campos","sequence":"additional","affiliation":[{"name":"Department of Informatics, University of Minho, Campus de Gualtar, 4710-057 Braga, Portugal"},{"name":"HASLab - High-Assurance Software Laboratory \/ INESC TEC, Campus de Gualtar, 4710-057 Braga, Portugal"}]}],"member":"286","published-online":{"date-parts":[[2021,4,21]]},"reference":[{"key":"2021070808100481300_ref1","volume-title":"Contextual Design: Defining Customer-Centred Systems","author":"Beyer","year":"1998"},{"key":"2021070808100481300_ref2","doi-asserted-by":"crossref","first-page":"561","DOI":"10.1109\/THMS.2014.2329476","article-title":"Automatically generating specification properties from task models for the verification of human-automation interaction","volume":"44","author":"Bolton","year":"2014","journal-title":"IEEE Trans. Hum. Mach. Syst."},{"key":"2021070808100481300_ref3","first-page":"1","article-title":"Using formal verification to evaluate human-automation interaction, a review","volume":"99","author":"Bolton","year":"2013","journal-title":"IEEE Trans. Syst. Man Cybern. Part A Syst. Humans"},{"key":"2021070808100481300_ref4","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/978-3-319-51838-1_6","article-title":"Combining Models for Interactive System Modelling","volume-title":"The Handbook of Formal Methods in Human-Computer Interaction","author":"Bowen","year":"2017"},{"key":"2021070808100481300_ref5","volume-title":"Scenario Based Design: Envisioning Work and Technology in System Development","author":"Carroll","year":"1995"},{"key":"2021070808100481300_ref6","article-title":"Analysis of erroneous actions in the design of critical systems","author":"Fields","year":"2001"},{"key":"2021070808100481300_ref7","doi-asserted-by":"crossref","first-page":"1668","DOI":"10.1016\/j.apergo.2014.05.012","article-title":"7 themes for guiding situated ergonomic assessments of medical devices: a case study of an inpatient glucometer","volume":"5","author":"Furniss","year":"2014","journal-title":"Appl. Ergon."},{"key":"2021070808100481300_ref8","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/978-3-642-14562-9_5","article-title":"Using Storyboards to Integrate Models and Informal Design Knowledge","volume-title":"Model-Driven Development of Advanced User Interfaces","author":"Haesen","year":"2011"},{"key":"2021070808100481300_ref9","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","article-title":"Statecharts: a visual formalism for complex systems","volume":"8","author":"Harel","year":"1987","journal-title":"Sci. Comput. Program."},{"key":"2021070808100481300_ref10","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/s11334-013-0201-3","article-title":"Reusing models and properties in the analysis of similar interactive devices","volume":"11","author":"Harrison","year":"2015","journal-title":"Innov. Syst. Softw. Eng."},{"key":"2021070808100481300_ref11","first-page":"274","article-title":"Formal Modelling as a Component of User Interface Design","volume-title":"Software Technologies: Applications and Foundations STAF 2018 Collocated Workshops (Revised Selected Papers)","author":"Harrison","year":"2018"},{"key":"2021070808100481300_ref12","doi-asserted-by":"crossref","first-page":"802","DOI":"10.1109\/TSE.2018.2804939","article-title":"Verification templates for the analysis of user interface software design","volume":"45","author":"Harrison","year":"2019","journal-title":"IEEE Trans. Softw. Eng."},{"key":"2021070808100481300_ref13","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/j.scico.2019.02.003","article-title":"Formal techniques in the safety analysis of software components of a new dialysis machine","volume":"175","author":"Harrison","year":"2019","journal-title":"Sci. Comput. Program."},{"key":"2021070808100481300_ref14","doi-asserted-by":"crossref","first-page":"834","DOI":"10.1109\/THMS.2017.2717910","article-title":"Verification of user interface software: the example of use-related safety requirements and programmable medical devices","volume":"47","author":"Harrison","year":"2017","journal-title":"ACM Trans. Hum. Mach. Syst."},{"key":"2021070808100481300_ref15","first-page":"50","article-title":"Formal tasks and systems models as a tool for specifying and assessing automation designs","volume-title":"Proc. 1st int. conf. application and theory of automation in command and control Systems, ATACCS \u201811","author":"Martinie","year":"2011"},{"key":"2021070808100481300_ref16","first-page":"81","article-title":"Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example","volume-title":"Proc. ACM symposium engineering interactive systems (EICS 2013)","author":"Masci","year":"2013"},{"key":"2021070808100481300_ref17","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/s11334-013-0202-2","article-title":"Using pvs to support the analysis of distributed cognition systems","volume":"11","author":"Masci","year":"2015","journal-title":"Innov. Syst. Softw. Eng."},{"key":"2021070808100481300_ref18","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/978-3-642-28891-3_27","article-title":"Using PVS to Investigate Incidents Through the Lens of Distributed Cognition","volume-title":"NASA Formal Methods","author":"Masci","year":"2012"},{"key":"2021070808100481300_ref19","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1007\/978-3-319-21690-4_30","article-title":"PVSio-web 2.0: Joining PVS to HCI","volume-title":"Computer aided verification: 27th int. conf. CAV 2015, San Francisco, CA, USA, July 18\u201324, 2015, Proceedings, Part I","author":"Masci","year":"2015"},{"key":"2021070808100481300_ref20","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1007\/978-3-319-66197-1_18","article-title":"A hazard analysis method for systematic identification of safety requirements for user interface software in medical devices","volume-title":"15th int. conf. software engineering and formal methods (SEFM 2017)","author":"Masci","year":"2017"},{"key":"2021070808100481300_ref21","volume-title":"Improving Your Human-Computer Interface: A Practical Technique","author":"Monk","year":"1993"},{"key":"2021070808100481300_ref22","volume-title":"Programming from Specifications","author":"Morgan","year":"1994"},{"key":"2021070808100481300_ref23","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1109\/TSE.2002.1027801","article-title":"CTTE: support for developing and analyzing task models for interactive system design","volume":"28","author":"Mori","year":"2002","journal-title":"IEEE Trans. Softw. Eng."},{"key":"2021070808100481300_ref24","article-title":"Rapid Prototyping in PVS","author":"Mu\u00f1oz","year":"2003"},{"key":"2021070808100481300_ref25","first-page":"249","article-title":"Heuristic evaluation of user interfaces","volume-title":"ACM CHI proc. CHI \u201890: empowering people","author":"Nielsen","year":"1990"},{"key":"2021070808100481300_ref26","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","article-title":"PVS: A prototype verification system","volume-title":"Eleventh int. conf. automated deduction (CADE)","author":"Owre","year":"1992"},{"key":"2021070808100481300_ref27","volume-title":"Software Engineering","author":"Sommerville","year":"2010"},{"key":"2021070808100481300_ref28","doi-asserted-by":"crossref","DOI":"10.4204\/EPTCS.284.8","article-title":"Integrating user design and formal models within PVSio-Web","volume-title":"Workshop on formal intergrated development environment (F-IDE-18). Electronic Proc. theoretical computer science (EPTCS)","author":"Watson","year":"2018"}],"container-title":["Interacting with Computers"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/iwc\/article-pdf\/33\/1\/55\/38495883\/iwab012.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/iwc\/article-pdf\/33\/1\/55\/38495883\/iwab012.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,8]],"date-time":"2021-07-08T16:41:37Z","timestamp":1625762497000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/iwc\/article\/33\/1\/55\/6232199"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1]]},"references-count":28,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2021,4,21]]},"published-print":{"date-parts":[[2021,1,12]]}},"URL":"https:\/\/doi.org\/10.1093\/iwcomp\/iwab012","relation":{},"ISSN":["0953-5438","1873-7951"],"issn-type":[{"value":"0953-5438","type":"print"},{"value":"1873-7951","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2021,1]]},"published":{"date-parts":[[2021,1]]}}}