Reducing the likelihood of human error in the use of interactive systems

is increasingly important: the use of such systems is becoming widespread

in applications that demand high reliability due to safety, security,

financial or similar considerations. Consequently, the use of formal methods

in verifying the correctness of interactive systems should also include

analysis of human behaviour in interacting with the interface.



This report includes pre-event versions of all papers

accepted for presentation at the 1st International Workshop on 

Formal Methods for Interactive Systems (FMIS 2006) held

on 31 December 2006 in Macau SAR China, as a satellite event of

ICFEM 2006. FMIS 2006 is organized by UNU-IIST in collaboration 

with the Human Error Modeling (HUM) project sponsored by

EPSRC on research grants GR/S67494 and GR/S67500.

 

The aim of this workshop is to bring together researchers in computer

science and cognitive psychology, from both academia and industry,

who are interested in developing formal and semi-formal methodologies

and tools for the evaluation and verification of interactive systems.

The outcome is to establish a worldwide network of researchers interested

in applying formal methods to HCI. The workshop focuses on general design

and verification methodologies based on cognitive psychology as well as

application areas such as mobile devices, embedded systems,

safety-critical systems, high-reliability systems, shared control systems,

digital libraries, eGovernment, pervasive systems, augmented reality.



All papers submitted to the workshop were reviewed by 3 referees followed by 

a meta-review process.

From the 18 submissions the Program Committee selected 6 papers for long

presentation (40 minutes) and 2 papers for short presentation (20 minutes).

Revised versions of the 6 papers accepted for long presentations will be

published after the workshop by Elsevier B. V. in the

Electronic Notes in Theoretical Computer Science Series.

The authors of the most relevant papers presented at the workshop

will be invited to submit extended versions of their papers to be

considered for publication in a special issue of a journal.



In addition to contributed papers, the workshop programme also

includes a keynote talk by Harold Thimbleby from the University of Wales,

Swansea. His presentation is entitled "Building dependable interactive systems"

and uses medical devices as a case study to discuss the problems of making

interactive systems dependable. It introduces suggestions for improving  them,

particularly by using formal methods.