Formal Methods in Human-Computer Interaction

ISBN-13: 9783540761587 / Angielski / Miękka / 1997 / 396 str.

Philippe Palanque; Fabio Paterno; Fabio Paterno

Opis

Formal methods improve the development process and quality assurance in system design and implementation. This text examines whether these benefits also apply to the field of human-computer interface design and implementation, and whether formal methods offer useful support in usability evaluation.

Spis treści

I Modelling Techniques.- 1 Specifying History and Backtracking Mechanisms.- 1.1 Introduction.- 1.2 Reflexive Specification.- 1.2.1 Browser Commands and State.- 1.2.2 Components of the Browser State and Command Classes.- 1.2.3 History Commands and State.- 1.2.4 Model and Implementation.- 1.2.5 Conservativeness of State.- 1.3 Six History Mechanisms.- 1.3.1 Windows Help — a Stack and a Trace.- 1.3.2 Think Reference — a Recency Ordered Set.- 1.3.3 Netscape — a Stack with Pointer.- 1.3.4 HyperCard-a First Use Ordered Set and a Navigable Trace.- 1.4 Comparing the Methods.- 1.4.1 Back or Not Back?.- 1.4.2 Visible History.- 1.4.3 One Mechanism or Two.- 1.4.4 Completeness of Histories.- 1.4.5 Searching.- 1.5 History and Undo.- 1.5.1 State and Conservativeness.- 1.5.2 Names, States, Icons and Actions.- 1.6 Summary.- 2 How to Model a Web (Without Getting Tangled in Nets).- 2.1 Introduction.- 2.2 The Plant and Environment.- 2.2.1 A Simple Model of Hypertext.- 2.2.2 The Effect of Distribution.- 2.2.3 Integrating Pages and Servers with HTML.- 2.3 The Interface: Display and Controls.- 2.3.1 Display.- 2.3.2 Control.- 2.4 The System.- 2.5 To Err is Human.- 2.6 Finishing Touches.- 2.7 Discussion and Conclusions.- 3 Software Architecture Modelling: Bridging Two Worlds Using Ergonomics and Software Properties.- 3.1 Introduction.- 3.2 Software Architecture and Life-Cycle: Point of Contact of Two Worlds.- 3.3 Model and Method with PAC-Amodeus.- 3.3.1 PAC-Amodeus, a Software Architecture Model for Interactive Systems.- 3.3.2 User-Centered Design and Software Design: a Point of Contact Using Properties.- 3.3.3 From Model to Reality: How to Apply PAC-Amodeus.- 3.4 A Case Study: a WWW Browser.- 3.4.1 Software Design.- 3.4.2 Scenario: Messages Passing.- 3.4.3 Properties.- 3.5 Conclusion.- 4 A Formal Approach to Consistency and Reuse of Links in World Wide Web Applications.- 4.1 Introduction.- 4.2 Perusing the Anchoring Layer.- 4.3 The Link Oriented Approach for Checking Consistency and Reuse.- 4.4 Recovering Links: a Formal Approach.- 4.5 Analysing Link Reuse Cases: The LiOS Tool.- 4.6 Experimenting with LiOS — Empirical Results.- 4.7 Conclusions.- 5 Using Declarative Descriptions to Model User Interfaces with Mastermind.- 5.1 Model-Based User Interfaces.- 5.1.1 Motivation.- 5.1.2 State of the Art.- 5.2 The Mastermind Conceptual Architecture.- 5.2.1 Mastermind Models.- 5.2.2 The Ontology of Mastermind Models.- 5.3 The UI Generation Process.- 5.4 The Mastermind Dialogue Notation.- 5.4.1 Dialogue Tokens: Interaction-Application Invocation.- 5.4.2 Dialogue Variables: Composite Ordering.- 5.4.3 Data Parameters.- 5.4.4 Dialogue Validation.- 5.5 Binding in Mastermind Models.- 5.5.1 The Mastermind Interaction Model.- 5.5.2 Selection Interaction Techniques.- 5.5.3 Form Entry Interaction Technique.- 5.6 The Mastermind Design Method.- 5.7 Case Study.- 5.7.1 Context: Web Browsers.- 5.7.2 Dialogue Model Example.- 5.7.3 Presentation Model Example.- 5.7.4 Interaction Techniques for a Web Browser.- 5.7.5 Dialogue Model Evolution: Web Browser History Mechanism.- 5.7.6 Presentation Model Evolution: Web Browser History Mechanism.- 5.7.7 Interaction Model Evolution: Web Browser History Mechanism.- 5.8 Status.- 5.8.1 Code Generators.- 5.8.2 Dukas.- 5.8.3 Contributions and Future Directions.- II Approaches to the Formal Specification.- 6 XTL: A Temporal Logic for the Formal Development of Interactive Systems.- 6.1 Introduction.- 6.1.1 Temporal Logic and HCl.- 6.1.2 The XTL Formalism.- 6.1.3 The Other Way of Reading this Chapter.- 6.2 The Very Bases of XTL.- 6.3 The XTL Formalism.- 6.3.1 Vocabulary and Symbols.- 6.3.2 Syntax of Expressions.- 6.3.3 Syntax of Formulas.- 6.3.4 Syntax of Assertions.- 6.3.5 Model of the Logic.- 6.3.6 Interpretation.- 6.4 Other Operators: Flow of Control Constructs.- 6.4.1 Definition 5: power.- 6.4.2 The Operator ‘empty’.- 6.4.3 p Holds One or Several Times.- 6.4.4 p Holds Zero or Several Times.- 6.4.5 p Holds Zero or One Time.- 6.4.6 p Holds Exactly n Times.- 6.4.7 Independent Order of Two Tasks p and q.- 6.4.8 The If-Then-Else Construct.- 6.4.9 The While Construct.- 6.5 Operators Related to Interruptions and Concurrency.- 6.5.1 History.- 7.3.4 Specification of Browser Commands.- 7.4 Analysing Interaction Object Graphs.- 7.4.1 State Invariance.- 7.4.2 Dialogue Completion.- 7.5 Conclusion.- 8 Specifying a Web Browser Interface Using Object-Z.- 8.1 Introduction.- 8.2 The Language Model.- 8.3 Interactor Specification.- 8.4 Choosing a Notation.- 8.5 Case Study.- 8.6 Conclusions.- 9 Modelling Clients and Servers on the Web Using Interactive Cooperative Objects.- 9.1 Introduction.- 9.2 The ICO Formalism.- 9.2.1 Relationship Between Interface and Behaviour.- 9.2.2 Invocation Modes and Their Semantics.- 9.2.3 Presentation.- 9.2.4 Abbreviation.- 9.2.5 Architecture.- 9.3 The Case Study.- 9.3.1 The Web Server.- 9.3.2 The Web Client.- 9.3.3 Refinement of the Specification.- 9.4 Discussion.- 9.4.1 Modelling Benefits.- 9.4.2 Formal Analysis.- 9.4.3 User Centered Modelling.- 9.4.4 Performance Evaluation.- 9.4.5 Automated Implementation.- 9.5 Conclusion.- 10 Development of a WWW Browser Using TADEUS.- 10.1 Introduction.- 10.2 TADEUS Approach — Brief Overview.- 10.3 Dialogue Graphs — Brief Introduction.- 10.3.1 Structural (or Static) Modelling.- 10.3.2 Behavioural (or Dynamic) Modelling.- 10.3.3 Special Views.- 10.3.4 Types of Dialogue Graphs.- 10.4 Specification of a WWW Browser.- 10.4.1 Requirements Analysis and Specification.- 10.4.2 Dialogue Design.- 10.4.3 Generation of the User Interface Prototype.- 10.4.4 Extending the Simple Web Browser with a History Mechanism and Bookmark Management.- 10.5 Related Work.- 10.6 Conclusion.- 10.6.1 Summary on Case Study Work.- 10.6.2 Future Developments.- 11 Algebraic Specification of a World Wide Web Application Using GRALPLA.- 11.1 Introduction.- 11.2 The Specification Language.- 11.3 Description of the Specification.- 11.4 Verification and Extensions.- 11.5 From Specification to Implementation.- 11.6 Conclusion and Evaluation of the Method.- III Approaches to the Formal Evaluation.- 12 TLIM, a Systematic Method for the Design of Interactive Systems.- 12.1. Introduction.- 12.2. The TLIM Method.- 12.3. ConcurTaskTrees.- 12.4. ConcurTaskTrees Specification of Tasks in a Web Session.- 12.5. The Transformation from the Task Model to the Software Architecture Model.- 12.5.1 The Transformation from the Task Model to the Software Architecture Model.- 12.5.2 The Identification of the Components.- 12.6. Formal Specification of Properties of the Web.- 12.6.1 A Formal Framework for Expressing Interaction Properties.- 12.6.2 Demonstration of Properties over the Specification of the Web.- 12.7. Conclusions.- 13 Electronic Gridlock, Information Saturation and the Unpredictability of Information Retrieval over the World Wide Web.- 13.1 Introduction.- 13.1.1 The Problems: Electronic Gridlock.- 13.1.2 The Problems: Information Saturation.- 13.1.3 The Problems: Unpredictability.- 13.2 Analysing Electronic Gridlock.- 13.3 Analysing Unpredictability.- 13.4 Analysing Information Saturation.- 13.4.1 Information Saturation and the Creativity of Design.- 13.4.2 Information Saturation and the Evaluation of Design.- 13.5 Conclusion.- 14 From Formal Models to Empirical Evaluation and Back Again.- 14.1 Introduction.- 14.2 An Informal Understanding Of Usability Issues.- 14.3 A Formal Model.- 14.3.1 An Abstract Model.- 14.3.2 A More Concrete Model.- 14.4 Selecting Tasks and Use Cases.- 14.5 Usability Inspection.- 14.5.1 The Cognitive Walkthrough Process.- 14.5.2 The Analysis.- 14.5.3 Usability Inspection Summary.- 14.6 User Testing.- 14.6.1 The Cooperative Evaluation Process.- 14.6.2 The Analysis.- 14.6.3 User Testing Summary.- 14.7 Integrating with Formal Modelling.- 14.8 Conclusions.- 15 A Component-Based Approach Applied to a Netscape-Like Browser.- 15.1 Introduction.- 15.2 Fashioning a Component-Oriented Toolkit.- 15.2.1 An Interconnection Language: IL.- 15.2.2 Generating Implementations.- 15.2.3 Fashioning Interfaces for Primitives.- 15.3 Modelling User Interface Behaviour.- 15.3.1 A Simple Language.- 15.3.2 Modelling Runs.- 15.3.3 Commands.- 15.3.4 Generating Models from IL Descriptions.- 15.4 Validation.- 15.4.1 State Invariants.- 15.4.2 Reactive Properties.- 15.5 Conclusions.- References.- The Web Browser Case Study.- Index of Key Words.- Index of Authors.