The Handbook of Formal Methods in Human-Computer Interaction (eBook)

Benjamin Weyers is a Senior Researcher at the Virtual Reality and Immersive Visualization Group at RWTH Aachen University, Germany. Benjamin is strongly involved in the FET-flagship project “The Human Brain Project” and co-leads the work package on interactive visualization. He studied Computer Science at the University of Duisburg-Essen and received his doctorate with the Computer Graphics and Scientific Computing Group at the University of Duisburg-Essen.  His research interests include human-computer interaction (HCI), formal modelling, information visualization and virtual reality (VR). Judy Bowen is a Senior Lecturer at the University of Waikato in New Zealand. For the past ten years she has been working in the area of formal modelling for interactive systems, specifically safety-critical interactive systems. Her work includes projects that consider safety-properties of systems, contexts of use for non-context aware systems and the use of technology in hazardous work-places and environments. Alan Dix is a Professor in the Human–Computer Interaction Centre at the University of Birmingham and a Senior Researcher at Talis. He has worked in HCI for over thirty years and his research has included foundational work on formal methods in HCI, some of the earliest work on privacy in HCI and the ethics of machine learning, and more recently has included learning analytics, IT and data issues for marginal communities as well as walking one thousand miles around Wales.  He runs the twice-yearly Tiree Tech Wave.  Philippe Palanque is a Professor of Computer Science at the University of Toulouse and leads the ICS Research Group. Since the late 80's, he has worked on the development and application of formal description techniques for interactive systems. The main aim of his research has been to address Usability, Safety and Dependability in order to build trustable safety-critical Interactive Systems.

