A Formal Framework for the Analysis of Human-Machine Interactions
Première édition
There are more and more automated systems with which people are led to interact everyday. Their complexity increases, and badly designed systems may result in automation surprises. The contribution of this thesis is a formal analysis framework to assess whether a system is prone to potential automation surprises in an interaction. Lire la suite
There are more and more automated systems with which people are led to interact everyday. Their increasing complexity makes it harder for operators to drive them safely, in particular because badly designed systems may result in automation surprises. Several accidents are due to such surprising situations, as testified by real accidents. Examples include the Three Mile Island nuclear meltdown, the lethal radiation doses administered by the Therac 25 medical device, or the shot down of the aircraft of the KAL007 flight.
The contribution of this thesis is a formal analysis framework to assess whether a system is prone to potential automation surprises in an interaction. Potential automation surprises are captured by the full-control property. The minimal fullcontrol conceptual model generation problem consists in finding a minimal conceptual model that allows full-control of the system. The existence of such conceptual model is characterised by the fc-deterministic property. The generated models can be used to generate artifacts, such as user manuals. Three algorithms are proposed: the
first one uses three-valued deterministic finite automata that characterise the fullcontrol property in terms of traces; the second one uses a variant of the Paige-Tarjan reduction algorithm, and the third one uses the L* active learning algorithm. The proposed framework has been tested on various examples, among which a large case study of an autopilot coming from ADEPT, a toolset to support designers in the early design phases of automation interfaces. Experiences show that the method proposed in this thesis can identify existing automation surprises and also find new ones.
There are more and more automated systems with which people are led to interact everyday. Their increasing complexity makes it harder for operators to drive them safely, in particular because badly designed systems may result in automation surprises. Several accidents are due to such surprising situations, as testified by real accidents. Examples include the Three Mile Island nuclear meltdown, the lethal radiation doses administered by the Therac 25 medical device, or the shot down of the aircraft of the KAL007 flight.
The contribution of this thesis is a formal analysis framework to assess whether a system is prone to potential automation surprises in an interaction. Potential automation surprises are captured by the full-control property. The minimal fullcontrol conceptual model generation problem consists in finding a minimal conceptual model that allows full-control of the system. The existence of such conceptual model is characterised by the fc-deterministic property. The generated models can be used to generate artifacts, such as user manuals. Three algorithms are proposed: the first one uses three-valued deterministic finite automata that characterise the fullcontrol property in terms of traces; the second one uses a variant of the Paige-Tarjan reduction algorithm, and the third one uses the L* active learning algorithm. The proposed framework has been tested on various examples, among which a large case study of an autopilot coming from ADEPT, a toolset to support designers in the early design phases of automation interfaces. Experiences show that the method proposed in this thesis can identify existing automation surprises and also find new ones.
Pour plus d'informations à propos de la TVA et d'autres moyens de paiement, consultez la rubrique "Paiement & TVA".
Les commandes en ligne se font via notre partenaire i6doc.
Spécifications
- Éditeur
- Presses universitaires de Louvain
- Partie du titre
-
Numéro 459
- Auteur
- Sébastien Combéfis,
- Collection
- Thèses de l'École polytechnique de Louvain
- Langue
- anglais
- Catégorie (éditeur)
- Sciences appliquées
- BISAC Subject Heading
- TEC000000 TECHNOLOGY & ENGINEERING
- Code publique Onix
- 06 Professionnel et académique
- CLIL (Version 2013-2019 )
- 3069 TECHNIQUES ET SCIENCES APPLIQUEES
- Description public visé
- Ingénieurs, ergonomistes
- Date de première publication du titre
- 16 janvier 2014
- Subject Scheme Identifier Code
- Classification thématique Thema: Technologie, ingénierie et agriculture, procédés industriels
- Type d'ouvrage
- Thèse
- Avec
- Index, Bibliographie
Livre broché
- Date de publication
- 01 décembre 2013
- ISBN-13
- 978-2-87558-252-2
- Ampleur
- Nombre de pages de contenu principal : 302
- Dépôt Légal
- D/2013/9964/43 Louvain-la-Neuve, Belgique
- Code interne
- 89078
- Format
- 16 x 24 x 1,7 cm
- Poids
- 488 grammes
- Prix
- 23,20 €
- ONIX XML
- Version 2.1, Version 3
Google Livres Aperçu
Publier un commentaire sur cet ouvrage
Si vous avez une question, utilisez plutôt notre formulaire de contact
Sommaire
Abstracti
Acknowledgments iii
Foreword vii
1 Introduction 1
11 Research Goals 3
12 Overview of the Contributions5
13 Publications 7
14 Organisation of the Thesis 8
2 Context and State of the Art 11
21 Human-Computer Interaction 11
211 Human-Machine Systems 12
212 General Overview of Involved Elements 14
22 Analysing Human-Machine Interactions 19
23 Formal Methods20
231 Model Checking21
232 Theorem Proving22
233 Limits to Adoption 22
24 Analysing HMI with Formal Methods24
241 Analysing Mode Confusion with Model Checking25
242 User Interfaces Analyses Based on Metrics32
243 Using Model Checking to Verify Usability Properties 34
244 Cognitive considerations for the human behaviour 39
245 Integrating User's Tasks into the Interaction Analysis 43
246 Human Factors Considerations47
247 Automatic Generation of User Interfaces 50
ix
x CONTENTS
25 Context and Discussion53
251 Human-Machine System53
252 Interaction Analysis55
253 Safe Minimal Mental Model55
3 Modelling Human-Machine Interactions 57
31 Background and Basic Notation57
311 Transitions, Executions, Traces and Reachable States 59
312 Enabled and Possible Actions 60
313 Exploration 61
314 Internal Actions63
315 Determinism63
316 Synchronous Parallel Composition67
32 Human-Machine Interaction LTS 68
321 Interaction Model 71
33 Enriched Models74
331 Enriched System Model75
332 Enriched Mental Model79
333 Modelling the Interaction 81
34 Alternate Models for HMI 82
341 LTS with Inputs and Outputs 84
342 I/O and Interface Automata 85
343 Statecharts 87
344 Modal Specifications88
345 Mode Automata89
4 Full-Control Property 91
41 Characterisation of Good Interaction 91
411 Potential Automation Surprises93
42 Full-control Property for HMI-LTSs 95
421 Full-control Property95
422 Enabled or Possible Sets of Commands and Observations
98
423 Full-control Compatibility and Determinism 99
424 Existence of Full-control Mental Model 105
43 Full-control Property for Enriched Models106
431 Enriched Traces108
432 Full-control Compatibility for Enriched Models 109
CONTENTS xi
433 Expansion of Enriched Models110
44 Comparisons with Other Relations115
441 Trace Preorder 116
442 Testing Preorder118
443 Conformance120
5 Generating Full-control Conceptual Models 123
51 Minimal Full-control Conceptual Model Generation 123
511 Unicity 125
512 Generation Algorithms 127
52 Three-Valued Deterministic Finite Automata127
521 Consistent DFA 130
522 DFA-minimisation 131
523 Trace Characterisation of Full-control Property 134
53 3DFA-based Approach 136
54 Reduction-based Approach139
541 Eliminating _ -transitions 140
542 Partition Refinement141
543 The Reduction-based Algorithm 143
55 Learning-based approach148
551 The L_ learning algorithm 148
552 Learning a 3DFA152
553 Learning a Minimal Full-control Conceptual Model 155
56 Comparison of the Generation Algorithms161
561 Time Complexities and Execution Time 161
562 Non-fc-deterministic System Models 163
6 HMI Analysis 169
61 The jpf-hmi Tool 169
611 Structure of the Tool170
62 Analysis of Training Material 171
621 The Microwave Oven Example173
63 System Analysis177
631 Non-fc-deterministic System Model178
632 Minimal Full-control Conceptual Model 180
64 Mode Confusion Analysis 182
641 Generating Minimal Mode-preserving Conceptual
Model183
xii CONTENTS
642 Discovering Fc-modes 187
65 User Task Model187
651 Task-supporting property 189
652 Symmetric Full-control Property 191
653 Task Model Completion194
7 The Autopilot Case Study 197
71 The ADEPT Toolset and Model 197
711 General Presentation197
712 A Simple Model Example 200
72 A Formal Semantics of ADEPT202
721 ADEPT Logic Tables 203
722 ADEPT Programs 206
723 Execution Semantics209
73 ADEPT to HMI-LTS Translation 213
731 ASF structure 214
732 ASF ADEPT Model Translation 218
733 The Video Cassette Recorder example220
74 The Autopilot Model222
741 Autopilot Model Characteristics 222
742 Independent Subsystems225
743 Reducing the Model226
75 Analysis 228
751 Inhibited Command228
752 A First Conceptual Model 230
753 Analysing Mode Confusion234
8 Conclusion 239
81 Contributions of this Thesis239
82 Perspectives 241
83 Final Word 242
A Abbreviations and Acronyms 245
B List of System Examples 247
CONTENTS xiii
C Algorithms 249
C1 Full-control Property Check249
C2 Identification of Pairs of Compatible State250
C3 Identification of Compatibles 251
C4 3NFA-completion Completion 251
C5 3NFA Determinisation 252
Glossary 253
Bibliography 257
Index 278