Skip to main content
SpringerLink
Log in

State of the Art on Formal Methods for Interactive Systems

  • Chapter
  • First Online:
The Handbook of Formal Methods in Human-Computer Interaction

Part of the book series: Human–Computer Interaction Series ((HCIS))

Abstract

This chapter provides an overview of several formal approaches for the design, specification, and verification of interactive systems. For each approach presented, we describe how they support both modelling and verification activities. We also exemplify their use on a simple example in order to provide the reader with a better understanding of their basic concepts. It is important to note that this chapter is not self-contained and that the interested reader should get more details looking at the references provided. The chapter is organized to provide a historical perspective of the main contributions in the area of formal methods in the field of human–computer interaction. The approaches are presented in a semi-structured way identifying their contributions alongside a set of criteria. The chapter is concluded by a summary section organizing the various approaches in two summary tables reusing the criteria previously derived.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 259.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 329.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 329.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  • Abowd GD (1991) Formal aspects of human-computer interaction. Dissertation, University of Oxford

    Google Scholar 

  • Abowd GD, Dix AJ (1992) Giving undo attention. Interact Comput 4(3):317–342

    Article  Google Scholar 

  • Abowd GD, Wang H-M, Monk AF (1995) A formal technique for automated dialogue development. In: Proceedings of the 1st conference on designing interactive systems: processes, practices, methods, & techniques. ACM, pp 219–226

    Google Scholar 

  • Abrial J-R (1996) The B-book: Assigning Programs to Meanings. Cambridge University Press, New York

    Book  MATH  Google Scholar 

  • Acharya C, Thimbleby HW, Oladimeji P (2010) Human computer interaction and medical devices. In: Proceedings of the 2010 british computer society conference on human-computer interaction, pp 168–176

    Google Scholar 

  • Aït-Ameur Y, Girard P, Jambon F (1998a) A uniform approach for specification and design of interactive systems: the B method. In: Proceedings of the fifth international eurographics workshop on design, specification and verification of interactive systems, pp 51–67

    Google Scholar 

  • Aït-Ameur Y, Girard P, Jambon F (1998b) A uniform approach for the specification and design of interactive systems: the B method. In: Eurographics workshop on design, specification, and verification of interactive systems, pp 333–352

    Google Scholar 

  • Aït-Ameur Y, Girard P, Jambon F (1999) Using the B formal approach for incremental specification design of interactive systems. In: Engineering for human-computer interaction. Springer, pp 91–109

    Google Scholar 

  • Aït-Ameur Y (2000) Cooperation of formal methods in an engineering based software development process. In: Proceedings of integrated formal methods, second international conference, pp 136–155

    Google Scholar 

  • Aït-Ameur Y, Baron M, Girard P (2003a) Formal validation of HCI user tasks. In: Software engineering research and practice, pp 732–738

    Google Scholar 

  • Aït-Ameur Y, Baron M, Kamel N (2003b) Utilisation de Techniques Formelles dans la Modelisation d’Interfaces Homme-machine. Une Experience Comparative entre B et Promela/SPIN. In: 6th International Symposium on Programming and Systems, p 57–66

    Google Scholar 

  • Aït-Ameur Y, Kamel N (2004) A generic formal specification of fusion of modalities in a multimodal HCI. In: Building the information society. Springer, pp 415–420

    Google Scholar 

  • Aït-Ameur Y, Baron M (2004) Bridging the gap between formal and experimental validation approaches in HCI systems design: use of the event B proof based technique. In: International symposium on leveraging applications of formal methods, pp 74–80

    Google Scholar 

  • Aït-Ameur Y, Breholee B, Girard P, Guittet L, Jambon F (2004) Formal verification and validation of interactive systems specifications. In: Human error, safety and systems development. Springer, p 61–76

    Google Scholar 

  • Aït-Ameur Y, Baron M, Kamel N (2005a) Encoding a Process Algebra Using the Event B Method. Application to the Validation of User Interfaces. In: Proceedings of 2nd IEEE international symposium on leveraging applications of formal methods, p 1–17

    Google Scholar 

  • Aït-Ameur Y, Idir A-S, Mickael B (2005b) Modelisation et Validation formelles d’IHM: LOT 1 (LISI/ENSMA). Technical report. LISI/ENSMA

    Google Scholar 

  • Aït-Ameur Y, Aït-Sadoune I, Mota J-M, Baron M (2006) Validation et Verification Formelles de Systemes Interactifs Multi-modaux Fondees sur la Preuve. In: Proceedings of the 18th International Conference of the Association Francophone d’Interaction Homme-Machine, pp 123–130

    Google Scholar 

  • Aït-Ameur Y, Baron M (2006) Formal and experimental validation approaches in HCI systems design based on a shared event B model. Int J Softw Tools Technol Transf 8(6):547–563

    Article  Google Scholar 

  • Aït-Sadoune I, Aït-Ameur Y (2008) Animating event B models by formal data models. In: Proceedings of leveraging applications of formal methods, verification and validation, pp 37–55

    Google Scholar 

  • Aït-Ameur Y, Baron M, Kamel N, Mota J-M (2009) Encoding a process algebra using the event B method. Int J Softw Tools Technol Transfer 11(3):239–253

    Article  Google Scholar 

  • Aït-Ameur Y, Boniol F, Wiels V (2010a) Toward a wider use of formal methods for aerospace systems design and verification. Int J Softw Tools Technol Transf 12(1):1–7

    Article  Google Scholar 

  • Aït-Ameur Y, Aït-Sadoune I, Baron M, Mota J-M (2010b) Verification et Validation Formelles de Systemes Interactifs Fondees sur la Preuve: Application aux Systemes Multi-Modaux. J Interact Pers Syst 1(1):1–30

    Google Scholar 

  • Aït-Ameur Y, Gibson JP, Mery D (2014) On implicit and explicit semantics: integration issues in proof-based development of systems. In: Leveraging applications of formal methods, verification and validation. Specialized techniques and applications. Springer, p 604–618

    Google Scholar 

  • Barboni E, Ladry J-F, Navarre D, Palanque PA, Winckler M (2010) Beyond modelling: an integrated environment supporting co-execution of tasks and systems models. In: Proceedings of ACM EICS conference, pp 165–174

    Google Scholar 

  • Basnyat S, Palanque PA, Schupp B, Wright P (2007) Formal socio-technical barrier modelling for safety-critical interactive systems design. Saf Sci 45(5):545–565

    Article  Google Scholar 

  • Bass L, Little R, Pellegrino R, Reed S, Seacord R, Sheppard S, Szezur MR (1991) The ARCH model: seeheim revisited. In: User interface developpers’ workshop

    Google Scholar 

  • Bastide R, Palanque PA (1990) Petri net objects for the design, validation and prototyping of user-driven interfaces. In: IFIP INTERACT 1990 conference, pp 625–631

    Google Scholar 

  • Bastide R, Navarre D, Palanque PA (2002) A model-based tool for interactive prototyping of highly interactive applications. In: CHI extended abstracts, pp 516–517

    Google Scholar 

  • Bastide R, Navarre D, Palanque PA (2003) A tool-supported design framework for safety critical interactive systems. Interact Comput 15(3):309–328

    Article  Google Scholar 

  • Bastide R, Navarre D, Palanque PA, Schyn A, Dragicevic P (2004) A model-based approach for real-time embedded multimodal systems in military aircrafts. In: Proceedings of the 6th international conference on multimodal interfaces, pp 243–250

    Google Scholar 

  • Beck K (1999) Extreme programming explained: embrace change. Addison-Wesley

    Google Scholar 

  • Booch G (2005) The unified modelling language user guide. Pearson Education, India

    Google Scholar 

  • Bourguet-Rouger A (1988) External behaviour equivalence between two petri nets. In: Proceedings of concurrency. Lecture notes in computer science, vol 335. Springer, pp 237–256

    Google Scholar 

  • Bowen J, Reeves S (2006) Formal refinement of informal GUI design artefacts. In: Proceedings of 17th Australian software engineering conference, pp 221–230

    Google Scholar 

  • Bowen J, Reeves S (2007a) Formal models for informal GUI designs. Electr Notes Theor Comput Sci 183:57–72

    Article  Google Scholar 

  • Bowen J, Reeves S (2007b) using formal models to design user interfaces: a case study. In: Proceedings of the 21st British HCI group annual conference on HCI, pp 159–166

    Google Scholar 

  • Bowen J, Reeves S (2012) Modelling user manuals of modal medical devices and learning from the experience. In: Proceedings of ACM SIGCHI symposium on engineering interactive computing systems, pp 121–130

    Google Scholar 

  • Bowen J, Reeves S (2013) UI-design driven model-based testing. Innov Syst Softw Eng 9(3):201–215

    Article  Google Scholar 

  • Bowen J (2015) Creating models of interactive systems with the support of lightweight reverse-engineering tools. In: Proceedings of the 7th ACM SIGCHI symposium on engineering interactive computing systems, pp 110–119

    Google Scholar 

  • Boyer RS, Moore JS (1983) Proof-checking, theorem proving, and program verification. Technical report, DTIC document

    Google Scholar 

  • Brat G, Martinie C, Palanque P (2013) V&V of lexical, syntactic and semantic properties for interactive systems through model checking of formal description of dialog. In: Proceedings of the 15th international conference on human-computer interaction, pp 290–299

    Google Scholar 

  • Bumbulis P, Alencar PSC, Cowan DD, Lucena CJP (1995a) Combining formal techniques and prototyping in user interface construction and verification. In: Proceedings of 2nd eurographics workshop on design, specification, verification of interactive systems, pp 7–9

    Google Scholar 

  • Bumbulis P, Alencar PSC, Cowan DD, de Lucena CJP (1995b) A framework for machine-assisted user interface verification. In: Proceedings of the 4th international conference on algebraic methodology and software technology, pp 461–474

    Google Scholar 

  • Burkolter D, Weyers B, Kluge A, Luther W (2014) Customization of user interfaces to reduce errors and enhance user acceptance. Appl Ergon 45(2):346–353

    Article  Google Scholar 

  • Campos JC, Harrison MD (1997) Formally verifying interactive systems: a review. In: Proceedings of design, specification and verification of interactive systems, pp 109–124

    Google Scholar 

  • Campos JC (1999) Automated deduction and usability reasoning. Dissertatoin, University of York

    Google Scholar 

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

    Article  MATH  Google Scholar 

  • Campos JC, Harrison MD (2007) Considering context and users in interactive systems analysis. In: Proceedings of the joint working conferences on engineering interactive systems, pp 193–209

    Google Scholar 

  • Campos JC, Harrison MD (2008) Systematic analysis of control panel interfaces using formal tools. In: Interactive systems. Design, specification, and verification. Springer, pp 72–85

    Google Scholar 

  • Campos JC, Harrison MD (2009) Interaction engineering using the IVY tool. In: Proceedings of the 1st ACM SIGCHI symposium on engineering interactive computing systems, pp 35–44

    Google Scholar 

  • Campos JC, Harrison MD (2011) Modelling and analysing the interactive behaviour of an infusion pump. Electron Commun EASST 45

    Google Scholar 

  • Cauchi A, Gimblett A, Thimbleby HW, Curzon P, Masci P (2012a) Safer “5-key” number entry user interfaces using differential formal analysis. In: Proceedings of the 26th annual BCS interaction specialist group conference on people and computers, pp 29–38

    Google Scholar 

  • Cauchi A, Gimblett A, Thimbleby HW, Curzon P, Masci P (2012b) Safer “5-key” number entry user interfaces using differential formal analysis. In: Proceedings of the 26th annual BCS interaction specialist group conference on people and computers, pp 29–38

    Google Scholar 

  • Cauchi A, Oladimeji P, Niezen G, Thimbleby HW (2014) triangulating empirical and analytic techniques for improving number entry user interfaces. In: Proceedings of ACM SIGCHI symposium on engineering interactive computing systems, pp 243–252

    Google Scholar 

  • Champelovier D, Clerc X, Garavel H, Guerte Y, Lang F, Serwe W, Smeding G (2010) Reference manual of the LOTOS NT to LOTOS translator (version 5.0). INRIA/VASY

    Google Scholar 

  • Chen P (1976) The entity-relationship model—toward a unified view of data. ACM Trans Database Syst 1(1):9–36

    Article  Google Scholar 

  • Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2):244–263

    Article  MATH  Google Scholar 

  • Cofer D, Whalen M, Miller S (2008) Software model checking for avionics systems. In: Digital avionics systems conference, pp 1–8

    Google Scholar 

  • Cofer D (2010) Model checking: cleared for take-off. In: Model checking software. Springer, pp 76–87

    Google Scholar 

  • Cofer D (2012) Formal methods in the aerospace industry: follow the money. In: Proceedings of the 14th international conference on formal engineering methods: formal methods and software engineering. Springer, pp 2–3

    Google Scholar 

  • Cofer D, Gacek A, Miller S, Whalen MW, LaValley B, Sha L (2012) Compositional verification of architectural models. In: Proceedings of the 4th international conference on NASA formal methods. Springer, pp 126–140

    Google Scholar 

  • Combefis S, Pecheur C (2009) A bisimulation-based approach to the analysis of human-computer interaction. In: Proceedings of the 1st ACM SIGCHI symposium on engineering interactive computing systems, pp 101–110

    Google Scholar 

  • Combéfis S, Giannakopoulou D, Pecheur C, Feary M (2011a) A formal framework for design and analysis of human-machine interaction. In: Proceedings of the IEEE international conference on systems, man and cybernetics, pp 1801–1808

    Google Scholar 

  • Combéfis S, Giannakopoulou D, Pecheur C, Feary M (2011b) Learning system abstractions for human operators. In: Proceedings of the international workshop on machine learning technologies in software engineering, pp 3–10

    Google Scholar 

  • Combéfis S (2013) A formal framework for the analysis of human-machine interactions. Dissertation, Universite catholique de Louvain

    Google Scholar 

  • Cortier A, d’Ausbourg B, Aït-Ameur Y (2007) Formal validation of java/swing user interfaces with the event B method. In: Human-computer interaction. Interaction design and usability. Springer, pp 1062–1071

    Google Scholar 

  • Coutaz J (1987) PAC, an object oriented model for dialogue design. In: Bullinger H-J, Shackel B (eds) Human computer interaction INTERACT’87, pp 431–436

    Google Scholar 

  • Curzon P, Blandford A (2004) Formally justifying user-centred design rules: a case study on post-completion errors. Proc IFM 2004:461–480

    Google Scholar 

  • d’Ausbourg B (1998) Using model checking for the automatic validation of user interface systems. In: Proceedings of the fifth international eurographics workshop on the design, specification and verification of interactive systems, pp 242–260

    Google Scholar 

  • d’Ausbourg B, Seguin C, Durrieu G, Roche P (1998) Helping the automated validation process of user interfaces systems. In: Proceedings of the 20th international conference on software engineering, p 219–228

    Google Scholar 

  • d’Ausbourg B (2002) Synthetiser I’Intention d’un Pilote pour Definir de Nouveaux Équipements de Bord. In: Proceedings of the 14th French-speaking Conference on Human-computer Interaction, pp 145–152

    Google Scholar 

  • De Moura L, Owre S, Rueß H, Rushby J, Shankar N, Sorea M, Tiwari A (2004) SAL 2. In: Proceeidngs of computer aided verification, pp 496–500

    Google Scholar 

  • Degani A, Heymann M (2002) Formal verification of human-automation interaction. Hum Fact J Hum Fact Ergon Soc 44(1):28–43

    Article  MATH  Google Scholar 

  • Dey T (2011) A comparative analysis on modelling and implementing with MVC architecture. In: Proceedings of the international conference on web services computing, vol 1, pp 44–49

    Google Scholar 

  • Dix AJ (1988) Abstract, generic models of interactive systems. In: Proceedings of fourth conference of the british computer society human-computer interaction specialist group. University of Manchester, pp 63–77

    Google Scholar 

  • Dix AJ, Harrison MD, Cunciman R, Thimbleby HW (1987) interaction models and the principled design of interactive systems. In: Proceedings of the 1st European software engineering conference, pp 118–126

    Google Scholar 

  • Dix AJ (1991) Formal methods for Interactive systems. Academic Press, London

    Google Scholar 

  • Dix AJ (1995) Formal Methods. In: Monk A, Gilbert N (eds) Perspectives on HCI: diverse approaches. Academic Press, London, pp 9–43

    Google Scholar 

  • Dix AJ (2012) Formal methods. In: Soegaard M, Dam R (eds) Encyclopedia of human-computer interaction

    Google Scholar 

  • Doherty G, Campos JC, Harrison MD (1998) Representational reasoning and verification. Formal Aspects Comput 12:260–277

    Article  MATH  Google Scholar 

  • Duke DJ, Harrison MD (1993) Abstract interaction objects. Comput Graph Forum 12:25–36

    Article  Google Scholar 

  • Duke DJ, Harrison MD (1995) Event model of human-system interaction. Softw Eng J 10(1):3–12

    Article  Google Scholar 

  • Elder MC, Knight J (1995) specifying user interfaces for safety-critical medical systems. In: Proceedings of the 2nd annual international symposium on medical robotics and computer assisted surgery, pp 148–155

    Google Scholar 

  • Fahssi R, Martinie C, Palanque PA (2015) Enhanced task modelling for systematic identification and explicit representation of human errors. In: Proceedings of INTERACT, pp 192–212

    Google Scholar 

  • Fields B, Wright P, Harrison M (1995) Applying formal methods for human error tolerant design. In: Software engineering and human-computer interaction. Springer, pp 185–195

    Google Scholar 

  • Foley JD, Wallace VL (1974) The art of natural graphic man-machine conversation. Comput Graph 8(3):87

    Article  Google Scholar 

  • Garavel H, Graf S (2013) formal methods for safe and secure computer systems. Federal office for information security

    Google Scholar 

  • Garavel H, Lang F, Mateescu R, Serwe W (2013) CADP 2011: a toolbox for the construction and analysis of distributed processes. Int J Softw Tools Technol Transf 15(2):89–107

    Article  MATH  Google Scholar 

  • Gimblett A, Thimbleby HW (2010) User interface model discovery: towards a generic approach. In: Proceedings of the 2nd ACM SIGCHI symposium on engineering interactive computing system, EICS 2010, Berlin, Germany, pp 145–154

    Google Scholar 

  • Gimblett A, Thimbleby HW (2013) Applying theorem discovery to automatically find and check usability heuristics. In: Proceedings of the 5th ACM SIGCHI symposium on engineering interactive computing systems, pp 101–106

    Google Scholar 

  • Hallinger P, Crandall DP, Seong DNF (2000) Systems thinking/systems changing & a computer simulation for learning how to make school smarter. Adv Res Theor School Manag Educ Policy 1(4):15–24

    Google Scholar 

  • Hamilton D, Covington R, Kelly J, Kirkwood C, Thomas M, Flora-Holmquist AR, Staskauskas MG, Miller SP, Srivas MK, Cleland G, MacKenzie D (1995) Experiences in applying formal methods to the analysis of software and system requirements. In: Workshop on industrial-strength formal specification techniques, pp 30–43

    Google Scholar 

  • Hamon A, Palanque PA, Silva JL, Deleris Y, Barboni E (2013) Formal description of multi-touch interactions. In: Proceedings of the 5th ACM SIGCHI symposium on engineering interactive computing systems, pp 207–216

    Google Scholar 

  • Hardin DS, Hiratzka TD, Johnson DR, Wagner L, Whalen MW (2009) Development of security software: a high assurance methodology. In: Proceedings of 11th international conference on formal engineering methods, pp 266–285

    Google Scholar 

  • Harrison M, Thimbleby HW (eds) (1990) Formal methods in HCI. Cambridge University Press

    Google Scholar 

  • Harrison MD, Duke DJ (1995) A review of formalisms for describing interactive behaviour. In: software engineering and human-computer interaction. Springer, pp 49–75

    Google Scholar 

  • Harrison MD, Masci P, Campos JC, Curzon P (2013) Automated theorem proving for the systematic analysis of an infusion pump. Electron Commun EASST69

    Google Scholar 

  • Harrison MD, Campos JC, Masci P (2015) Reusing models and properties in the analysis of similar interactive devices, pp 95–111

    Google Scholar 

  • Hix D, Hartson RH (1993) Developing user interfaces: ensuring usability through product process. Wiley, New York

    MATH  Google Scholar 

  • ISO/IEC (1989) LOTOS—a formal description technique based on the temporal ordering of observational behaviour. International Standard 8807

    Google Scholar 

  • IEC ISO (2001) Enhancements to LOTOS (E-LOTOS). Int Stand 15437:2001

    Google Scholar 

  • ISO/IEC (2002) 13568, Information technology—Z formal specification notation—syntax, type system and semantics

    Google Scholar 

  • Jambon F, Girard P, Aït-Ameur Y (2001) Interactive system safety and usability enforced with the development process. In: Proceedings of 8th IFIP international conference on engineering for human-computer interaction, pp 39–56

    Google Scholar 

  • Kieras DE, Polson PG (1985) An approach to the formal analysis of user complexity. Int J Man Mach Stud 22:94–365

    Article  Google Scholar 

  • Kluge A, Greve J, Borisov N, Weyers B (2014) Exploring the usefulness of two variants of gaze-guiding-based dynamic job aid for performing a fixed sequence start up procedure after longer periods of non-use. Hum Fact Ergon 3(2):148–169

    Article  Google Scholar 

  • Knight JC, Kienzle DM (1992) Preliminary experience Using Z to specify a Safety-critical system. In: Proceedings of Z User workshop, pp 109–118

    Google Scholar 

  • Knight JC, Brilliant SS (1997) Preliminary evaluation of a formal approach to user interface specification. In: The Z formal specification notation. Springer, pp 329–346

    Google Scholar 

  • Knight JC, Fletcher PT, Hicks BR (1999) Tool support for production use of formal techniques. In: Proceedings of the world congress on formal methods in the development of computing systems, pp 242–251

    Google Scholar 

  • Kummer O, Wienberg F, Duvigneau M, Köhler M, Moldt D, Rölke H (2000) Renew–the reference net workshop. In: Proceedings of 21st international conference on application and theory of petri nets-tool demonstrations, pp 87–89

    Google Scholar 

  • Kummer O (2002) Referenznetze. Universität Hamburg, Disseration

    Google Scholar 

  • Li K-Y, Oladimeji P, Thimbleby HW (2015) Exploring the effect of pre-operational priming intervention on number entry errors. In: Proceedings of the 33rd annual ACM conference on human factors in computing systems, pp 1335–1344

    Google Scholar 

  • Loer K, Harrison MD (2000) formal interactive systems analysis and usability inspection methods: two incompatible worlds? In: Interactive systems: design, specification, and verification, pp 169–190

    Google Scholar 

  • Loer K, Harrison MD (2002) Towards usable and relevant model checking techniques for the analysis of dependable interactive systems. In: Proceedings of automated software engineering, pp 223–226

    Google Scholar 

  • Loer K, Harrison MD (2006) An integrated framework for the analysis of dependable interactive systems (IFADIS): its tool support and evaluation. Autom Softw Eng 13(4):469–496

    Article  Google Scholar 

  • Lutz RR (2000) Software engineering for safety: a roadmap. In: Proceedings of the conference on the future of software engineering, pp 213–226

    Google Scholar 

  • Mancini R (1997) Modelling interactive computing by exploiting the undo. Dissertation, University of Rome

    Google Scholar 

  • Markopoulos P (1995) On the expression of interaction properties within an interactor model. In: Interactive systems: design, specification, and verification, pp 294–310

    Google Scholar 

  • Markopoulos P, Rowson J, Johnson P (1996) Dialogue modelling in the framework of an interactor model. In: Pre-conference proceedings of design specification and verification of interactive systems, Namur, Belgium, vol 44

    Google Scholar 

  • Markopoulos P (1997) A compositional model for the formal specification of user interface software. Dissertation, University of London

    Google Scholar 

  • Markopoulos P, Johnson P, Rowson J (1998) Formal architectural abstractions for interactive software. Int J Hum Comput Stud 49(5):675–715

    Article  Google Scholar 

  • Martinie C, Palanque PA, Navarre D, Winckler M, Poupart E (2011) Model-based training: an approach supporting operability of critical interactive systems. In: Proceedings of ACM EICS conference, pp 53–62

    Google Scholar 

  • Martinie C, Palanque PA, Winckler M (2011) Structuring and composition mechanisms to address scalability issues in task models. In: Proceedings of IFIP TC 13 INTERACT, pp 589–609

    Google Scholar 

  • Martinie C, Navarre D, Palanque PA (2014) A multi-formalism approach for model-based dynamic distribution of user interfaces of critical interactive systems. Int J Hum Comput Stud 72(1):77–99

    Article  Google Scholar 

  • Masci P, Ruksenas R, Oladimeji P, Cauchi A, Gimblett A, Li Y, Curzon P, Thimbleby H (2011) On formalising interactive number entry on infusion pumps. Electron Commun the EASST 45

    Google Scholar 

  • Masci P, Ayoub A, Curzon P, Harrison MD, Lee I, Thimbleby H (2013a) Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example. In: Proceedings of the 5th ACM SIGCHI symposium on engineering interactive computing systems pp 81–90

    Google Scholar 

  • Masci P, Zhang Y, Jones PL, Oladimeji P, D’Urso E, Bernardeschi C, Curzon P, Thimbleby H (2014a) Formal verification of medical device user interfaces using PVS. In: Proceedings of the 17th international conference on fundamental approaches to software engineering. Springer, pp 200–214

    Google Scholar 

  • Masci P, Zhang Y, Jones PL, Oladimeji P, D’Urso E, Bernardeschi C, Curzon P, Thimbleby H (2014b) Combining PVSio with stateflow. In: Proceedings of NASA formal methods—6th international symposium, pp 209–214

    Google Scholar 

  • Masci P, Ruksenas R, Oladimeji P, Cauchi A, Gimblett A, Li AY, Curzon P, Thimbleby HW (2015) The benefits of formalising design guidelines: a case study on the predictability of drug infusion pumps. Innov Syst Softw Eng 11(2):73–93

    Article  Google Scholar 

  • Mateescu R, Thivolle D (2008) A model checking language for concurrent value-passing systems. In: Cuellar J, Maibaum T, Sere K (eds) Proceedings of the 15th international symposium on formal methods. Springer, pp 148–164

    Google Scholar 

  • Merriam NA, Harrison MD (1996) Evaluating the interfaces of three theorem proving assistants. In: Proceedings of DSV-IS conference. Springer, pp 330–346

    Google Scholar 

  • Miller SP, Tribble AC, Whalen MW, Heimdahl MPE (2006) Proving the shalls. Int J Softw Tools Technol Transf 8(4–5):303–319

    Article  Google Scholar 

  • Miller SP (2009) Bridging the gap between model-based development and model checking. In: Tools and algorithms for the construction and analysis of systems. Springer, pp 443–453

    Google Scholar 

  • Miller SP, Whalen MW, Cofer DD (2010) Software model checking takes off. Commun ACM 53(2):58–64

    Article  Google Scholar 

  • Milner R (1980) A calculus of communicating systems. Springer

    Google Scholar 

  • Moher T, Dirda V, Bastide R (1996) A bridging framework for the modelling of devices, users, and interfaces. Technical report

    Google Scholar 

  • Murugesan A, Whalen MW, Rayadurgam S, Heimdahl MPE (2013) Compositional verification of a medical device system. In: Proceedings of the 2013 ACM SIGAda annual conference on high integrity language technology, pp 51–64

    Google Scholar 

  • Navarre D, Palanque PA, Paterno F, Santoro C, Bastide R (2001) A tool suite for integrating task and system models through scenarios. In: Proceedings of the 8th international workshop on interactive systems: design, specification, and verification-revised papers. Springer, pp 88–113

    Google Scholar 

  • Navarre D, Palanque PA, Bastide R, Schyn A, Winckler M, Nedel LP, Freitas CMDS (2005) A formal description of multimodal interaction techniques for immersive virtual reality applications. In: Proceedings of the 2005 IFIP TC13 international conference on human-computer interaction. Springer, pp 170–183

    Google Scholar 

  • Navarre D, Palanque PA, Basnyat S (2008) A formal approach for user interaction reconfiguration of safety critical interactive systems. In: Computer safety, reliability, and security. Springer, pp 373–386

    Google Scholar 

  • Navarre D, Palanque PA, Ladry J-F, Barboni E (2009) ICOs: a model-based user interface description technique dedicated to interactive systems addressing usability, reliability and scalability. ACM Trans Comput Hum Interact 16(4):1–56

    Article  Google Scholar 

  • Niwa Y, Takahashi M, Kitamura M (2001) The design of human-machine interface for accident support in nuclear power plants. Cogn Technol Work 3(3):161–176

    Article  Google Scholar 

  • Oladimeji P, Thimbleby HW, Cox AL (2011) number entry interfaces and their effects on error detection. In: Proceedings of human-computer interaction—INTERACT 2011—13th IFIP TC 13 international conference, pp 178–185

    Google Scholar 

  • Oladimeji P, Thimbleby HW, Cox AL (2013) A performance review of number entry interfaces. In: Proceedings of human-computer interaction—INTERACT 2013—14th IFIP TC 13 international conference, pp 365–382

    Google Scholar 

  • Oliveira R, Dupuy-Chessa S, Calvary G (2014) Formal verification of UI using the power of a recent tool suite. In: Proceedings of the ACM SIGCHI symposium on engineering interactive computing systems, pp 235–240

    Google Scholar 

  • Oliveira R (2015) Formal specification and verification of interactive systems with plasticity: applications to nuclear-plant supervision. Dissertation, Université Grenoble Alpes

    Google Scholar 

  • Oliveira R, Dupuy-Chessa S, Calvary G (2015a) Verification of plastic interactive systems. i-com 14(3):192–204

    Article  Google Scholar 

  • Oliveira R, Dupuy-Chessa S, Calvary G (2015b) Equivalence checking for comparing user interfaces. In: Proceedings of the 7th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, p 266–275

    Google Scholar 

  • Oliveira R, Dupuy-Chessa S, Calvary G (2015c) Plasticity of user interfaces: formal verification of consistency. In: Proceedings of the 7th ACM SIGCHI symposium on engineering interactive computing systems, pp 260–265

    Google Scholar 

  • OMG (2010) Systems modelling language (OMG SysML™), version 1.2

    Google Scholar 

  • Palanque PA, Bastide R, Sengès V (1995) Validating interactive system design through the verification of formal task and system models. In: Proceedings of IFIP WG 2.7 conference on engineering human computer interaction, pp 189–212

    Google Scholar 

  • Palanque PA, Bastide R (1995) Petri net based design of user-driven interfaces using the interactive cooperative objects formalism. In: Interactive systems: design, specification, and verification. Springer, pp 383–400

    Google Scholar 

  • Palanque PA, Bastide R, Senges V (1996) Validating interactive system design through the verification of formal task and system models. In: Proceedings of the IFIP TC2/WG2.7 working conference on engineering for human-computer interaction, pp 189–212

    Google Scholar 

  • Palanque PA, Paternó F (eds) (1997) Formal methods in HCI. Springer

    Google Scholar 

  • Palanque PA, Bastide R, Paternó F (1997) Formal specification as a tool for objective assessment of safety-critical interactive systems. In: Proceedings of the IFIP TC13 international conference on human-computer interaction, pp 323–330

    Google Scholar 

  • Palanque PA, Farenc C, Bastide R (1999) Embedding ergonomic rules as generic requirements in a formal development process of interactive software. In: Human-computer interaction INTERACT’99: IFIP TC13 international conference on human-computer interaction, pp 408–416

    Google Scholar 

  • Palanque PA, Winckler M, Ladry J-F, ter Beek M, Faconti G, Massink M (2009) A formal approach supporting the comparative predictive assessment of the interruption-tolerance of interactive systems. In: Proceedings of ACM EICS 2009 conference, pp 46–55

    Google Scholar 

  • Payne SJ, Green TRG (1986) Task-action grammars: a model of mental representation of task languages. Hum Comput Interact 2(2):93–133

    Article  Google Scholar 

  • Park D (1981) Concurrency and automata on infinite sequences. In: Proceedings of the 5th GI-conference on theoretical computer science. Springer, pp 167–183

    Google Scholar 

  • Parnas DL (1969) On the use of transition diagrams in the design of a user interface for an interactive computer system. In: Proceedings of the 24th national ACM conference, pp 379–385

    Google Scholar 

  • Paternó F, Faconti G (1992) On the use of LOTOS to describe graphical interaction. People and computers VII. Cambridge University Press, pp 155–155

    Google Scholar 

  • Paternó F (1994) A Theory of User-interaction Objects. J Vis Lang Comput 5(3):227–249

    Article  Google Scholar 

  • Paternó F, Mezzanotte M (1994) Analysing MATIS by interactors and ACTL. Technical report

    Google Scholar 

  • Paternó F, Mezzanotte M (1996) Formal verification of undesired behaviours in the CERD case study. In: Proceedings of the IFIP TC2/WG2.7 working conference on engineering for human-computer interaction, pp 213–226

    Google Scholar 

  • Paternó F (1997) Formal reasoning about dialogue properties with automatic support. Interact Comput 9(2):173–196

    Article  Google Scholar 

  • Paternó F, Mancini C, Meniconi S (1997) ConcurTaskTrees: a diagrammatic notation for specifying task models. In: Proceedings of the IFIP tc13 international conference on human-computer interaction, pp 362–369

    Google Scholar 

  • Paternó F, Santoro C (2001). Integrating Model checking and HCI tools to help designers verify user interface properties. In: Proceedings of the 7th international conference on design, specification, and verification of interactive systems. Springer, pp 135–150

    Google Scholar 

  • Paternó F, Santoro C (2003) Support for reasoning about interactive systems through human-computer interaction designers’ representations. Comput J 46(4):340–357

    Article  MATH  Google Scholar 

  • Petri CA (1962) Kommunikation mit Automaten. Dissertation, University of Bonn

    Google Scholar 

  • Pfaff G, Hagen P (eds) (1985) Seeheim workshop on user interface management systems. Springer, Berlin

    MATH  Google Scholar 

  • Reeve G, Reeves S (2000) μCharts and Z: Hows, Whys, and Wherefores. In: Integrated formal methods: second international conference. Springer, Berlin

    Google Scholar 

  • Reisner P (1981) Formal grammar and human factors design of an interactive graphics system. IEEE Trans Softw Eng 7(2):229–240

    Article  Google Scholar 

  • Schwaber K (2004) Agile project management with scrum. Microsoft Press

    Google Scholar 

  • Sifakis J (1979) Use of petri nets for performance evaluation. In: Beilner H, Gelenbe E (eds), Proceedings of 3rd international symposium on modelling and performance of computer systems

    Google Scholar 

  • Shepherd A (1989) Analysis and training in information technology tasks. In Diaper D (ed) Task analysis for human-computer interaction, pp 15–55

    Google Scholar 

  • Sufrin B (1982) Formal specification of a display-oriented text editor. Sci Comput Program 1:157–202

    Article  MATH  Google Scholar 

  • Sousa M, Campos J, Alves M, Harrison M, (2014) Formal verification of safety-critical user interfaces: a space system case study. In: Proceedings of the AAAI spring symposium on formal verification and modelling in human machine systems, pp 62–67

    Google Scholar 

  • Spivey MJ (1989) The Z notation: a reference manual. Prentice-Hall, Upper Saddle River

    MATH  Google Scholar 

  • Strunk EA, Yin X, Knight JC (2005) ECHO: a practical approach to formal verification. In: Proceedings of the 10th international workshop on formal methods for industrial critical systems, pp 44–53

    Google Scholar 

  • Stückrath J, Weyers, B (2014) Lattice-extended coloured petri net rewriting for adaptable user interface models. Electron Commun EASST 67(13):13 pages. http://journal.ub.tu-berlin.de/eceasst/article/view/941/929

  • Thevenin D, Coutaz J (1999) Plasticity of user interfaces: framework and research agenda. In: Sasse A, Johnson C (eds) Proceedings of interact, pp 110–117

    Google Scholar 

  • Thimbleby H (2007a) Interaction walkthrough: evaluation of safety critical interactive systems. In: interactive systems. design, specification, and verification. Springer, pp 52–66

    Google Scholar 

  • Thimbleby H (2007b) User-centered methods are insufficient for safety critical systems. In: 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. Springer, pp 1–20

    Google Scholar 

  • Thimbleby H, Gow J (2008) Applying graph theory to interaction design. In: Gulliksen J, Harning MB, Palanque P, Veer GC, Wesson J (eds) Engineering interactive systems. Springer, pp 501–519

    Google Scholar 

  • Thimbleby H (2010) Think! interactive systems need safety locks. J Comput Inf Technol 18(4):349–360

    Article  Google Scholar 

  • Thimbleby HW, Gimblett A (2011) Dependable keyed data entry for interactive systems. Electron Commun EASST 45

    Google Scholar 

  • Tu H, Oladimeji P, Li KY, Thimbleby HW, Vincent C (2014) The effects of number-related factors on entry performance. In: Proceedings of the 28th international BCS human computer interaction conference, pp 246–251

    Google Scholar 

  • Turchin P, Skii R (2006) History and mathematics. URSS

    Google Scholar 

  • Turner CS (1993) An investigation of the therac-25 accidents. Computer 18:9I62/93, 0700–001830300

    Google Scholar 

  • van Glabbeek RJ, Weijland WP (1996) Branching time and abstraction in bisimulation semantics. J ACM 43(3):555–600

    Article  MathSciNet  MATH  Google Scholar 

  • Wang H-W, Abowd G (1994) A tabular interface for automated verification of event-based dialogs. Technical report. DTIC Document

    Google Scholar 

  • Wegner P (1997) Why interaction is more powerful than algorithms. Commun ACM 40(5):80–91

    Article  Google Scholar 

  • Weyers B, Baloian N, Luther W (2009) Cooperative creation of concept keyboards in distributed learning environments. In: Borges MRS, Shen W, Pino JA, Barthès J-P, Lou J, Ochoa SF, Yong J (eds), Proceedings of 13th international conference on CSCW in design, pp 534–539

    Google Scholar 

  • Weyers B, Luther W, Baloian N (2010a) Interface creation and redesign techniques in collaborative learning scenarios. J Futur Gener Comput Syst 27(1):127–138

    Article  Google Scholar 

  • Weyers B, Burkolter D, Kluge A, Luther W (2010) User-centered interface reconfiguration for error reduction in human-computer interaction. In: Proceedings of the third international conference on advances in human-oriented and personalized mechanisms, technologies and services, pp 52–55

    Google Scholar 

  • Weyers B, Luther W, Baloian N (2012a) Cooperative reconfiguration of user interfaces for learning cryptographic algorithms. J Inf Technol Decis Mak 11(6):1127–1154

    Article  Google Scholar 

  • Weyers B (2012) Reconfiguration of user interface models for monitoring and control of human-computer systems. Dissertation, University of Duisburg-Essen. Dr. Hut, Berlin

    Google Scholar 

  • Weyers B, Burkolter D, Luther W, Kluge A (2012b) Formal modelling and reconfiguration of user interfaces for reduction of human error in failure handling of complex systems. J Hum Comput Interact 28(1):646–665

    Article  Google Scholar 

  • Weyers B, Borisov N, Luther W (2014) Creation of adaptive user interfaces through reconfiguration of user interface models using an algorithmic rule generation approach. Int J Adv Intell Syst 7(1&2):302–336

    Google Scholar 

  • Weyers B (2015) FILL: formal description of executable and reconfigurable models of interactive systems. In: Proceedings of the workshop on formal methods in human computer interaction, pp 1–6

    Google Scholar 

  • Weyers B, Frank B, Bischof K, Kluge A (2015) Gaze guiding as support for the control of technical systems. Int J Inf Syst Crisis Resp Manag 7(2):59–80

    Article  Google Scholar 

  • Whalen M, Cofer D, Miller S, Krogh BH, Storm W (2008) Integration of formal analysis into a model-based software development process. In: Formal methods for industrial critical systems. Springer, pp 68–84

    Google Scholar 

  • Yin X, Knight JC, Nguyen EA, Weimer W (2008) Formal verification by reverse synthesis. In: Proceedings of international conference on computer safety, reliability, and security, pp 305–319

    Google Scholar 

  • Yin X, Knight J, Weimer W (2009a) Exploiting refactoring in formal verification. In: Proceedings of dependable systems & networks, pp 53–62

    Google Scholar 

  • Yin X, Knight JC, Weimer W (2009b) Exploiting refactoring in formal verification. In: Proceedings of the 2009 IEEE/IFIP international conference on dependable systems and networks, pp 53–62

    Google Scholar 

  • Yin X, Knight JC (2010) Formal verification of large software systems. In: Proceedings of second NASA formal methods symposium, pp 192–201

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IRIT— MACAO Group, University of Toulouse 3—Paul Sabatier, Toulouse, France

    Raquel Oliveira

  2. IRIT— Interactive Critical Systems Group, University of Toulouse 3—Paul Sabatier, Toulouse, France

    Philippe Palanque

  3. Visual Computing Institute—Virtual Reality & Immersive Visualization, RWTH Aachen University, Aachen, Germany

    Benjamin Weyers

  4. Department of Computer Science, The University of Waikato, Hamilton, New Zealand

    Judy Bowen

  5. School of Computer Science, University of Birmingham, Birmingham, UK

    Alan Dix

  6. Talis Ltd., Birmingham, UK

    Alan Dix

Authors
  1. Raquel Oliveira
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Philippe Palanque
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Benjamin Weyers
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Judy Bowen
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Alan Dix
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Benjamin Weyers .

Editor information

Editors and Affiliations

  1. Visual Computing Institute—Virtual Reality & Immersive Visualization, RWTH Aachen University, Aachen, Germany

    Benjamin Weyers

  2. Department of Computer Science, The University of Waikato, Hamilton, New Zealand

    Judy Bowen

  3. School of Computer Science, University of Birmingham, Birmingham, United Kingdom

    Alan Dix

  4. Universite de Toulouse, ICS-IRIT, Toulouse, France

    Philippe Palanque

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Cite this chapter

Oliveira, R., Palanque, P., Weyers, B., Bowen, J., Dix, A. (2017). State of the Art on Formal Methods for Interactive Systems. In: Weyers, B., Bowen, J., Dix, A., Palanque, P. (eds) The Handbook of Formal Methods in Human-Computer Interaction. Human–Computer Interaction Series. Springer, Cham. https://doi.org/10.1007/978-3-319-51838-1_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-51838-1_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-51837-4

  • Online ISBN: 978-3-319-51838-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation