Electronic Communications of the EASST Volume 22 (2009) Proceedings of the Third International Workshop on Formal Methods for Interactive Systems (FMIS 2009) Guest Editors: Michael Harrison, Mieke Massink Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122 http://www.easst.org/eceasst/ ECEASST Preface This volume of the Electronic Communications of EASST contains the proceedings of the third edition of the International Workshop on Formal Methods for Interactive Systems (FMIS 2009). FMIS is a forum for the presentation and discussion of research in the interface between formal methods and interactive system design. This subfield, within applied formal methods, provides interesting challenges to the specification and analysis of systems: what features of interactive systems can be specified that contribute to an understanding of their usability? what analytic techniques are appropriate to assessing whether the design represented by the specification has appropriate properties relating to its use? The theme of the workshop has been admirably scoped by the keynote address: “Who wants a model and why?” in which Muffy Calder reflects on the role of models in recent analyses relating to pervasive and uniquitous systems. This year there were 12 submissions of which 5 have been selected for this volume. All papers were evaluated by at least three reviewers who addressed originality and contribution, technical quality, readability, organisation, presentation and references to related work. The selected pa- pers combine traditional concerns of formal methods in HCI with novel concerns associated with more recent software applications. Bowen and Reeves’ paper focuses on the model based development problem and considers the role of testing in relation to the specification of inter- active systems addressing traditional concerns. It is encouraging to see continuing development of these themes. Several of the papers deal with emerging mainstream application areas includ- ing ubiquitous systems in general and techniques for their analysis (Arapinis and others, Calder and others). These applications require novel analysis from the perspective of human computer interaction. They require focus on interoperability (Arapinis and others) and context awareness (Calder and others). Further papers in this volume focus on particular frameworks and analytic techniques that are required to model and analyse trust-related emotion (Bonnefon and others) and the stochastic properties of software based systems (Anderson and others). Previous workshops in this series were held in Macau (October 2006) and Lancaster (Septem- ber 2007). This year FMIS was co-located with the 16th International Symposium on Formal Methods and was held on November 2, 2009 in Eindhoven, the Netherlands. It has been a privi- lege to be co-located with this international forum for researchers, practitioners and educators in the field of formal methods. We would like to thank all the members of the Programme Committee and the additional referees for their careful and timely evaluation and discussion of the submitted papers. We are also grateful to the FM2009 Conference for hosting FMIS 2009 this year and taking care of many organisational aspects, and to FM Europe for its financial support. Finally, we thank all authors for their submissions without which this workshop could not have taken place, and EASST (European Association of Software Science Technology) and our home institutions Newcastle University and CNR-ISTI for their support. We hope that you will find this volume interesting and thought-provoking and that it will stimulate further research in this interesting and multi-disciplinary field. December, 2009 Michael Harrison Mieke Massink Newcastle University CNR-ISTI FMIS09 Co-Chair FMIS09 Co-Chair 1 / 3 Volume 22 (2009) Organisation Programme Committee Chairs Michael Harrison Newcastle University, UK Mieke Massink National Research Council, CNR-ISTI, Italy Programme Committee Ann Blandford UCL Interaction Center, UK Judy Bowen University of Waikato, New Zealand Paul Cairns University of York, UK José Creissac Campos University of Minho, Portugal Antonio Cerone UNI-IIST, Macau SAR China Paul Curzon Queen Mary, University of London, UK Alan Dix Lancaster University, UK Gavin Doherty Trinity College, University of Dublin, Ireland David Duce Oxford Brookes University, Oxford, UK Stefania Gnesi CNR-ISTI, Pisa, Italy Michael Harrison Newcastle University, UK C. Michael Holloway NASA Langley Research Center, USA Chris Johnson University of Glasgow, UK Mieke Massink CNR-ISTI, Pisa, Italy Philippe Palanque University of Toulouse III, France Luca Simoncini University of Pisa, Italy Daniel Sinnig Concordia University, Canada Harold Thimbleby University of Wales Swansea, Wales External Referees Alessandro Fantechi University of Florence, Italy Proc. FMIS 2009 2 / 3 ECEASST Contents UI-Design Driven Model-Based Testing Judy Bowen and Steve Reeves Towards the Verification of Pervasive Systems Myrto Arapinis, Muffy Calder, Louise Dennis, Michael Fisher, Philip Gray, Savas Konur, Alice Miller, Eike Ritter, Mark Ryan, Sven Schewe, Chris Unsworth and Rehana Yasmin Tightly Coupled Verification of Pervasive Systems Muffy Calder, Phil Gray and Chris Unsworth Markov Abstractions for Probabilistic π -Calculus Hugh Anderson and Gabriel Ciobanu A Logical Framework for Trust-Related Emotions. Jean-François Bonnefon, Dominique Longin and Manh-Hung Nguyen 3 / 3 Volume 22 (2009)