Preface 6
References 8
Contents 10
Contributors 13
Introduction 15
1 State of the Art on Formal Methods for Interactive Systems 16
Abstract 16
1.1 Introduction 17
1.2 Modelling and Formal Modelling 18
1.3 Verification and Validation 19
1.4 Criteria to Describe and Analyse the State of the Art 22
1.5 Modelling and Verification 23
1.6 Succinct Presentation of the Approaches 23
1.6.1 Abowd et al. (USA 1991–1995) 25
1.6.1.1 Modelling 25
1.6.1.2 Verification 26
1.6.2 Dix et al. (United Kingdom 1985–1995) 27
1.6.2.1 Modelling 27
1.6.2.2 Verification 28
1.6.3 Paternò et al. (Italy 1990–2003) 28
1.6.3.1 Modelling 28
1.6.3.2 Verification 29
1.6.4 Markopoulos et al. (United Kingdom 1995–1998) 30
1.6.4.1 Modelling 30
1.6.4.2 Verification 30
1.6.5 Duke and Harrison et al. (United Kingdom 1993–1995) 31
1.6.5.1 Modelling 31
1.6.5.2 Verification 32
1.6.6 Campos et al. (Portugal 1997–2015) 33
1.6.6.1 Modelling 33
1.6.6.2 Verification 33
1.6.7 d’Ausbourg et al. (France 1996–2002) 34
1.6.7.1 Modelling 34
1.6.7.2 Verification 34
1.6.8 Bumbulis et al. (Canada 1995–1996) 35
1.6.8.1 Modelling 35
1.6.8.2 Verification 36
1.6.9 Oliveira et al. (France 2012–2015) 36
1.6.9.1 Modelling 36
1.6.9.2 Verification 37
1.6.10 Knight et al. (USA 1992–2010) 38
1.6.10.1 Modelling 38
1.6.10.2 Verification 39
1.6.11 Miller et al. (USA 1995–2013) 39
1.6.11.1 Modelling 39
1.6.11.2 Verification 41
1.6.12 Loer and Harrison et al. (Germany 2000–2006) 41
1.6.12.1 Modelling 41
1.6.12.2 Verification 42
1.6.13 Thimbleby et al. (United Kingdom 1987–2015) 43
1.6.13.1 Modelling 43
1.6.13.2 Verification 44
1.6.14 Palanque et al. (France 1990–2015) 45
1.6.14.1 Modelling 45
1.6.14.2 Verification 46
1.6.15 Aït-Ameur et al. (France 1998–2014) 47
1.6.15.1 Modelling 47
1.6.15.2 Verification 48
1.6.16 Bowen and Reeves (New Zealand 2005–2015) 49
1.6.16.1 Modelling 49
1.6.16.2 Verification 51
1.6.17 Weyers et al. (Germany 2009–2015) 52
1.6.17.1 Modelling 52
1.6.17.2 Model Reconfiguration and Formal Rewriting 53
1.6.18 Combéfis et al. (Belgium 2009–2013) 54
1.6.18.1 Modelling 54
1.6.18.2 Verification 55
1.6.19 Synthesis 56
1.6.20 Summary 56
References 58
2 Topics of Formal Methods in HCI 69
2.1 Introduction 69
2.2 Describing the Human User of Interactive Systems 71
2.3 Formal Methods for Specific Types of Interactive Systems 72
2.4 Descriptions of the Modelling Process and Supporting Tools 74
2.5 Summary 75
References 75
3 Trends and Gaps 77
Abstract 77
3.1 Introduction 78
3.2 HCI Trends 78
3.2.1 Changing User Interaction 79
3.2.2 Changing Technology 83
3.2.3 Changing Design and Development 85
3.3 Formalising Interaction: What and How 87
3.3.1 What—Actors and Entities 87
3.3.2 What—Levels of Abstraction 89
3.3.3 Who and When (and Why?) 90
3.3.4 How 92
3.4 Summary 95
References 97
4 Case Studies 101
Abstract 101
4.1 Introduction 102
4.2 Case Study 1—Control of a Nuclear Power Plant 103
4.2.1 Formalization of the Simplified BWR Design 105
4.2.2 Standard Operating Procedures 109
4.2.3 Automation 111
4.2.4 Connection with Formal Methods 112
4.3 Case Study 2—Arrival Manager Within an Air Traffic Control Workstation 113
4.3.1 Air Traffic Controller Tasks 115
4.3.2 User Interface of the Air Traffic Control Radar Screen 115
4.3.3 Connection with Formal Methods 115
4.4 Case Study 3—Interactive Aircraft Cockpits 117
4.4.1 The FCUS Application 118
4.4.2 Pilots Tasks 121
4.4.3 Connection with Formal Methods 122
4.5 Case Study 4—Interactive Systems in Rural Areas—Maintenance of Wind Turbines 122
4.5.1 Tilley—A Community Wind Turbine 123
4.5.2 Connection with Formal Methods 125
4.6 Case Study 5—Interactive Systems in Public Areas—Interactive Public Displays 126
4.6.1 Community Information Displays—The Internet-Enabled Shop-Open Sign 127
4.6.2 Connection with Formal Methods 131
References 132
Modeling, Execution and Simulation 134
5 Visual and Formal Modeling of Modularized and Executable User Interface Models 135
5.1 Introduction 135
5.2 Overview and Terminology 137
5.3 Background 138
5.4 Architecture 140
5.5 Modeling---Formalization 144
5.5.1 Formal Interaction Logic Language---FILL 144
5.5.2 Component-Based and Multidevice Models 150
5.5.3 Transformation to Reference Nets 153
5.6 Modeling and Editing 162
5.6.1 UIEditor---Creation 162
5.6.2 UIEditor---Execution 163
5.7 Case Study 164
5.8 Conclusion 168
References 168
6 Combining Models for Interactive System Modelling 171
6.1 Introduction 171
6.2 Related Work 172
6.3 Background 174
6.3.1 Presentation Model 176
6.3.2 Presentation Interaction Model 178
6.3.3 Presentation Model Relation 179
6.3.4 Specification 179
6.3.5 ?Charts 180
6.3.6 Combining the Models 180
6.4 The Nuclear Power Plant Case Study 181
6.4.1 Benefits of Combining the Models 189
6.5 Conclusion 191
References 191
7 Activity Modelling for Low-Intention Interaction 193
Abstract 193
7.1 Introduction 194
7.2 What Is Low-Intention Interaction? 195
7.2.1 Intentional and Low-Intention Interaction 195
7.2.2 The Intentional Spectrum 196
7.2.3 Examples of Low-Intention Interaction 196
7.2.4 Intentional Shifts 197
7.2.5 Two Tasks 198
7.3 Frameworks and Paradigms 200
7.3.1 Design Concepts 200
7.3.2 Low Intention and Naturalness 202
7.3.3 Architecture and Modelling 203
7.4 Modelling Low-Intention Interactions 205
7.4.1 Modelling Process 205
7.4.2 Car Courtesy Lights 206
7.5 Into Practice: The Internet-Enabled Shop Open Sign 208
7.5.1 Concept—The Chip Van That Tweets 208
7.5.2 TireeOpen—The Internet-Enabled Open Sign 209
7.6 Further Design Considerations for Low Intention 213
7.6.1 User Models 214
7.6.2 Privacy 214
7.6.3 Can Task Models Help? 215
7.7 Discussion 216
Acknowledgements 217
References 217
8 Modelling the User 221
8.1 Introduction 221
8.1.1 Between Demonic and Angelic Behaviour 222
8.2 Verifying Systems with a User Model 224
8.2.1 Defining Systems Involving User Models 224
8.2.2 System Verification Involving User Models 227
8.2.3 Instantiating a Generic User Model 228
8.3 A Simple Model of Cognitively Plausible Behaviour 229
8.3.1 Non-determinism 230
8.3.2 Reactive Behaviour 231
8.3.3 Goal-Based Behaviour 234
8.3.4 Termination Behaviour 235
8.3.5 Modelling the Physical World 237
8.4 Internally Prompted Behaviour 238
8.4.1 Cognitively-Cued Behaviour 238
8.4.2 Procedurally-Cued Behaviour 240
8.4.3 Mental Commit Actions 241
8.4.4 Case Studies 242
8.5 A More Complex Salience Model 243
8.5.1 Different Kinds of Salience 244
8.5.2 Load 244
8.5.3 Combining Salience 245
8.6 Alternate Uses of Generic User Models 246
8.6.1 Combining Error Analysis with Timing Analysis 246
8.6.2 Supporting Experiments by Exploring Behavioural Assumptions 248
8.6.3 Hazards, Requirements and Design Rules 250
8.6.4 Security Analysis 250
8.7 Other Forms of User Model 251
8.7.1 Interactive Cognitive Subsystems 251
8.7.2 Mental Models 252
8.8 Future Challenges 252
References 253
9 Physigrams: Modelling Physical Device Characteristics Interaction 256
Abstract 256
9.1 Introduction 257
9.2 Physical and Digital Feedback Loops 257
9.3 The Device Unplugged 259
9.4 Modelling the Device Unplugged 260
9.5 Physigrams—Modelling Physical States 261
9.6 Plugging in—Mappings to Digital State 264
9.7 Properties of Physical Interactions 266
9.8 Flexibility and Formality 269
9.9 Case Study—Tilley, a Community Wind Turbine 272
9.10 Conclusions 275
9.11 Key to Notation 276
Acknowledgements 279
References 279
10 Formal Description of Adaptable Interactive Systems Based on Reconfigurable User Interface Models 281
10.1 Introduction 281
10.2 Related Work 283
10.3 Formal Reconfiguration 285
10.3.1 Double Pushout Approach-Based Reconfiguration 285
10.3.2 Rewriting Inscriptions 289
10.4 Interactive Reconfiguration and Rule Generation 292
10.5 Case Study 294
10.5.1 Case Study: SCRAM Operation 295
10.5.2 User Study: Error Reduction Through Individualization 296
10.5.3 Discussion 298
10.6 Conclusion 301
References 301
Analysis, Validation and Verification 303
11 Learning Safe Interactions and Full-Control 304
11.1 Introduction 304
11.2 Background 306
11.3 Modelling the Learning Process with the Merge Operator 310
11.4 Basic Learning Units 313
11.5 How to Teach Full-Control 318
11.6 Related Work 321
11.7 Conclusion 322
References 323
12 Reasoning About Interactive Systems in Dynamic Situations of Use 325
12.1 Introduction 325
12.2 Background 328
12.3 Models and Reasoning 330
12.4 Earthquake Emergency Management Example 333
12.4.1 Use in Practice 340
12.5 Related Work 342
12.5.1 Disaster Management and Communications 342
12.5.2 Semantic Modelling for Interactive and Context-Aware Systems 343
12.6 Conclusions 344
12.6.1 Summary 344
12.6.2 Limitations and Future Work 345
References 346
13 Enhanced Operator Function Model (EOFM): A Task Analytic Modeling Formalism for Including Human Behavior in the Verification of Complex Systems 348
13.1 Introduction 349
13.2 Case Study 350
13.3 Enhanced Operator Function Model (EOFM) and EOFM with Communication (EOFMC) 351
13.3.1 Syntax 353
13.3.2 Visual Notation 358
13.3.3 Case Study Model 358
13.3.4 Formal Semantics 361
13.3.5 EOFM to SAL Translation 364
13.3.6 Erroneous Behavior Generation 368
13.3.7 Specification and Verification 372
13.3.8 Counterexample Visualization 373
13.4 Discussion 374
13.4.1 Applications 374
13.4.2 EOFM Extensions 377
13.5 Conclusions 379
References 379
14 The Specification and Analysis of Use Properties of a Nuclear Control System 383
14.1 Introduction 383
14.2 The Use Case 384
14.3 Structure of the Models 385
14.3.1 The Interface Specification 385
14.3.2 Structuring Specifications 386
14.4 Tool Support 388
14.4.1 Representing and Proving the Model 388
14.4.2 Property Templates 389
14.5 Modelling the Nuclear Power Plant Control User Interface 391
14.5.1 Types and Constants 392
14.5.2 The Process Layer 393
14.5.3 The Interface Layer 394
14.5.4 Proving Properties of the Interface Layer 397
14.5.5 The Activity Layer 400
14.6 Related Work 402
14.7 Discussion and Conclusions 404
References 405
15 Formal Analysis of Multiple Coordinated HMI Systems 408
15.1 Introduction 409
15.2 From HMI Frameworks to Full-Blown Multi-agent Systems 410
15.3 Formal Design and Analysis Techniques for HMI Properties 412
15.3.1 Extended LTS 412
15.3.2 Properties 413
15.3.3 Analysis 414
15.3.4 Example 416
15.3.5 Analysis of ADEPT Models 417
15.4 Coordinating HMIs as Multi-agent Systems 420
15.4.1 The Brahms Language 421
15.4.2 MAS Formal Analysis 421
15.4.3 Case Study: The Überlingen Collision 423
15.5 Related Work 430
15.6 Conclusions and Future Work 432
References 432
Future Opportunities and Developments 435
16 Domain-Specific Modelling for Human--Computer Interaction 436
16.1 Introduction 437
16.1.1 Case Study 438
16.1.2 Terminology 439
16.1.3 Outline 440
16.2 Syntax 440
16.2.1 Abstract Syntax 440
16.2.2 Concrete Syntax 441
16.3 Semantics 445
16.3.1 Semantic Domain 445
16.3.2 Semantic Mapping 446
16.4 Verification of Properties 453
16.4.1 Abstraction and Annotation Phase 455
16.4.2 ProMoBox Generation Phase 456
16.4.3 Specifying and Checking Properties Using ProMoBox 460
16.5 Conclusion 461
References 462
17 Exploiting Action Theory as a Framework for Analysis and Design of Formal Methods Approaches: Application to the CIRCUS Integrated Development Environment 465
Abstract 465
17.1 Introduction 466
17.2 A Global View on Modelling Activities During the Development of Interactive Systems 467
17.2.1 Engineer’s Tasks When Developing Interactive Systems 467
17.2.2 Norman’s Action Theory and Its Application to Models Production Tasks 469
17.3 Illustrative Example: The CIRCUS Integrated Development Environment 472
17.3.1 The Weather Radar Application Description 472
17.3.2 Formal Modelling of the WXR Application 474
17.3.2.1 Task Modelling 474
17.3.2.2 System Modelling 477
17.3.3 Tools Within the CIRCUS Integrated Development Environment 479
17.3.3.1 HAMSTERS Tool 479
17.3.3.2 PetShop Tool 481
17.3.3.3 SWAN Tool 482
17.4 Editing Tools for the Development of Interactive Systems 484
17.4.1 Norman’s Action Theory Applied to Editing Tools 484
17.4.2 Illustration with CIRCUS Environment 486
17.5 Verification Tools for the Development of Interactive Systems 488
17.5.1 Norman’s Action Theory Applied to Verification Tools 488
17.5.2 Illustration with CIRCUS Environment 490
17.6 Validation Tools for the Development of Interactive Systems 491
17.6.1 Norman’s Action Theory Applied to Validation Tools 491
17.6.2 Illustration with CIRCUS Environment 492
17.7 Beyond Multiple Unrelated Views: Connecting Models to Leverage V& V Tasks
17.7.1 Norman’s Action Theory Applied to V & V Tools
17.7.2 Illustration with the CIRCUS Environment 499
17.8 Discussion 501
17.9 Conclusion and Perspectives 502
References 503
18 A Public Tool Suite for Modelling Interactive Applications 505
Abstract 505
18.1 Introduction 505
18.2 Background 506
18.3 The Proposed Tool Suite 509
18.4 Task Modelling 511
18.4.1 CTT Task Models 511
18.4.2 ResponsiveCTT 513
18.5 Modelling and Generating Multimodal User Interfaces 516
18.6 Reverse Engineering User Interface Logical Descriptions 520
18.6.1 The Reverse Algorithm 522
18.7 Reverse Engineering Task Models 524
18.8 Conclusions and Future Work 526
References 527
19 Formal Modelling of App-Ensembles 529
Abstract 529
19.1 Introduction 530
19.2 Related Work 531
19.3 Background 532
19.4 The AOF-Language 533
19.4.1 Graphical Modelling Elements 534
19.4.1.1 Activities 535
19.4.1.2 Gateways 535
19.4.1.3 Events 537
19.4.1.4 Connecting Objects 537
19.4.1.5 Swimlanes 537
19.4.2 Textual Notation of the Model 537
19.5 Use Case Examples 539
19.5.1 Example 1: Wind Turbine Maintenance 539
19.5.2 Example 2: Nuclear Power Plant Maintenance 540
19.6 Formal Modelling 542
19.7 Petri Net Representation 543
19.8 Discussion 544
19.9 Conclusion and Outlook 546
Acknowledgements 546
References 546
20 Dealing with Faults During Operations: Beyond Classical Use of Formal Methods 548
Abstract 548
20.1 Introduction 549
20.2 Identifying Issues for the Dependability of Interactive Systems 550
20.2.1 Fault Taxonomy 550
20.2.2 Approaches for Addressing Faults 552
20.3 Addressing the Dependability of Interactive Systems 552
20.3.1 Addressing Development Software Faults (Issue 1) 553
20.3.2 Addressing Malicious Faults (Issue 2) 553
20.3.3 Addressing Development Hardware Faults (Issue 3) 554
20.3.4 Addressing Operational Natural Faults (Issue 4) 554
20.3.5 Addressing Operational Human Errors (Issue 5) 555
20.3.6 Concluding Remarks on the Identified Issues 555
20.4 Connection with Formal Methods 556
20.4.1 Development Software Faults 556
20.4.2 Malicious Faults 557
20.4.3 Development Hardware Faults 557
20.4.4 Operational Natural Faults 557
20.4.5 Operational Human Errors 557
20.5 Illustrative Example: Dealing with Both Development Software Faults and Operational Natural Faults in Interactive Cockpits 558
20.5.1 Main Hypotheses and Functional Failures Taken into Account 558
20.5.2 Dealing with Development Software Faults in Interactive Cockpits 560
20.5.2.1 A Fault Prevention Approach Using Formal Description Techniques 560
20.5.2.2 Illustration with the FCUS Case Study 561
20.5.3 Dealing with Operational Natural Faults in Interactive Cockpits 564
20.5.3.1 Related Work on Fault-Tolerant Systems 564
20.5.3.2 A Self-checking Architecture for Fault-Tolerant Interactive Components 566
20.5.3.3 Illustration with the FCUS Case Study 567
20.5.3.4 Connection with Formal Methods 568
20.5.4 Dealing with These Faults for the Entire Interactive System 569
20.6 Future Work 570
20.7 Conclusion 570
Acknowledgements 571
References 571
21 Erratum to: The Handbook of Formal Methods in Human-Computer Interaction 575
Erratum to:& #6