Model-based approaches for
the design of safety critical
interactive systems
Philippe Palanque
LIIHS-IRIT
University Paul Sabatier
Toulouse – France
http://liihs.irit.fr/palanque
[email protected]
Rio de Janeiro – 18-19 september 2007
1
Overview of the lectures







Overview of LIIHS Research Group
State of the art in MBA for HCI
System modeling
Task modeling
Design rationale
Research Themes and Productions
A Roadmap on FM & HCI
2
1 - Overview of LIIHS
A bit of History about LIIHS


Started in 1988 at University Toulouse 1 (law
and economics) gathering all the computer
scientists at UT1
In 1993 main research theme is HCI and name
changed to LIHS (group size about 15 people)



From research on software engineering
methodologies
From research on notations for modeling activities
~ 20 PhDs
3
1 - Overview of LIIHS
Research at LIIHS

Mono-disciplinary research: Human Computer Interaction




Special point of view: Software Engineering for HumanComputer Interaction




Computer Scientists,
Human Factors, Ergonomics,
HCI specialists
Usability (methods for design and evaluation of computer systems)
Reliability (formal specification, human error assessment, …)
Traceability (Design rationale)
Special application domain: (safety) critical interactive systems
– cost of development much lower than the cost of a failure
4
1 - Overview of LIIHS
Safety Critical Interactive Systems

Safety Critical Systems








Software Engineers
System centered
Reliability
Safety requirements
(certification)
Formal specification
Verification / Proof
Waterfall model / structured
Archaic interaction
techniques

Interactive Systems








Usability experts
User centered
Usability
Human factors
Task analysis & modeling
Evaluation
Iterative process / Prototyping
Novel Interaction techniques
5
Modeling

Tasks models


Scenarios



Concrete description of users' planned activities
Temporal organization of actions (and related information)
System models




Abstract description of users' planned activities (goal)
Both structure (object oriented approach) and behavioral
description
How user's actions change system state
How system state (rendering)
 Reduces authorized user's actions
 Is presented to the user
Designing options rationally
6
1 - Overview of LIIHS
Research Projects

Current projects



Recently completed





ReSIST EU Network of Excellence Project (Resilience for Information Society) (012006/12-2008)
COST NSF EU action MAUSE (Maturing Usability) (01-2005/12-2008)
INTUITION Project (Multimodal Interfaces military aircrafts) (02-2003/02-2006)
MISC Project (Multimodal Interfaces for Safety-critical Command and Control) (012003/01-2007)
Research Training Network EU ADVISES (11-2002/ 12-2006)
Capes/ Cofecub SPIDER WEB (07-2002/07-2005)
Previous relevant projects






DoD Drones Project (Unmanned Aerial Vehicles) (03-2001/09-2002)
EUD-Net EU Network of Excellence (07-2002/07-2002)
EVALWEB Project: Building ergonomic web sites by design (1999-2002)
Project CNET SERPICO : Specifications for CORBA Components Engineering
(1998-2001)
Esprit Project LTR MEFISTO n°24963 Modeling Evaluation and Formalizing
Interactive Systems using Tasks and Objects (1997-2001)
ERGOVAL (1995)
7
1 - Overview of LIIHS
EvalWeb




1998-2002
Ergonomic application web by design
Partners : Univ. Louvain la neuve (J.
Vanderdonckt) & INRIA (D. Scapin)
Funding : CNRS GIS Cogniscience (1999)
8
MEFISTO (overview)




Modeling, Evaluating and Formalizing Interactive
Systems using Tasks and interaction Objects
ESPRIT Reactive LTR 24963 Project (EC)
Air Traffic Control domain
Multi disciplinary team




Computer Scientists (F. Paterno CNUCE, LIIHS)
Psychologists (P. Wright Univ. York, P. Marti Univ.
Sienna)
Industrial partners (DERA UK, CENA F, Alenia I)
Users (ENAV I ATC association)
9
1 - Overview of LIIHS
UAV Project (1/2)
10
1 - Overview of LIIHS
UAV Project (2/2)




Design, implementation and evaluation of
user interfaces for drones command and
control
Performance and user capabilities
Authority sharing
From several controllers per drone to one
controller for several drones
11
1 - Overview of LIIHS
MISC Project



