dr. Antonio CERONE
Research Fellow
United Nations University
Macau
China
-----------------------------------
          
Formal Analysis of Human-computer Interaction using Model-checking
-----------------------------------
          
ABSTRACT
-----------------------------------
The widespread use of computers in safety-critical and security
systems increases the need for human-computer interaction to
be designed in a way that reduces the likelihood of human errors.
Experiments with simulators allow psychologists to better understand
the causes of human errors and build formal models of cognitive
processes.

This seminar introduces an approach to task failure analysis
based on patterns of behaviour, by contrast to more traditional
event-based approaches. The approach is applied to a model of
an air traffic control (ATC) system which incorporates controller
behaviour. The cognitive model is formalised in the CSP process
algebra. Patterns of behaviour are expressed as temporal logic
properties. Then a model-checking technique is used to verify
whether the decomposition of the operator's behaviour into patterns
is sound and complete with respect to the cognitive model. The
decomposition is shown to be incomplete and a new behavioural
pattern is identified, which appears to have been overlooked
in the analysis of the data provided by the experiments with
the simulator. This illustrates how formal analysis of operator
models can yield fresh insights into how failures may arise
in interactive systems.
          
SHORT CV
-----------------------------------
Dr.Antonio Cerone joined the International Institute for Software
Engineering (IIST) of the United Nations University (UNU) in
February 2004. 
His research focuses on formal methods and their application
to information security, asynchronous hardware, interactive
systems, concurrent and real-time systems, and safety-critical
systems.
Before joining the UNU-IIST, dr.Cerone held research positions
at the Software Verification Research Centre (SVRC), the Advanced
Computing Research Centre (ACRC) of the University of South
Australia (UniSA), the University of Frankfurt, Germany.
Dr.Cerone completed his PhD in 1993 and his Master's degree
in 1989, both at the University of Pisa, Italy.