Preface; References; Contents; Contributors; Introduction; 1 State of the Art on Formal Methods for Interactive Systems; Abstract; 1.1 Introduction; 1.2 Modelling and Formal Modelling; 1.3 Verification and Validation; 1.4 Criteria to Describe and Analyse the State of the Art; 1.5 Modelling and Verification; 1.6 Succinct Presentation of the Approaches; 1.6.1 Abowd et al. (USA 1991-1995); 1.6.1.1 Modelling; 1.6.1.2 Verification; 1.6.2 Dix et al. (United Kingdom 1985-1995); 1.6.2.1 Modelling; 1.6.2.2 Verification; 1.6.3 Paternò et al. (Italy 1990-2003); 1.6.3.1 Modelling; 1.6.3.2 Verification

1.6.4 Markopoulos et al. (United Kingdom 1995-1998)1.6.4.1 Modelling; 1.6.4.2 Verification; 1.6.5 Duke and Harrison et al. (United Kingdom 1993-1995); 1.6.5.1 Modelling; 1.6.5.2 Verification; 1.6.6 Campos et al. (Portugal 1997-2015); 1.6.6.1 Modelling; 1.6.6.2 Verification; 1.6.7 d'Ausbourg et al. (France 1996-2002); 1.6.7.1 Modelling; 1.6.7.2 Verification; 1.6.8 Bumbulis et al. (Canada 1995-1996); 1.6.8.1 Modelling; 1.6.8.2 Verification; 1.6.9 Oliveira et al. (France 2012-2015); 1.6.9.1 Modelling; 1.6.9.2 Verification; 1.6.10 Knight et al. (USA 1992-2010); 1.6.10.1 Modelling

1.6.10.2 Verification1.6.11 Miller et al. (USA 1995-2013); 1.6.11.1 Modelling; 1.6.11.2 Verification; 1.6.12 Loer and Harrison et al. (Germany 2000-2006); 1.6.12.1 Modelling; 1.6.12.2 Verification; 1.6.13 Thimbleby et al. (United Kingdom 1987-2015); 1.6.13.1 Modelling; 1.6.13.2 Verification; 1.6.14 Palanque et al. (France 1990-2015); 1.6.14.1 Modelling; 1.6.14.2 Verification; 1.6.15 Aït-Ameur et al. (France 1998-2014); 1.6.15.1 Modelling; 1.6.15.2 Verification; 1.6.16 Bowen and Reeves (New Zealand 2005-2015); 1.6.16.1 Modelling; 1.6.16.2 Verification; 1.6.17 Weyers et al. (Germany 2009-2015)

1.6.17.1 Modelling1.6.17.2 Model Reconfiguration and Formal Rewriting; 1.6.18 Combéfis et al. (Belgium 2009-2013); 1.6.18.1 Modelling; 1.6.18.2 Verification; 1.6.19 Synthesis; 1.6.20 Summary; References; 2 Topics of Formal Methods in HCI; 2.1 Introduction; 2.2 Describing the Human User of Interactive Systems; 2.3 Formal Methods for Specific Types of Interactive Systems; 2.4 Descriptions of the Modelling Process and Supporting Tools; 2.5 Summary; References; 3 Trends and Gaps; Abstract; 3.1 Introduction; 3.2 HCI Trends; 3.2.1 Changing User Interaction; 3.2.2 Changing Technology

3.2.3 Changing Design and Development3.3 Formalising Interaction: What and How; 3.3.1 What-Actors and Entities; 3.3.2 What-Levels of Abstraction; 3.3.3 Who and When (and Why?); 3.3.4 How; 3.4 Summary; References; 4 Case Studies; Abstract; 4.1 Introduction; 4.2 Case Study 1-Control of a Nuclear Power Plant; 4.2.1 Formalization of the Simplified BWR Design; 4.2.2 Standard Operating Procedures; 4.2.3 Automation; 4.2.4 Connection with Formal Methods; 4.3 Case Study 2-Arrival Manager Within an Air Traffic Control Workstation; 4.3.1 Air Traffic Controller Tasks