Top

Innovations in Systems and Software Engineering

Published in:

01-06-2015 | SI: FMIS

Reusing models and properties in the analysis of similar interactive devices

Authors: Michael D. Harrison, José Creissac Campos, Paolo Masci

Published in: Innovations in Systems and Software Engineering | Issue 2/2015

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

The paper is concerned with the comparative analysis of interactive devices. It compares two devices by checking systematically a set of template properties that are designed to explore important interface characteristics. The two devices are designed to support similar tasks in a clinical setting. The devices differ as a result of judgements based on a range of considerations including software. Variations between designs are often relatively subtle and do not always become evident through even relatively thorough user testing. Notwithstanding their subtlety, these differences may be important to the safety or usability of the device. The illustrated approach uses formal techniques to provide the analysis. This means that similar analysis can be applied systematically.

previous article The benefits of formalising design guidelines: a case study on the predictability of drug infusion pumps

next article Using PVS to support the analysis of distributed cognition systems

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

A key bounce occurs when physically pressing a button once causes a repeat of the same key.

Amnell T, Behrmann G, Bengtsson J, D’Argenio PR, David A, Fehnker A, Hune T, Jeannet B, Larsen KG, Möller MO, Pettersson P, Weise C, Yi W (2001) UPPAAL-Now, Next, and Future. In: Cassez F, Jard C, Rozoy B, Ryan M (eds) Modelling and Verification of Parallel Processes, number 2067 in Lecture Notes in Computer Science Tutorial, Springer-Verlag, Berlin, pp 100–125

Arney D, Kim B, Jetley R, Jones P, Lee I, Ray A, Sokolsky O, Zhang Y (0000) Safety requirements for the generic patient controlled analgesia pump. http://rtg.cis.upenn.edu/gip.php3

B. Braun Melsungen AG (2007) B.Braun Infusomat Space User Manual. Technical report, B. Braun Melsungen AG, 34209 Melsungen, Germany

Bligard L-A, Osvalder A-L (2007) An analytical approach for predicting and identifying use error and usability problem. In: Holzinger A (ed) Proceedings of the 3rd Human-computer interaction and usability engineering of the Austrian computer society conference on HCI and usability for medicine and health care, number 4799 in Springer Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp 427–440

Bolton ML, Bass EJ (2010) Formally verifying human-automation interaction as part of a system model: limitations and tradeoffs. Innov Syst Softw Eng 6(3):219–231CrossRef

Bolton ML, Bass EJ, Sininiceanu RI (2012) Generating phenotypical erroneous human behavior to evaluate human-automation interaction using model checking. Intern J Hum Comput Stud 70: 888–906

Bolton ML, Bass EJ, Siminiceanu RI (2013) Using formal verification to evaluate human-automation interaction, a review. IEEE Transactions on Systems, Man, and Cybernetics, Part A: Systems and Humans 99:1–16

Campos JC (2012) Minho HCI repository. http://hcispecs.di.uminho.pt

Campos JC, Harrison MD (2001) Model checking interactor specifications. Autom Softw Eng 8:275–310CrossRefMATH

10.

Campos JC, Harrison MD (2008) Systematic analysis of control panel interfaces using formal tools. In: Graham N, Palanque P (eds) Interactive systems: Design, Specification and Verification, DSVIS ’08, number 5136 in Springer Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp 72–85

11.

Campos JC, Harrison MD (2009) Interaction engineering using the IVY tool. In: Calvary G, Graham TCN, Gray P (eds) Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems, ACM Press, New York, pp 35–44

12.

Campos JC, Harrison MD (2011) Modelling and analysing the interactive behaviour of an infusion pump. Electronic Communications of the EASST, 5, San Ramon

13.

Campos JC, Harrison MD (1997) Formally Verifying Interactive Systems: A Review. In: Harrison MD, Torres JC (eds) Proceedings on the 4th Eurographics Workshop on Design, Specification and Verification of Interactive Systems (DSVIS), Springer-Verlag, Berlin, pp 119–134

14.

Cardinal Health Inc (2006) Alaris GP volumetric pump: directions for use. Technical report, Cardinal Health, 1180 Rolle, Switzerland

15.

Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV 2: An Open Source Tool for Symbolic Model Checking. In: Larsen KG, Brinksma E (eds) Computer-Aided Verification (CAV ’02), vol 2404, Lecture Notes in Computer Science, Springer-Verlag, Berlin

16.

Clarke EM, Grumberg O, Peled DA (1999) Model Checking. MIT Press, Cambridge

17.

Moura de L (2004) SAL: Tutorial. Technical report, SRI International. Computer Science Laboratory, 333 Ravenswood Avenue, Menlo Park

18.

Dix A, Finlay J, Abowd G, Beale R (1993) Human-Computer Interaction. ACM SIGCHI Bulletin, Prentice Hall

19.

Dix AJ (1991) Formal Methods for Interactive Systems. Academic Press, London

20.

Doherty G, Campos JC, Harrison MD (2008) Resources for situated actions. In: Graham N, Palanque P (eds) Interactive systems: Design, Specification and Verification, DSVIS ’08, vol 5136. Springer Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp 194–207

21.

Duke DJ, Harrison MD (1993) Abstract interaction objects. Comput Gr Forum 12(3):25–36CrossRef

22.

Fiadeiro J, Maibaum T, Bakker de J, Roever de W, Rozenberg G (1991) Describing, structuring and implementing objects. In: Foundations of Object-Oriented Languages, number 489 in Springer Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp 274–310

23.

Fields RE (2001) Analysis of erroneous actions in the design of critical systems. PhD thesis, Department of Computer Science, University of York, Heslington, York

24.

US Food and Drug Administration (2010) Infusion pump improvement initiative. Technical report, Center for Devices and Radiological Health. University of York, New york

25.

Heymann M, Degani A (2007) Formal analysis and automatic generation of user interfaces: approach, methodology, and an algorithm. J Hum Fact Ergon Soc 49(2):311–330CrossRef

26.

Johnson-Laird PN (1983) Mental Models. Harvard University Press, Cambridge

27.

Kim B, Ayoub A, Sokolsky O, Lee I, Jones P, Zhang Y, Jetley R (2011) Safety-assured development of the GPCA infusion pump software. In: Proceedings of the 9th ACM international conference on Embedded software, EMSOFT ’11, ACM, New York, pp 155–164

28.

Kirwan B, Ainsworth L (1992) A Guide to Task Analysis. Taylor and Francis, Lodon

29.

Lane R, Stanton NA, Harrison D (2006) Applying hierarchical task analysis to medication administration errors. Appl Ergon 37:669–679CrossRef

30.

Larsen KG, Pettersson P, Yi W (1997) UPPAAL in a Nutshell. Int J Softw Tool Technol Transf 1(1—-2):134–152CrossRefMATH

31.

Masci P, Rukšėnas R, Oladimeji P, Cauchi A, Gimblett A, Li Y, Curzon P, Thimbleby H (2011) On formalising interactive number entry on infusion pumps, vol 45. ECEASST, Bolton

32.

Nielsen J, Molich R (1990) Heuristic evaluation of user interfaces. In: Chew J, Whiteside J (eds) ACM CHI Proceedings CHI ’90: Empowering, People, New York, pp 249–256

33.

Oladimeji P (2012) Alaris simulation. http://cs.swan.ac.uk/cspo/simulations

34.

Oladimeji P, Thimbleby H, Cox A (2011) Number entry and their effects on error detection. In: Campos P et al (eds) Interact 2011, number 6949 in Springer Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp 178–185

35.

Paternò F, Faconti G (1992) On the Use of LOTOS to Describe Graphical Interaction. In: Monk A, Diaper D, Harrison MD (eds) People and Computers VII: HCI ’92 Conference, Cambridge University Press, BCS HCI Specialist Group, Cambridge, pp 155–174

36.

Ruksenas R, Back J, Curzon P, Blandford A (2009) Verification-guided modelling of salience and cognitive load. Form Asp Comput 21:541–569

37.

Ryan M, Fiadeiro J, Maibaum T (1991) Sharing actions and attributes in modal action logic. In Theoretical Aspects of Computer Software, volume 526 of Springer Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp 569–593

38.

Thimbleby H, Cairns P (2010) Reducing number entry errors: solving a widespread, serious problem. J R Soc Interf 7(51):1429–1439CrossRef

39.

Thimbleby H, Gimblett A (2011) Dependable keyed data entry for interactive systems, vol 45. ECEASST, Bolton

40.

Thimbleby H (2007) Interaction walkthrough: evaluation of safety critical interactive systems. In: Doherty G, Blandford A (eds Interactive Systems: Design, Specification and Verification, number 4323 in Springer Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp 52–66

41.

Thimbleby H (2007) Press on: principles of interaction programming. MIT Press, Cambridge

42.

Zhang J, Johnson TR, Patel VL, Paige DL, Kuboseb T (2003) Using usability heuristics to evaluate patient safety of medical devices. J Biomed Inform 36:23–30CrossRef

Title: Reusing models and properties in the analysis of similar interactive devices
Authors: Michael D. Harrison
José Creissac Campos
Paolo Masci
Publication date: 01-06-2015
Publisher: Springer London
Published in: Innovations in Systems and Software Engineering / Issue 2/2015
Print ISSN: 1614-5046
Electronic ISSN: 1614-5054
DOI: https://doi.org/10.1007/s11334-013-0201-3

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 2/2015

Is my configuration any good: checking usability in an interactive sensor-based activity monitor

Early detection of evolving system failures and temporal conflicts using parameterized formal specifications and bounded constraint-solving

Using PVS to support the analysis of distributed cognition systems

The benefits of formalising design guidelines: a case study on the predictability of drug infusion pumps

Preface

Premium Partner