Slide 1: Formal Models for Informal GUI Designs Judy Bowen & Steve Reeves
Slide 2: Introduction • • • • • • • • • Introduction Background Approach Formalising the informal Presentation model Refinement PIMs Conclusions Future Work Judy Bowen & Steve Reeves FMIS, November 2006 2
Slide 3: Introduction • Formal Methods – Requirements gathering – Specification – Refinement – Testing • User-Centred Design – User requirements – Iterative design processes – Usability testing Judy Bowen & Steve Reeves FMIS, November 2006 3
Slide 4: Background UI + SYSTEM =? Judy Bowen & Steve Reeves FMIS, November 2006 4
Slide 5: Background USER USER UI UI SYSTEM SYSTEM Judy Bowen & Steve Reeves FMIS, November 2006 5
Slide 6: Approach Judy Bowen & Steve Reeves FMIS, November 2006 6
Slide 7: Approach Judy Bowen & Steve Reeves FMIS, November 2006 7
Slide 8: Approach Interactors User Interface System Judy Bowen & Steve Reeves FMIS, November 2006 8
Slide 9: Approach User Interface User-Centred Design Techniques System Formal Specifications and Refinements Judy Bowen & Steve Reeves FMIS, November 2006 9
Slide 10: Approach UI Functionality System Functionality User-Centred Design Techniques State Operations Formal Specifications and Refinements Judy Bowen & Steve Reeves FMIS, November 2006 10
Slide 11: Formalising the Informal • Design artefacts are deliberately informal – Sketches and paper-based prototypes – Whiteboard sessions – Scenarios • Capturing the narrative of design artefacts Judy Bowen & Steve Reeves FMIS, November 2006 11
Slide 12: Formalising the Informal • Pre-implementation user-centred design generates different artefacts at different levels of formality – – – – – – User requirements Task analysis Personas and scenarios Collaborative design sessions Paper prototypes Feedback iterations with users Judy Bowen & Steve Reeves FMIS, November 2006 12
Slide 13: Formalising the Informal • A paper-based prototype has a story – How does the user interact? – What are the results of interaction? – What do the pictured elements do? • We can build a model of that narrative – Identify the components i.e. the widgets – Describe the intended behaviour Judy Bowen & Steve Reeves FMIS, November 2006 13
Slide 14: Presentation Model • Each widget in the design is described as by a triple : – Identifier – Category – Behaviours • Different parts of the design described by different models Judy Bowen & Steve Reeves FMIS, November 2006 14
Slide 15: Presentation Model Judy Bowen & Steve Reeves FMIS, November 2006 15
Slide 16: Presentation Model Prototype is (FileMenu, Container, (ShowMenuItems)) (QuitMenuItem, ActionCtrl, (SysQuit)) (CircleSel, SValSelector, (DrawCircle)) (SquareSel, SValSelector, (DrawSquare)) (TriangleSel, SValSelector, (DrawTriangle)) (ShapeFrame, SValResponder, (DrawCircle,) DrawSquare, DrawTriangle)) Judy Bowen & Steve Reeves FMIS, November 2006 16
Slide 17: Presentation Model • We can use the presentation model in this form to examine issues such as design consistency • We can also ‘translate’ the model into Z using our previously defined framework as a basis Judy Bowen & Steve Reeves FMIS, November 2006 17
Slide 18: Presentation Model • Including UI in refinement process – Data refinement of presentation model • Design Equivalence – Simplifying refinement process – Multiple interface consistency • Consistency within designs – HCI principle Judy Bowen & Steve Reeves FMIS, November 2006 18
Slide 19: Refinement SysA UIA Sysc UIc 19 Judy Bowen & Steve Reeves FMIS, November 2006
Slide 20: Refinement (SysA || UIA) (Sysc || UIc ) Judy Bowen & Steve Reeves FMIS, November 2006 20
Slide 21: Refinement (SysA || UIA) (Sysc || UIc ) Judy Bowen & Steve Reeves FMIS, November 2006 21
Slide 22: Presentation Interaction Model • • • • Limitations of presentation model Dynamic behaviour of UI Reachability and deadlock Design refinement Judy Bowen & Steve Reeves FMIS, November 2006 22
Slide 23: Presentation Interaction Model • Presentation models and finite state machines • Avoid state explosion by using FSM with the presentation model which is already an abstraction of UI Judy Bowen & Steve Reeves FMIS, November 2006 23
Slide 24: Presentation Interaction Model • • • • • Set of states, Q Set of input labels ∑ Transition function δ Start state, q0 (one of the states of Q) Relation from presentation model to state, R (Q, ∑, δ, q0, R) Judy Bowen & Steve Reeves FMIS, November 2006 24
Slide 25: Presentation Interaction Model MPHeat MPMenu MPBath MPLounge Judy Bowen & Steve Reeves FMIS, November 2006 MPBed 25
Slide 26: Presentation Interaction Model MPHeat MPMenu MPBath MPLounge Judy Bowen & Steve Reeves FMIS, November 2006 MPBed 26
Slide 27: Presentation Interaction Model MPHeat is MPMenu : MPBath : MPLounge : MPBed MPMenu is …. MPBath is …. MPLounge is …. MPBed is …. Judy Bowen & Steve Reeves FMIS, November 2006 27
Slide 28: Presentation Interaction Model Judy Bowen & Steve Reeves FMIS, November 2006 28
Slide 29: Presentation Interaction Models • Proving reachability problems • Discovering deadlocks • Identifying non-determinism • Categorising desirable UI refinement properties (as conditions on PIMs) Judy Bowen & Steve Reeves FMIS, November 2006 29
Slide 30: Conclusions • We can integrate existing informal UCD methods with formal methods • Presentation models allow us to formalise informal design artefacts – Incorporate UI design into formal process – Investigate refinement • PIMs enable us to extend their uses – Dynamic UI properties Judy Bowen & Steve Reeves FMIS, November 2006 30
Slide 31: Future Work • • • • Formalise the || Defining refinement properties for UIs Proving monotonicity Exploring refinement of (Sys || UI) in the context of standard refinement techniques Judy Bowen & Steve Reeves FMIS, November 2006 31
Slide 32: Questions? Judy Bowen & Steve Reeves FMIS, November 2006 32