Multimodal Interaction for Command and
Control of Safety critical Systems
Starting: beginning 01/2003
Finances: DGA (French Department of
Defense , CNES (National center for spatial
studies), and LIIHS
12
1 - Overview of LIIHS
Project SPIDER WEB





Specification and Prototyping for user Interface
Design, Engineering and Re-engineering for the
Web
France- Brazil cooperation
Partners LIIHS and Instituto de Informatica (Porto
Alegre)
Beginning Feb. 2002
In conjunction with a CNPq funding of Marco
Winckler PhD about "model-based approaches
for wed application evaluation"
COFECUB
13
ADVISES: Analysis Design and Validation
of Interactive Safety-critical and Error-tolerant
Systems




Type de projet: Research Training Network
Sponsors: EU (Fifth Framework Improving Human Potential Programme)
8 sites : Delft University of Technology (NL), ISTI-CNR(I), Risø National
Laboratory (DK), Université de Liège (B), Université Paul Sabatier
Toulouse (F), University of Glasgow (UK), University of York (UK),
Universität Paderborn (D)
Objectifs


Étudier et développer des méthodes outils et techniques pour l'analyse, la conception
et la validation de systèmes interactifs fiables et tolérants aux erreurs humaines
Principes

Durée (4 ans):
Oct. 02  Oct. 06
Budget LIIHS:

160 K€ HT

Approche pluridisciplinaire intégrant des spécialistes facteurs humains (ergonomie
cognitive, psychologie du travail) des spécialistes informatiques (génie logiciel,
méthodes formelles, approches à objets et distribuées) des spécialistes en interaction
homme-machine (méthodes de conception centrée utilisateur) et des spécialistes en
systèmes critiques (analyse d'incidents/accidents, systèmes embarqués civil et
militaires, nucléaire)
Formation à la recherche et par la recherche
Formation des jeunes chercheurs dans ces domaine par la mobilité au sein du réseau
14
1 - Overview of LIIHS
EUD-Net



The EUD-NET Network of Excellence is
financed by European Community and
started in July, 1st 2002.
Goal: help the European Commission to
prepare a research agenda in the end-user
development field
Related to previous work on notations and
tools for visual programming
15
Project INTUITION




Financed by DoD. THALES avionic in charge. LIIHS
team 240K€ HT.
Start January 2003. 3 years
Definition and construction of a platform for the design,
specification and development of multimodal interactive
systems
Application domains:


Rafale Cockpit
Air Traffic Control multimodal Interfaces
16
Cockpit Rafale
Visu tête haute
Ecran tactile
Joystick
17
MAUSE: Towards the MAturation of
http://www.cost294.org/


Information Technology USability
Evaluation
Type de projet: action COST
Sponsors: ESF (European Science Foundation) et COST (European
Cooperation in the field of Scientific and Technical research)
http://www.esf.org/

19 pays UE: (AT, BE, CY, CZ, DK, FI, FR, DE, GR, IS, NL, NO, PL, RO, SI, ES, SE,
CH and UK)

http://cost.cordis.lu/
Durée (4 ans):
Déc. 04  Nov. 08
Objectifs


Étudier, développer, évaluer et comparer les Méthodes d’Evaluation de
l’Utilisabilité (MEU)s
Activités



Budget:

Défini en fonctions
des missions et des
activités des
participants


WG 1: Révision et Analyse de (MEU)s
WG 2: Comparaison de (MEU)s: Stratégies et Implémentation
WG 3: Validation de Schèmes de Classification de Problèmes d’utilisabilité
WG 4: Révision des approches assistées par l’ordinateurs pour
l’évaluation de l’utilisabilité
(SIG): E-Learning
Dissémination de résultats (Coordination): LIIHS-IRIT, P. Palanque, M. Winckler
18
1 - Overview of LIIHS
ReSIST


http://www.resist-noe.eu/
Resilience






Diversity
Usability
Evolvability
Assessability
Dependability+Safety+Security+Usability
Duration 3 years
19
1 - Overview of LIIHS
Members of LIIHS working in
that field
David
NAVARRE
Lecturer
Marco
WINCKLER
Lecturer
Christelle
FARENC
Lecturer
Joseph Xiong
PhD Student
4th year
Regina
BERNHAUPT
Visiting
Professor
Philippe
PALANQUE
Professor
Florence
Pontico
PhD Student
4th year
Sandra
BASNYAT
Post Doc
Jean-François
LADRY
PhD Student
1st year
Eric BARBONI
Post Doc
20
Outline of the presentation


Overview of LIIHS Research Group
State of the art in MBA for HCI









Specificities of Interactive System
What is modeling?
What kind of modelling in HCI?
What has still to be done?
System modelling
Task modelling
Design rationale
Research Themes and Productions
A Roadmap on FM & HCI
21
2 – State of the art
Interactive Systems
Output
System
User
Input
input
output
Interactive
System
Time
22
2 – State of the art
"Classical" Design Process SS
Informal
requirements
Manual
Specification
Spec 1
...
Spec n
Design
Design 1
...
Design n
Coding
Prog. 1
...
Prog. n
User testing
23
2 – State of the art
What is a "Model" ?


Concepts relationships between concepts
Example : Entity Relationship Model



Concepts : Entity types, Relationship Types,
Attributes, Domain of Values, Identifiers, ...
Relationships between concepts : "A Relationship
type is a sub set of the Cartesian product of two
Entity Type"
An entity e1 cannot have more than one
relationship with another entity e2 through the
same relationship type
e1 x
e2 x
e3 x
x f1
x f2
x f3
24
2 – State of the art
What can we Expect from a
Model ?



Completeness (we can express all the
information we need to)
Consistency (Contradictory elements cannot
be expressed)
Generality (Independent from a given
application domain … always ?)
25
2 – State of the art
What is a "formalism" ?

A set of conventions for representing the
concepts of a Model



Lexical elements (graphical or textual)
Concrete Syntax (separators, terminators, ...)
A formal definition of these conventions
(otherwise just a notation)
Flat
1,1
0,n
Person
Owns
26
2 – State of the art
What can we expect from a
"formalism" ? Flat 1,1 Owns 0,n






Person
Expressiveness
0,1
0,n
Rents
Conciseness
Closeness of the representation to the application
domain
Completeness wrt the Model (counter example :
Graphical formalism of the Entity Relationship Model)
L. Lamport "the only difficult problem the author
solved was understanding his own notation"
L. Lamport "Automaton is a formal description
technique dedicated to the specification of stacks"
27
2 – State of the art
Bug : With a "Formalism" we
build "models"
Modelling



model: ideal representation of a given
situation form the real world restrained to the
concepts covered by the Model
Goal: analyze the model to draw conclusions
about the actual state of the real world
Meta-model: model representing the
concepts of the Model using the formalism
(done for E/R and UML using class diagrams)
28
2 – State of the art
What and why modeling
systems?

An abstract description of the system




independent from the implementation
that do not deal too early with details
Describe what are the outputs of the system
according to the inputs
To allow discussions between the various
actors (at a time, along the design process)

to store results of discussions
29
2 – State of the art
What is a system model
for Interactive Systems ?


Represents the system data and actions
Represents behaviour of the system




what actions are offered by the system
when an action is available (according to the state
of the system)
what is the effect of an action on the state of the
system
Represents both how the system is
presented to the user and how the user
interacts with it
30
2 – State of the art
Design process for IS ?
Manual
Informal
requirements
Spec 1
...
Spec n
Goal 1
...
Goal n
User
requirements
Design
Design 1
...
Design n
Task 1
...
Task n
Task Analysis
Coding
Prog. 1
...
Prog. n
Specification
User testing
31
2 – State of the art
Why Modelling Interactive
Systems Formally ?





To cope with the complexity
To avoid a human observer (checking models)
To avoid a human translator (writing code)
To reason (verification, validation)
To meet three basic requirements



Reliability: generic and specific properties
Efficiency : performance of the system, the user
(workload, …) and the couple (user, system) tasks
Usability
32
2 – State of the art
Design process using FM
Automatic
Informal
requirements
Specification
Spec 1
...
Spec n
Manual
Verification
Validation
Design
Coding
Progr.
Gener.
Design 1
...
Design n
Prog. 1
...
Prog. n
Verification
Generic
properties
Informal
validation
33
2 – State of the art
The design process of models
P relim in ary
F o rm al an alysis
m o d el
C h eck
D esired
P ro p erties
Ok
Not Ok
M o d el,
i th iteratio n
M en d in g o f
th e m o d el
34
2 – State of the art
Examples of models
(requirements)

A need for a declarative formalismRequirements

Every clearance sent by a controler to a plane p is received
by this plane
" p Planes, " req DLRequest,
AG[send(req,p)]AF<receive(req,p)>true

A data-link clearance sent by a controler to a plane p will
only be received by that plane
" p,p' Planes, " req DLRequest,
AG[send(req,p)]AG[not(receive(req,p')]true
35
2 – State of the art
Temporal Logic CTL *
(Computational Tree Logic Star)
A
state has one or mode successors
 The set of possible states is infinite
 Operators:
A
(all the possible future); E (one possible
future) + {F eventually, G always, X next,
U until}
 Logical

connectors :
(and);  (or);  (not);  (implies)
36
2 – State of the art
Temporal Logic CTL *
si
si |= AGp
si |= AFp
si
si |= EGp
si |= EFp
p formula is true if the system is in red state false otherwise
37
2 – State of the art
Temporal Logic CTL *
si
si
si |= AXp
si
si |= EXp
si
si |= A(p U q)
si |= E(p U q)
38
2 – State of the art
Relating tasks and system
Maintain task and system
models consistency
Formal system modelling
Formal task modelling
Preliminary
system model
i
Preliminary
th
th
i
iteration
iteration
task model
Quantitative
analysis
Proposals for
improving the
system model
Not Ok
Check
Objectives
Ok
Towards
Usability
Testing
39
2 – State of the art
Proving compatibility of
models




All the objects in the tasks model are part of
the data model of the system model
All the actions in the tasks model are offered
by the system model
All the actions in the system model exist in
the tasks models
All the sequences of actions in the tasks
model are "legal" in the system model
40
2 – State of the art
Fundamental elements for
formal methods for IS






Describe both state and events
Describe both data structure and control structure
Provide structuring mechanisms (80% of the code is
dedicated to UI Myers 90)
Take into account concurrency (multimodal systems)
Deals with temporal aspects (temporal windows)
Do it formally (it is easier to prove than to test)
41
2 – State of the art
State versus Events (Dix 91)




Reactive systems
Event driven
Slicing of code into event handlers require
explicit state representations
Approaches



Approaches coming from Reactive Systems
Reactive or synchronous languages (esterel,
Lotos)
Methodological use of Petri nets
42
2 – State of the art
Data Structure / Control
Structure


Software crisis has shown limitations of
separation (maintainability, modifiability,
reusability, ...)
Approaches


Mix two dedicated approaches (CSP-Z, ObjectZ, …)
Integrate two approaches (Full LOTOS, Petri
nets with objects)
43
2 – State of the art
Structuring Mechanisms





Handling of complex components
Understandability of models
Reusability
Modifiability
Approaches



composition (aggregation, association, …)
communication (client-server, actors)
macros and plugs
44
2 – State of the art
Concurrence




Concurrency between input and output
devices (+ multimodality)
Groupware
Multi threaded dialogues
Approaches



Textual formalisms (CSP, CCS, LOTOS, Temporal
Logic)
Graphical formalisms (Petri nets, Statecharts)
Only Petri nets feature full concurrency semantics
45
2 – State of the art
Temporal Aspects

Multimodal systems
Animation (time based evolution)
Alarms
Calendar events

Approaches





Procedural (Petri nets, Lotos, ... )
Declarative (Temporal Logics, ...)
46
2 – State of the art
Formal Aspects





Easier to prove than to test
Critical Systems
Completeness, concision et non-ambiguity
Executability
Approaches



Mathematical validation
Test case generation
Automatic code generation
47
A Small Example/Exercise


Model of a Mouse behaviour (one button, no
wheel)
Model of the interaction technique



Click
Double click
Extensions



Several buttons
Behaviour of the wheel
Several mice
48
2 – State of the art
A Small Example

Requirement:

Whatever state the system is in, Move is always
available
Dow n
Move
Idle
P ressed
Move
Up
49
2 – State of the art
A Small Example
d
Idle
u
d
Down
One_Click
Two_Down
t
C
u
DC
50
2 – State of the art
A Small Example
t
C
d
Idle
u / StartT im er
d
Down
One_Click
Two_Down
t
C
u
DC
Adding Time
51
2 – State of the art
A Small Example
m
C,B
m
D
M ov ing
u
E
m
B
t
C
d, target=this
Idle
u / StartT im er
d
Down
m
C,M
One_Click
Two_Down
t
C
u
DC
Taking Movements into account
52
2 – State of the art
State of the Art in FM for HCI

Understanding interactive systems




What is an IS ?
What are the generic properties of IS ?
Specific properties of IS ?
Engineering interactive systems



What are the components of IS ?
How to model components and their relationships ?
Relationships with design process ?
53
2 – State of the art
Understanding IS

Generic architectures for IS



Generic properties for IS



PIE and red-PIE models (Dix 91)
Seeheim (Green 85) and Arch/Slinky (Bass 92)
(Sufrin & He 90), (Dix 91)
External and internal prop. (Gram & Cockton 96)
Between understanding and engineering


CNUCE interactors (Paternò & Faconti 92)
York interactors (Duke & Harrison 93)
54
2 – State of the art
Engineering IS

Dialogue modelling WIMP



Model-Based UIMS (WIMP) (CADUI'96)






(Bastide & Palanque 90)
(Beck et al. 95)
UIDE (Foley et al. 93)
Tadeus (Elwert & Schlungbaum 95)
PetShop (Bastide & Palanque 95)
TRIDENT (Vanderdonckt 95)
Design Patterns: PAC (Coutaz 87) & MVC
Model-Driven Interactive Systems Engineering
(Vanderdonckt 2002, Paterno 2004) targeting at
multiplatform UI (One model many interfaces)
Paterno 98
55
2 – State of the art
Generic properties

Generic properties for Software Systems




Liveness
Safety
Ability to wear
Generic properties for Interactive Systems





Predictability
Observability
Reachability
Insistence
Honesty, …
56
2 – State of the art
Verification of properties

Observability :


Insistence:


the system makes all relevant information
potentially available to the user
the dialogue structure ensures that necessary
information is perceived
Predictibility:

users can predict future states and system
response time from current and prior observable
states
57
2 – State of the art
References (books)



Formal Methods in HCI, Harrison &
Thimbleby 90, Cambridge University Press
Formal Methods for Interactive Systems, Dix
91, Cambridge University Press
Formal Methods in HCI, Palanque & Paterno
97, Springer Verlag
58
2 – State of the art
References (conferences)









Eurographics workshops DSV-IS (Design, Specification and
Verification of Interactive Systems) since 94 published by
Springer Verlag (LNCS)
CHI 96 workshop on Formal Methods and HCI
CHI 98 workshop on designing user interfaces for safety critical
systems
CHI 05 SIG on Safety Critical Interaction
CHI 07 SIG Beyond Usability for Safety Critical System
HCI Aero 2000 SUCA (Safety and Usability concerns in
Aeronautics)
Mini-track of World Congress on FM 99
FMIS workshop series (Formal Methods for Interactive Systems)
MDAUI workshop series at MODELS conference (formerly UML
conference)
59
2 – State of the art
References (journals)

No dedicated journal



Software engineering journals
HCI journals
Some "special issues"



Interacting with Computers vol 9, n°3, 1997
Journal of Visual Language and Computing (vol
10, n°3, 1999)
ACM Transactions on Computer Human
Interaction (2001)
60
Research Work
carried out at LIIHS
61
Outline of the presentation



Overview of LIIHS Research Group
State of the art in FM for HCI
Research Themes and Productions



Formalisms and tools
Demos
A Roadmap on FM & HCI
62
3 – Research results
Main Results Relevant to
FM in HCI




Vilage (work with S. Chatty at CENA)
 A notation: Whizz
 A case tool: Whizz'ed
SpiderWeb (work with Marco Winckler)
 A notation: StateWebCharts
 A tool: SWC Environment
PetShop
 A formal notation: ICOs
 A case tool: PetShop
User-centered design methods
 Linking tasks, scenarios, system and user models
 Design rationale (lecture on that topic on Wednesday morning)
63
3 – Research results
VILAGE (1)



Initially developed for Air Traffic Controllers
Interactive prototyping of highly interactive
applications (post-WIMP)
Build and test prototypes in a modeless way
64
3 – Research results
VILAGE (2)




A data flow
model
A set of basic
building bricks
Strongly typed
connection
Event listeners
POINT
POINT
Tempo
Trajectoire
Segment
65
3 – Research results
VILAGE (3)
Tool Palete
Dialogue Zone
Editing Zone
Simulation Zone
66
3 – Research results
Overview of the Interactive
Cooperative Objects (1)

Petri nets with objects





Specific aspects for Interactive Systems



Petri nets inside objects
Objects inside Petri nets
Petri nets for dynamic aspects
Objects for structuring
Activation
Rendering
Tool support

Editing, Execution, Analysis, Prototyping
67
3 – Research results
Overview of the Interactive
Cooperative Objects (2)


Set of cooperating classes
For each class




Behaviour (places and transitions) in the Petri net
Software Services (availability)
States (distribution AND value of tokens)
Presentation
 Rendering function
 Activation function
 User services
68
3 – Research results
Verification

What ?






Safety “nothing bad will ever happen”
Liveness “something good will eventually happen”
"Smooth functioning"
"good cooperation between Models"
Efficiency (both local and global)
How ?



Based on Petri nets theory (the basic brick of our system
modelling technique)
Cross execution of models
Performance evaluation techniques
69
3 – Research results
PetShop Fundamental
Principles

Highly interactive tool support for the ICO notation


“Shortening the Path from Specification to
Prototype”


Formal methods can be usable (and useful beyond n!
calculation)
… to practically nothing
Model-Based


The specification model is embedded and interpreted at
run-time WYMIWYR (what you model is what you run) to
reduce gaps in interpretation (Norman's model)
No “Modes” : no “automation surprises”
 The model is editable and interpretable at any time
 Allows for interactive prototyping of new interaction
scenarios
70
3 – Research results
R u n tim e
D e sig n T im e
PetShop Architecture
A naly sis
T ools
G raphical
editor
U I lay out
O bC S
U ser Interface
B uilder
R endering
F unction
A ctivation
F unction
IC O
Interpretor
71
Widget
Event
Service
userAssume
userOpenMenu
Place
Type
Planes
AssumedPl
Plane
LabeClick
Plane
ButtonClick
anes
1)Presentation
2)Behaviour
3)Activation
Feature
ObCS Element
Place Planes
token
<p>
Rendering method
p.show()
4)Rendering
72
3 – Research results
Requirements
A voice request sent to a plane p is received by all the
planes in the sector
" p Planes, " req VRequest,
send (p, req) " p' Planes, receive (p', req)
 It is not possible to build several orders at a time
" p Planes, " req, req' DLRequest,
AF[start_send(req,p)]A[True{not(start_send(req',p)}U(end
_send(req,p)}true]

73
A demonstration ?
74
3 – Research results
ATM in France

Systems currently used




A radar screen
A board of paper strips
Limited interaction with the radar screen
(zoom)
Few systems - a lot of prototypes
3 – Research results
ATM
76
3 – Research results
An Air Traffic Management Case
Study: Current System

VHF communication




all the pilots listen to all the communications
limited bandwidth
low quality
Manual stripping


the controller has to write down by hand all the
information given to pilots
only a note pad and an aide memoire
Envisioned ATM
System
A demonstration !
79
User Centered Design
Methods
Preliminary
needs
User's evaluation
Prototype
& verification
no
yes
adéquat ?
Requirements
Requirements
Maintenance
Final System
Specification
Requirements
Formal specifications
Hi-fidelity prototype
Software
Architecture
Validation
Implementation
and test
Architecture
design
Detailed
design
Unitary
tests
Coding
80
3 – Research results
User Centered Design Methods
PetShop
CTTE
High-fidelity
prototyping
Task model
A demonstration
?
Formal
Scenario
Input
Description of
the System
81
3 – Research results
Routine Scenario





Several aircrafts in my sector
I assume two of them
I have to transfer both of them
2 slips then first aircraft transferred
Second plane directly transferred
82
3 – Research results
A small case study : a timer
controlled light switch

The system




User’s goal



use of a timer controlled switch (30 sec period)
very simple
hardware based (but same as screen saver)
maintain the light on 3 minuts
don’t press the button more than necessary
Two iterations on the life cycle
83
3 – Research results
Task model

What ?





both activity and planned tasks
based on the notion of goal
several task models for a given goal
sequence of user’s actions on the system
How ?


temporal relationships in Petri nets
invocation of actions offered by the system
84
3 – Research results
User Model




Only basic user Models (human processor)
Possibility to describe user learning
Cooperation and/or merging with tasks and
system models
Currently working on higher level user
models (ICS)
85
3 – Research results
Initial System
the light bulb
 the timer
 not possible to
reach the goal

LightOff
PressSwitch
AutoSwitchOff
LightOn
[30]
PressSwitch
86
3 – Research results
First Improvement
Add a stop-watch
 Require hand and eyes

WatchOff
Press
Press
WatchOn
CurrentTime
<t>
87
3 – Research results
The Task model
t > 25
T1
Goal reachable
 Really complex
for the user
ReadyTo
StopWatch
P1

Watch.Press
CountDown
ReadyTo
StartLight
P2
<t>
Watch.Press
T3 Light.PressSwitch
Light
Light Started
Started
CurrentTime
P5
ReadyTo
StartWatch
P3
P6
StartCounting
T5
t := Watch.CurrentTime
T6
<0>
<t>
<t>
T4
P7
t <= 25
T7
P4
Watch Started
<t>
<t>
T2
ReadyTo
ReadTime
P8
88
3 – Research results
Second Improvement


Add a bell
Remove stop watch
LightOff
PressSwitch
AutoSwitchOff
[5]
AutoBeep
LightOn,
Beeping
[25]
LightOn
PressSwitch
PressSwitch
89
3 – Research results
The Task model


Less complex
Less pooling
Start/ Elapsed
CountDown
Light.PressSwitch
Hear beep
Waitting
90
3 – Research results
User model

The perceptual system



The motor system



boundary with the environment
eye : between 50 and 200 ms (average 100 ms)
physical mouvement
hand : between 30 and 100 ms (average 70 ms)
The cognitive sytem


interface between motor and perceptual
brain : between 25 and 125 ms (average 70 ms)
91
3 – Research results
Performance Evaluation of the
first System
(0,n,1,1,0,0,0,0)
T3 / n>=1
n=n-1
T4
(0,n,0,1,0,1,0,0)



based on
marking graph
of the Petri net
based on the
previous user
model
Initial state n=7
(0,n,1,0,0,0,1,0)
T3 / n>=1
n=n-1
T4
(0,n,0,0,0,1,1,0)
T6
(0,n,0,0,0,0,0,1)
T7
T5
(0,n,0,0,1,0,0,0)
T1
(1,n,1,0,0,0,0,0)
T3 / n>=1
n=n-1
T2
(0,n,1,1,0,0,0,0)
T3 / n>=1
n=n-1
T4
(0,n,1,0,0,0,1,0)
(1,n,0,0,0,1,0,0)
T3 / n>=1
n=n-1
(0,n,0,1,0,1,0,0)
T2
T4
92
3 – Research results
Performance Evaluation of the
first System (2)
T1
Cognitive
Comparison of values
T2
Motor
Press button (Stop Watch)
T3
Motor
Press button (Light)
T4
Motor
Press button (Stop Watch)
T5
Cognitive
Comparison of values
T6
-
Nothing
T7
Perceptual
Look at the Stop Watch
93
3 – Research results
Performance Evaluation of the
second System(1)
T1
(7,1,0)
T2
(3,0,1)
(6,1,0)
(7,0,1)
T1
T1
T2
(3,1,0)
T2
(6,0,1)
(5,1,0)
T1
(4,0,1)
T1
T2
(4,1,0)
(5,0,1)
T2
(2,1,0)
(2,0,1)
T1
(1,0,1)
(1,1,0)
T2
T1
(0,1,0)
T2
T1
Motor
Press button (Stop Watch)
T2
Perceptual
Hear the beep
(0,1,0)
T1
94
3 – Research results
Results

First upgrade




Min Time (Goal) = 7*165 + 60 = 1205 ms
Mean Time(Goal) = 7*380 + 140= 2800 ms
Max Time(Goal) = 7*625 + 200 = 4575 ms
Second upgrade



Min Time (Goal) = (8*30) +(7*50) = 590 ms
Mean Time(Goal) = (8*70) + (7*100) = 1260 ms
Max Time(Goal) = (8*200) + (7*100) = 2300 ms
95
Roadmap
on Formal
Methods
in HCI
All Applications
The Invisible UI
2020
No more programming ?
No more bugs ?
2010
Command and
Control Systems
Web Applications
Business Applications
Automated autonomous RealTime Systems (VAL, TCAS)
Target Applications,
Domains
Embodied UI
Tangible User
•Full concurrency
Interface
•Dynamic instantiation
•Hardware/Software Augmented
Reality
•Infinite number of
states
Multimodal
•Tool support
Interaction
•Advanced Analysis
Direct
techniques
Manipulation
UML, E/R, …
B (Atelier B), Z, …
Notations and tools
2007
WIMP
No Interaction
Technique
User Interface Interaction
Technique 96
Descargar

Diapositive 1