06 3012405004818 Ciaco scrl onixsuitesupport@onixsuite.com 20260421 eng

COM.ONIXSUITE.9782875582522 03 02 i6doc 01 SKU 89078 02 2875582526 03 9782875582522 15 9782875582522 10 BC Numéro 459 Thèses de l'École polytechnique de Louvain 459 01 GCOI 28001100376640 1 A01 Sébastien Combéfis Combéfis, Sébastien Sébastien Combéfis <p>Sébastien Combéfis graduated from the Louvain School of Engineering (EPL) at theUniversité catholique de Louvain (UCL) with a Master of Computer Science Engineeringin June 2007. He is currently working as a part-time research assistant for ICTEAM atUCL.</p> 1 01 eng 302 00 302 03 TEC000000 29 2012 3069 TECHNIQUES ET SCIENCES APPLIQUEES 01 06 01 <p>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.<br />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<br />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.</p> 03 <p>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.<br />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<br />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.</p> 02 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... 01 <p> 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.</p><p> 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.</p> 03 <p> 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.</p><p> 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.</p> 02 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... 04 <p> Abstracti<br /> Acknowledgments iii<br /> Foreword vii<br /> 1 Introduction 1<br /> 11 Research Goals 3<br /> 12 Overview of the Contributions5<br /> 13 Publications 7<br /> 14 Organisation of the Thesis 8<br /> 2 Context and State of the Art 11<br /> 21 Human-Computer Interaction 11<br /> 211 Human-Machine Systems 12<br /> 212 General Overview of Involved Elements 14<br /> 22 Analysing Human-Machine Interactions 19<br /> 23 Formal Methods20<br /> 231 Model Checking21<br /> 232 Theorem Proving22<br /> 233 Limits to Adoption 22<br /> 24 Analysing HMI with Formal Methods24<br /> 241 Analysing Mode Confusion with Model Checking25<br /> 242 User Interfaces Analyses Based on Metrics32<br /> 243 Using Model Checking to Verify Usability Properties 34<br /> 244 Cognitive considerations for the human behaviour 39<br /> 245 Integrating User's Tasks into the Interaction Analysis 43<br /> 246 Human Factors Considerations47<br /> 247 Automatic Generation of User Interfaces 50<br /> ix<br /> x CONTENTS<br /> 25 Context and Discussion53<br /> 251 Human-Machine System53<br /> 252 Interaction Analysis55<br /> 253 Safe Minimal Mental Model55<br /> 3 Modelling Human-Machine Interactions 57<br /> 31 Background and Basic Notation57<br /> 311 Transitions, Executions, Traces and Reachable States 59<br /> 312 Enabled and Possible Actions 60<br /> 313 Exploration 61<br /> 314 Internal Actions63<br /> 315 Determinism63<br /> 316 Synchronous Parallel Composition67<br /> 32 Human-Machine Interaction LTS 68<br /> 321 Interaction Model 71<br /> 33 Enriched Models74<br /> 331 Enriched System Model75<br /> 332 Enriched Mental Model79<br /> 333 Modelling the Interaction 81<br /> 34 Alternate Models for HMI 82<br /> 341 LTS with Inputs and Outputs 84<br /> 342 I/O and Interface Automata 85<br /> 343 Statecharts 87<br /> 344 Modal Specifications88<br /> 345 Mode Automata89<br /> 4 Full-Control Property 91<br /> 41 Characterisation of Good Interaction 91<br /> 411 Potential Automation Surprises93<br /> 42 Full-control Property for HMI-LTSs 95<br /> 421 Full-control Property95<br /> 422 Enabled or Possible Sets of Commands and Observations<br /> 98<br /> 423 Full-control Compatibility and Determinism 99<br /> 424 Existence of Full-control Mental Model 105<br /> 43 Full-control Property for Enriched Models106<br /> 431 Enriched Traces108<br /> 432 Full-control Compatibility for Enriched Models 109<br /> CONTENTS xi<br /> 433 Expansion of Enriched Models110<br /> 44 Comparisons with Other Relations115<br /> 441 Trace Preorder 116<br /> 442 Testing Preorder118<br /> 443 Conformance120<br /> 5 Generating Full-control Conceptual Models 123<br /> 51 Minimal Full-control Conceptual Model Generation 123<br /> 511 Unicity 125<br /> 512 Generation Algorithms 127<br /> 52 Three-Valued Deterministic Finite Automata127<br /> 521 Consistent DFA 130<br /> 522 DFA-minimisation 131<br /> 523 Trace Characterisation of Full-control Property 134<br /> 53 3DFA-based Approach 136<br /> 54 Reduction-based Approach139<br /> 541 Eliminating _ -transitions 140<br /> 542 Partition Refinement141<br /> 543 The Reduction-based Algorithm 143<br /> 55 Learning-based approach148<br /> 551 The L_ learning algorithm 148<br /> 552 Learning a 3DFA152<br /> 553 Learning a Minimal Full-control Conceptual Model 155<br /> 56 Comparison of the Generation Algorithms161<br /> 561 Time Complexities and Execution Time 161<br /> 562 Non-fc-deterministic System Models 163<br /> 6 HMI Analysis 169<br /> 61 The jpf-hmi Tool 169<br /> 611 Structure of the Tool170<br /> 62 Analysis of Training Material 171<br /> 621 The Microwave Oven Example173<br /> 63 System Analysis177<br /> 631 Non-fc-deterministic System Model178<br /> 632 Minimal Full-control Conceptual Model 180<br /> 64 Mode Confusion Analysis 182<br /> 641 Generating Minimal Mode-preserving Conceptual<br /> Model183<br /> xii CONTENTS<br /> 642 Discovering Fc-modes 187<br /> 65 User Task Model187<br /> 651 Task-supporting property 189<br /> 652 Symmetric Full-control Property 191<br /> 653 Task Model Completion194<br /> 7 The Autopilot Case Study 197<br /> 71 The ADEPT Toolset and Model 197<br /> 711 General Presentation197<br /> 712 A Simple Model Example 200<br /> 72 A Formal Semantics of ADEPT202<br /> 721 ADEPT Logic Tables 203<br /> 722 ADEPT Programs 206<br /> 723 Execution Semantics209<br /> 73 ADEPT to HMI-LTS Translation 213<br /> 731 ASF structure 214<br /> 732 ASF ADEPT Model Translation 218<br /> 733 The Video Cassette Recorder example220<br /> 74 The Autopilot Model222<br /> 741 Autopilot Model Characteristics 222<br /> 742 Independent Subsystems225<br /> 743 Reducing the Model226<br /> 75 Analysis 228<br /> 751 Inhibited Command228<br /> 752 A First Conceptual Model 230<br /> 753 Analysing Mode Confusion234<br /> 8 Conclusion 239<br /> 81 Contributions of this Thesis239<br /> 82 Perspectives 241<br /> 83 Final Word 242<br /> A Abbreviations and Acronyms 245<br /> B List of System Examples 247<br /> CONTENTS xiii<br /> C Algorithms 249<br /> C1 Full-control Property Check249<br /> C2 Identification of Pairs of Compatible State250<br /> C3 Identification of Compatibles 251<br /> C4 3NFA-completion Completion 251<br /> C5 3NFA Determinisation 252<br /> Glossary 253<br /> Bibliography 257<br /> Index 278</p> 04 01 http://www.i6doc.com/resources/titles/28001100376640/images/19e901474bd32d47931f0219992ff889/HIGHQ/9782875582522.jpg 17 03 01 https://i6doc.com/resources/publishers/35.jpg 18 09 01 https://i6doc.com/resources/publishers/73.png 38 https://i6doc.com/en/book/?GCOI=28001100376640 06 3052405007518 Presses universitaires de Louvain 01 06 3052405007518 Presses universitaires de Louvain 01 Presses universitaires de Louvain http://pul.uclouvain.be/ Louvain-la-Neuve BE 04 20131201 2013 02 WORLD 01 9.45 in 02 6.30 in 03 1.61 in 08 17.07 oz 01 24 cm 02 16 cm 03 1.61 cm 08 484 gr 06 3012405004818 CIACO - DUC 33 www.i6doc.com http://www.i6doc.com 03 WORLD 01 2 20 1 02 00 02 02 STD 02 23.20 EUR R 6.00 21.89 1.31