Formal methods have already been shown to improve the development process and quality assurance in system design and implementation. This volume examines whether these benefits also apply to the field of human-computer interface design and implementation, and whether formal methods can offer useful support in usability evaluation and obtaining more reliable implementations of user requirements. Its main aim is to compare the different approaches and examine which particular type of implementation and problem each one is best suited to. To enable the reader to compare and contrast the approaches as easily as possible, each one is applied to the same case study: the specification of an ideal Netscape-like web browser and html page server. The resulting volume will provide invaluable reading for final year undergraduate and postgraduate courses on user interfaces, user interface design, and applications of formal methods.

Inhalt

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 A…