Geschäftskunden Kundenprogramme
Vor Ort
Merkzettel Warenkorb
Formal Methods in Human-Computer Interaction

Formal Methods in Human-Computer Interaction

Aus der Reihe

Fr. 72.90

inkl. gesetzl. MwSt.
Versandkostenfrei
Taschenbuch

Taschenbuch

Fr. 72.90 eBook

eBook

Fr. 62.90

Formal Methods in Human-Computer Interaction

Ebenfalls verfügbar als:

Taschenbuch

Taschenbuch

ab Fr. 72.90
eBook

eBook

ab Fr. 62.90

Beschreibung

Details

Einband

Taschenbuch

Erscheinungsdatum

29.10.1997

Herausgeber

Philippe Palanque + weitere

Verlag

Springer Berlin

Seitenzahl

376

Beschreibung

Details

Einband

Taschenbuch

Erscheinungsdatum

29.10.1997

Herausgeber

Verlag

Springer Berlin

Seitenzahl

376

Maße (L/B/H)

23.5/15.5/2.2 cm

Gewicht

598 g

Auflage

Softcover reprint of the original 1st ed. 1998

Sprache

Englisch

ISBN

978-3-540-76158-7

Weitere Bände von Formal Approaches to Computing and Information Technology (FACIT)

Unsere Kundinnen und Kunden meinen

0.0

0 Bewertungen

Informationen zu Bewertungen

Zur Abgabe einer Bewertung ist eine Anmeldung im Konto notwendig. Die Authentizität der Bewertungen wird von uns nicht überprüft. Wir behalten uns vor, Bewertungstexte, die unseren Richtlinien widersprechen, entsprechend zu kürzen oder zu löschen.

Verfassen Sie die erste Bewertung zu diesem Artikel

Helfen Sie anderen Kund*innen durch Ihre Meinung

Erste Bewertung verfassen

Unsere Kundinnen und Kunden meinen

0.0

0 Bewertungen filtern
  • Formal Methods in Human-Computer Interaction
  • 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.