Course on

Formal Modelling and Analysis of
Interactive Systems


Course Abstract | Course Slides | Examination Procedure | Assignements

Course Abstract

The course will start by illustrating the challenge of taking human errors into account while modelling interactive systems and by investigating the nature and aspects of human error with reference to practical examples.
It will then present how to incorporate human behaviour in the modelling of interactive systems and how to apply model-checking methodologies to the formal analysis of such systems. This part of the course will focus on important cognitive aspects of human behaviour, such has the role of short-term memory in goal-based tasks and the switching between automaticity and attention, as well as the emergence of cognitive errors and their detection using model-checking.
Finally the course will show how to formalise task failures, how to use model-checking to verify the soundness and completeness of a task failure decomposition and how to give a psychological interpretation to the outcome of the model-checking analysis.

Course Slides and Code

One single file containing all parts: presentation version | printable version

Separate files (presentation versions):
  1. Introduction - Slides.
  2. Formal Tools and HCI Concepts - Slides, Code.
  3. Formal Analysis and Cognitive Models - Slides, Code,
  4. Tasks and Task Failures - Slides, Code,
  5. Usability and Security - Slides, Code.
  6. Examination Assignments - Slides.

Examination Procedure

Written Report on research topic suggested by the lecturer or proposed by the student.
Each report may be co-authored by at most two students, unless explicitly specified in the assignment description.
If two or more students co-author the same report, it is mandatory to specify in the introduction to which part and in which measure each student contributed to the work and to the writing of the report.
Deadline: 31 March 2011

Assignements


R-1 User Interface Design: Paper 1 | Paper 2 | Paper 3
Type: written report
expression of interests: Daniele Bernabei, Dung Dinh, (Gabriele Costa).
still available

R-2 Salience and Expectancy in Attention: Paper 1 | Paper 2
Type: written report
expression of interests: Aureliano Rama, Daniele Bernabei, Davide Spano.
This report may be co-authored by up to three students, each working in one the three possible direction specified in the assigment description. It is also possible for up to three students to work indipendently to three separate report, each in one the three possible direction specified in the assigment description.
Directions:

R-3 Planned versus Reactive Behaviour: Paper 1 | Paper 2
Type: written report
expression of interests: (Daniele Bernabei), Davide Spano.
assigned to: Davide Spano

R-4 Model of ATM using Abstract Data Types: Paper 1 | Paper 2
Type: code development and short written report
expression of interests: Aureliano Rama.
assigned to: Aureliano Rama

R-5 Qualitative Extension of the ATC Case Study: Paper 1 | Paper 2 | Paper 3
Type: code development and short written report
expression of interests: none.
still available

R-6 Quantitative Extension of the ATC Case Study: Paper 1 | Paper 2 | Paper 3
Type: written report
expression of interests: none.
still available

R-7 Trust in Interaction and Usability: Paper 1 | Paper 2 | Paper 3 | Paper 4
Type: written report
expression of interests: Leanid Krautsevich, Gabriele Costa, Dung Dinh.
independently assigned to:


Created: Wed Dec 29 11:20:54 CET 2010 Feedback
Updated: Tue Feb 22 02:40:53 CET 2011