Formal verification using models of cognition
How can mathematical models of human behaviour be used as the basis of tools to detect potential for human error in the use of device designs?
Traditional approaches to the verification of computer systems focus on the device itself. The aim is then to find bugs in the software or hardware. However a design that has been verified in this way may still have problems. In particular, people may have an unnecessarily high likelihood of making mistakes when using it.
In this project we explore how formal verification can be extended to also highlight flaws in the design of devices that lead to people making systematic errors when using them. In particular, we are exploring how models of human behaviour can be integrated into verification approaches. We have developed a simple mathematical model of cognitively plausible behaviour, based on the results of empirical experiments. By combining this model with models of devices we can use model checking tools to automatically explore whether people will make particular kinds of slip errors when using devices.
▼ ▼ ▼ ▼ ▼ ▼
CHI+MED publications
- Paolo Masci, Huayi Huang, Paul Curzon & Michael Harrison
Using PVS to investigate incidents through the lens of distributed cognition (PDF, 565 KB) 4th NASA Formal Methods Symposium, Norfolk, Virginia, USA, April 3-5, 2012.
- Paul Curzon, Michael Harrison, Paolo Masci & Rimvydas Ruksenas Safety assurance cases, proof and the prevention of user error (PDF, 289 KB) Presented at the Workshop on Theorem Proving in Certification. Cambridge, UK 10 Nov 2011
- Paolo Masci, Rimvydas Ruksenasi, Patrick Oladimeji, Abigail Cauchi, Andy Gimblett, Yunqiu L, Paul Curzon & Harold Thimbleby The benefits of formalising interactive number entry (PDF, 1.1 MB) Proceedings of the 4th International Workshop on Formal Methods for Interactive Systems (FMIS2011), volume 45 of Electronic Communications of the EASST 12 Oct 2011
- Harold Thimbleby, Andy Gimblett & Abigail Cauchi Buffer Automata: a UI architecture prioritising HCI concerns for interactive devices (PDF, 729 KB) Proceedings of the 3rd ACM SIGCHI symposium on engineering interactive computer systems. EICS-11, 73-78 10 Oct 2011
- Harold Thimbleby Avoiding latent design conditions using UI discovery tools (PDF, 797 KB) International Journal of Human-Computer Interaction, 26(2-3):120-131 6 Oct 2011
- Paolo Masci & Paul Curzon Checking user-centred design principles in distributed cognition models: A case study in the healthcare domain (PDF, 552 KB) Paper for USAB2011, the 7th Conference of the Austrian Computer Society on Information Quality in eHealth 21 Sep 2011
- Jose Creissac Campos & Michael Harrison Modelling and analysing the interactive behaviour of an infusion pump (PDF, 723 KB) Proceedings of FMIS-2011, Fourth International Workshop on Formal Methods for Interactive Systems 12 Sep 2011
- Huayi Huang, Rimvydas Ruksenas, Maartje Ament, Paul Curzon, Anna Cox, Ann Blandford & Duncan Brumby Capturing the distinction between task and device errors in a formal model of user behaviour (PDF, 1.4 MB) Proceedings of FMIS-2011, Fourth International Workshop on Formal Methods for Interactive Systems 10 Jun 2011
- Paolo Masci, Paul Curzon, Huayi Huang, Rimvydas Ruksenas, Ann Blandford, Dominic Furniss & Atish Rajkomar Towards a formal framework for reasoning about the resilience of dynamic interactive systems (PDF, 348 KB) Proceedings of the 13th European Workshop on Dependable Computing, ISBN 978-1-4503-0284-5 28 Mar 2011
- Rimvydas Ruksenas & Paul Curzon Abstract models and cognitive mismatch in formal verification (PDF, 347 KB) Proceedings of FMIS-2011, Fourth International Workshop on Formal Methods for Interactive Systems 26 May 2011
- Paolo Masci, Paul Curzon, Ann Blandford & Dominic Furniss Modelling distributed cognition systems in PVS (PDF, 652 KB) Proceedings of the Fourth International Workshop on Formal Methods for Interactive Systems (FMIS 2011), Electronic Communications of the EASST, vol. 45, 2011, ISSN: 1863-2122 25 May 2011
- Paolo Masci, Rimvydas Ruksenas, Patrick Oladimeji, Abigail Cauchi, Yunqiu Li, Paul Curzon & Harold Thimbleby On formalising interactive number entry on infusion pumps (PDF, 1.1 MB) Proceedings of the Fourth International Workshop on Formal Methods for Interactive Systems (FMIS 2011), Electronic Communications of the EASST, vol. 45, 2011, ISSN: 1863-2122 25 May 2011
- Ann Blandford, Abigail Cauchi, Paul Curzon, Parisa Eslambolchilar, Dominic Furniss, Andy Gimblett, Huayi Huang, Paul Lee, Yunqiu Li, Paolo Masci, Patrick Oladimeji, Atish Rajkomar, Rimvydas Ruksenas & Harold Thimbleby Comparing actual practice and user manuals: A case study based on programmable infusion pumps (PDF, 1.1 MB) Proceedings of EICS4Med, First International Workshop on Engineering Interactive Computing Systems for Medicine and Health Care 25 May 2011
- Abigail Cauchi, Paul Curzon, Parisa Eslambolchilar, Andy Gimblett, Huayi Huang, Paul Lee, Yunqiu Li, Paolo Masci, Patrick Oladimeji, Rimvydas Ruksenas & Harold Thimbleby Towards dependable number entry for medical devices (PDF, 651 KB) Proceedings of EICS4Med, First International Workshop on Engineering Interactive Computing Systems for Medicine and Health Care 25 May 2011
- Paul Curzon, Rimvydas Ruksenas & Jonathan Back The HUM generic user model: An informal overview of the main features (PDF, 357 KB) Working paper prepared for the Work Package on Individual Cognition 8 May 2010
- Harold Thimbleby & Paul Cairns Reducing number entry errors: solving a widespread, serious problem (PDF, 647 KB) Published in "Journal of the Royal Society Interface", online 7 April 2010. (doi: 10.1098/rsif.2010.0112) 11 Apr 2010
Background publications:
Keywords: Cognition, verification, modelling
Key people: Rimvydas Ruksenas, Paolo Masci, Paul Curzon
