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 Verification
1.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 Modelling
1.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 Development
3.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
4.3.2 User Interface of the Air Traffic Control Radar Screen
4.3.3 Connection with Formal Methods
4.4 Case Study 3—Interactive Aircraft Cockpits
4.4.1 The FCUS Application
4.4.2 Pilots Tasks
4.4.3 Connection with Formal Methods
4.5 Case Study 4—Interactive Systems in Rural Areas—Maintenance of Wind Turbines
4.5.1 Tilley—A Community Wind Turbine
4.5.2 Connection with Formal Methods
4.6 Case Study 5—Interactive Systems in Public Areas—Interactive Public Displays
4.6.1 Community Information Displays—The Internet-Enabled Shop-Open Sign
4.6.2 Connection with Formal Methods
References
Modeling, Execution and Simulation
5 Visual and Formal Modeling of Modularized and Executable User Interface Models
5.1 Introduction
5.2 Overview and Terminology
5.3 Background
5.4 Architecture
5.5 Modeling---Formalization
5.5.1 Formal Interaction Logic Language---FILL
5.5.2 Component-Based and Multidevice Models
5.5.3 Transformation to Reference Nets
5.6 Modeling and Editing
5.6.1 UIEditor---Creation
5.6.2 UIEditor---Execution
5.7 Case Study
5.8 Conclusion
References
6 Combining Models for Interactive System Modelling
6.1 Introduction
6.2 Related Work
6.3 Background
6.3.1 Presentation Model
6.3.2 Presentation Interaction Model
6.3.3 Presentation Model Relation
6.3.4 Specification
6.3.5 μCharts
6.3.6 Combining the Models
6.4 The Nuclear Power Plant Case Study
6.4.1 Benefits of Combining the Models
6.5 Conclusion
References
7 Activity Modelling for Low-Intention Interaction
Abstract
7.1 Introduction
7.2 What Is Low-Intention Interaction?
7.2.1 Intentional and Low-Intention Interaction
7.2.2 The Intentional Spectrum
7.2.3 Examples of Low-Intention Interaction
7.2.4 Intentional Shifts
7.2.5 Two Tasks
7.3 Frameworks and Paradigms
7.3.1 Design Concepts
7.3.2 Low Intention and Naturalness
7.3.3 Architecture and Modelling
7.4 Modelling Low-Intention Interactions
7.4.1 Modelling Process
7.4.2 Car Courtesy Lights
7.5 Into Practice: The Internet-Enabled Shop Open Sign
7.5.1 Concept—The Chip Van That Tweets
7.5.2 TireeOpen—The Internet-Enabled Open Sign
7.6 Further Design Considerations for Low Intention
7.6.1 User Models
7.6.2 Privacy
7.6.3 Can Task Models Help?
7.7 Discussion
Acknowledgements
References
8 Modelling the User
8.1 Introduction
8.1.1 Between Demonic and Angelic Behaviour
8.2 Verifying Systems with a User Model
8.2.1 Defining Systems Involving User Models
8.2.2 System Verification Involving User Models
8.2.3 Instantiating a Generic User Model
8.3 A Simple Model of Cognitively Plausible Behaviour
8.3.1 Non-determinism
8.3.2 Reactive Behaviour
8.3.3 Goal-Based Behaviour
8.3.4 Termination Behaviour
8.3.5 Modelling the Physical World
8.4 Internally Prompted Behaviour
8.4.1 Cognitively-Cued Behaviour
8.4.2 Procedurally-Cued Behaviour
8.4.3 Mental Commit Actions
8.4.4 Case Studies
8.5 A More Complex Salience Model
8.5.1 Different Kinds of Salience
8.5.2 Load
8.5.3 Combining Salience
8.6 Alternate Uses of Generic User Models
8.6.1 Combining Error Analysis with Timing Analysis
8.6.2 Supporting Experiments by Exploring Behavioural Assumptions
8.6.3 Hazards, Requirements and Design Rules
8.6.4 Security Analysis
8.7 Other Forms of User Model
8.7.1 Interactive Cognitive Subsystems
8.7.2 Mental Models
8.8 Future Challenges
References
9 Physigrams: Modelling Physical Device Characteristics Interaction
Abstract
9.1 Introduction
9.2 Physical and Digital Feedback Loops
9.3 The Device Unplugged
9.4 Modelling the Device Unplugged
9.5 Physigrams—Modelling Physical States
9.6 Plugging in—Mappings to Digital State
9.7 Properties of Physical Interactions
9.8 Flexibility and Formality
9.9 Case Study—Tilley, a Community Wind Turbine
9.10 Conclusions
9.11 Key to Notation
Acknowledgements
References
10 Formal Description of Adaptable Interactive Systems Based on Reconfigurable User Interface Models
10.1 Introduction
10.2 Related Work
10.3 Formal Reconfiguration
10.3.1 Double Pushout Approach-Based Reconfiguration
10.3.2 Rewriting Inscriptions
10.4 Interactive Reconfiguration and Rule Generation
10.5 Case Study
10.5.1 Case Study: SCRAM Operation
10.5.2 User Study: Error Reduction Through Individualization
10.5.3 Discussion
10.6 Conclusion
References
Analysis, Validation and Verification
11 Learning Safe Interactions and Full-Control
11.1 Introduction
11.2 Background
11.3 Modelling the Learning Process with the Merge Operator
11.4 Basic Learning Units
11.5 How to Teach Full-Control
11.6 Related Work
11.7 Conclusion
References
12 Reasoning About Interactive Systems in Dynamic Situations of Use
12.1 Introduction
12.2 Background
12.3 Models and Reasoning
12.4 Earthquake Emergency Management Example
12.4.1 Use in Practice
12.5 Related Work
12.5.1 Disaster Management and Communications
12.5.2 Semantic Modelling for Interactive and Context-Aware Systems
12.6 Conclusions
12.6.1 Summary
12.6.2 Limitations and Future Work
References
13 Enhanced Operator Function Model (EOFM): A Task Analytic Modeling Formalism for Including Human Behavior in the Verification of Complex Systems
13.1 Introduction
13.2 Case Study
13.3 Enhanced Operator Function Model (EOFM) and EOFM with Communication (EOFMC)
13.3.1 Syntax
13.3.2 Visual Notation
13.3.3 Case Study Model
13.3.4 Formal Semantics
13.3.5 EOFM to SAL Translation
13.3.6 Erroneous Behavior Generation
13.3.7 Specification and Verification
13.3.8 Counterexample Visualization
13.4 Discussion
13.4.1 Applications
13.4.2 EOFM Extensions
13.5 Conclusions
References
14 The Specification and Analysis of Use Properties of a Nuclear Control System
14.1 Introduction
14.2 The Use Case
14.3 Structure of the Models
14.3.1 The Interface Specification
14.3.2 Structuring Specifications
14.4 Tool Support
14.4.1 Representing and Proving the Model
14.4.2 Property Templates
14.5 Modelling the Nuclear Power Plant Control User Interface
14.5.1 Types and Constants
14.5.2 The Process Layer
14.5.3 The Interface Layer
14.5.4 Proving Properties of the Interface Layer
14.5.5 The Activity Layer
14.6 Related Work
14.7 Discussion and Conclusions
References
15 Formal Analysis of Multiple Coordinated HMI Systems
15.1 Introduction
15.2 From HMI Frameworks to Full-Blown Multi-agent Systems
15.3 Formal Design and Analysis Techniques for HMI Properties
15.3.1 Extended LTS
15.3.2 Properties
15.3.3 Analysis
15.3.4 Example
15.3.5 Analysis of ADEPT Models
15.4 Coordinating HMIs as Multi-agent Systems
15.4.1 The Brahms Language
15.4.2 MAS Formal Analysis
15.4.3 Case Study: The Überlingen Collision
15.5 Related Work
15.6 Conclusions and Future Work
References
Future Opportunities and Developments
16 Domain-Specific Modelling for Human--Computer Interaction
16.1 Introduction
16.1.1 Case Study
16.1.2 Terminology
16.1.3 Outline
16.2 Syntax
16.2.1 Abstract Syntax
16.2.2 Concrete Syntax
16.3 Semantics
16.3.1 Semantic Domain
16.3.2 Semantic Mapping
16.4 Verification of Properties
16.4.1 Abstraction and Annotation Phase
16.4.2 ProMoBox Generation Phase
16.4.3 Specifying and Checking Properties Using ProMoBox
16.5 Conclusion
References
17 Exploiting Action Theory as a Framework for Analysis and Design of Formal Methods Approaches: Application to the CIRCUS Integrated Development Environment
Abstract
17.1 Introduction
17.2 A Global View on Modelling Activities During the Development of Interactive Systems
17.2.1 Engineer’s Tasks When Developing Interactive Systems
17.2.2 Norman’s Action Theory and Its Application to Models Production Tasks
17.3 Illustrative Example: The CIRCUS Integrated Development Environment
17.3.1 The Weather Radar Application Description
17.3.2 Formal Modelling of the WXR Application
17.3.2.1 Task Modelling
17.3.2.2 System Modelling
17.3.3 Tools Within the CIRCUS Integrated Development Environment
17.3.3.1 HAMSTERS Tool
17.3.3.2 PetShop Tool
17.3.3.3 SWAN Tool
17.4 Editing Tools for the Development of Interactive Systems
17.4.1 Norman’s Action Theory Applied to Editing Tools
17.4.2 Illustration with CIRCUS Environment
17.5 Verification Tools for the Development of Interactive Systems
17.5.1 Norman’s Action Theory Applied to Verification Tools
17.5.2 Illustration with CIRCUS Environment
17.6 Validation Tools for the Development of Interactive Systems
17.6.1 Norman’s Action Theory Applied to Validation Tools
17.6.2 Illustration with CIRCUS Environment
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
17.8 Discussion
17.9 Conclusion and Perspectives
References
18 A Public Tool Suite for Modelling Interactive Applications
Abstract
18.1 Introduction
18.2 Background
18.3 The Proposed Tool Suite
18.4 Task Modelling
18.4.1 CTT Task Models
18.4.2 ResponsiveCTT
18.5 Modelling and Generating Multimodal User Interfaces
18.6 Reverse Engineering User Interface Logical Descriptions
18.6.1 The Reverse Algorithm
18.7 Reverse Engineering Task Models
18.8 Conclusions and Future Work
References
19 Formal Modelling of App-Ensembles
Abstract
19.1 Introduction
19.2 Related Work
19.3 Background
19.4 The AOF-Language
19.4.1 Graphical Modelling Elements
19.4.1.1 Activities
19.4.1.2 Gateways
19.4.1.3 Events
19.4.1.4 Connecting Objects
19.4.1.5 Swimlanes
19.4.2 Textual Notation of the Model
19.5 Use Case Examples
19.5.1 Example 1: Wind Turbine Maintenance
19.5.2 Example 2: Nuclear Power Plant Maintenance
19.6 Formal Modelling
19.7 Petri Net Representation
19.8 Discussion
19.9 Conclusion and Outlook
Acknowledgements
References
20 Dealing with Faults During Operations: Beyond Classical Use of Formal Methods
Abstract
20.1 Introduction
20.2 Identifying Issues for the Dependability of Interactive Systems
20.2.1 Fault Taxonomy
20.2.2 Approaches for Addressing Faults
20.3 Addressing the Dependability of Interactive Systems
20.3.1 Addressing Development Software Faults (Issue 1)
20.3.2 Addressing Malicious Faults (Issue 2)
20.3.3 Addressing Development Hardware Faults (Issue 3)
20.3.4 Addressing Operational Natural Faults (Issue 4)
20.3.5 Addressing Operational Human Errors (Issue 5)
20.3.6 Concluding Remarks on the Identified Issues
20.4 Connection with Formal Methods
20.4.1 Development Software Faults
20.4.2 Malicious Faults
20.4.3 Development Hardware Faults
20.4.4 Operational Natural Faults
20.4.5 Operational Human Errors
20.5 Illustrative Example: Dealing with Both Development Software Faults and Operational Natural Faults in Interactive Cockpits
20.5.1 Main Hypotheses and Functional Failures Taken into Account
20.5.2 Dealing with Development Software Faults in Interactive Cockpits
20.5.2.1 A Fault Prevention Approach Using Formal Description Techniques
20.5.2.2 Illustration with the FCUS Case Study
20.5.3 Dealing with Operational Natural Faults in Interactive Cockpits
20.5.3.1 Related Work on Fault-Tolerant Systems
20.5.3.2 A Self-checking Architecture for Fault-Tolerant Interactive Components
20.5.3.3 Illustration with the FCUS Case Study
20.5.3.4 Connection with Formal Methods
20.5.4 Dealing with These Faults for the Entire Interactive System
20.6 Future Work
20.7 Conclusion
Acknowledgements
References
21 Erratum to: The Handbook of Formal Methods in Human-Computer Interaction
Erratum to:B. Weyers et al. (eds.), The Handbook of Formal Methods in Human-Computer Interaction, Human-Computer Interaction Series, DOI 10.1007/978-3-319-51838-1