Formal Notations and Tools
for addressing both Safety
and Usability concerns for
Interactive Systems
Philippe Palanque
LIIHS-IRIT
University Paul Sabatier
Toulouse - France
1
Overview of LIIHS-IRIT (1)

Research themes





Software Engineering for Human-Computer Interaction
Formal description techniques and tools
Visual notations
More dealing with modeling power than with usability of
notations
Application domains



Air traffic control
Military systems (command & control systems)
Web applications
2
Overview of LIIHS-IRIT (2)

LIIHS




6 tenured people mainly HCI (CS and human factors)
5 PhD students
IRIT about 400 people (mainly in CS)
Current projects



RTN ADVISES (Analysis Design and Validation of
Interactive Safety-critical Error-tolerant Systems) 4 years
(starting 11/2002)
MISCC (Multimodal Interactive Systems for Command and
Control) 3 years starting 01/2003
SPIDER Web (Specification and Prototyping for user
Interface Design, Engineering and Re-engineering for the
Web ) started July 2002 (2 years)
3
We are what we publish ;-)

Human-Computer Interaction


Objects Technology


Int. Journal on Visual Languages and Computing
Model-Based Approaches


ATPN (Petri Net conference), FMOODS
Visual Languages


OOPSLA, ECOOP, DOA
Formal Methods


BCS HCI, DSVIS, EHCI, HCI Aeronautics, INTERACT,
Interacting with Computers
CADUI, TAMODIA, IEEE Rapid System Prototyping
Web Applications

Human Factors and the Web
4
Main Results Relevant to
EUD-Net

PetShop



User-centered design methods



A formal notation: ICOs
An interactive editor: PetShop
Linking tasks, scenarios, system and user models
Design rationale (not presented here)
Vilage (work with S. Chatty at CENA)


A notation: Whizz
An editor: Whizz'ed
5
Widget
Event
Service
userAssume
userOpenMenu
Place
Type
Planes
AssumedPl
Plane
LabeClick
Plane
ButtonClick
anes
2)Behaviour
1)Presentation
3)Activation
Feature
ObCS Element
Place Planes
token
<p>
Rendering method
p.show()
4)Rendering
6
PetShop

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
7
Preliminary
needs
PetShop
User's evaluation
Prototype
& verification
no
yes
adequate ?
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
8
User Centered Design Methods
PetShop
CTTE
Task model
High-fidelity
prototyping
Scenario
Formal
Description of
the System
Input
9
VILAGE (1)



Initially developed for Air Traffic Controllers
Interactive prototyping of highly interactive
applications (post-WIMP)
Build and test prototypes in a modeless way
10
VILAGE (1)




A data flow
model
A set of basic
building bricks
Strongly typed
connection
Event listeners
POINT
POINT
Tempo
Trajectoire
Segment
11
VILAGE (3)
Tool Palete
Dialogue Zone
Editing Zone
Simulation Zone
12
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
13
What are we aiming at ?





Kind of applications (one application, every kind of
applications)
Kind of User Interfaces (basic, complex)
Kind of users (skills, expertise in the domain, …)
Spreadsheets are really good for building a fairly
reduced kind of application, basic UI and by a
significant amount of users
L. Lamport "Automaton is a formal description
technique dedicated to the specification of stacks
14
Descargar

Diapositive 1