Electronic Communications of the EASST Volume 45 (2011) Proceedings of the Forth International Workshop on Formal Methods for Interactive Systems (FMIS 2011) Preface 1 pages Guest Editors: Judy Bowen, Steve Reeves 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 As for the three previous editions, this fourth edition of the International Workshop on Formal Methods for Interactive Systems (FMIS 2011) is a forum for the presentation and discussion of research into the interface between formal methods and interactive system design. This year, due to the demise of several workshops at FM, we also had (very welcome) submissions from the pervasive computing community. Our invited speaker this year is Chris Johnson from the University of Glasgow. His paper looks at how formal reasoning techniques can be used to identify safety and security around interaction, with particular reference to future generations of Global Navigation Satellite Systems applications. Other papers present a validation study of an existing generic model of user behaviour (H. Huang et al.), the scalable and systematic analysis of interactive systems (using the infusion pump as an example; Campos and Harrison), a formalization of DiCoT, an informal structured approach for analysing complex work systems, as distributed cognition systems (Masci et al.), abstract modelling of hybrid systems and their automated analysis as supported by an SMT solver (Bass et al.), a process algebraic framework to formalise a model of automatic behaviour (Cerone), a process algebraic description of a model of coordination (Bhandal et al.), a sys- tematic approach to dealing with the unavoidable errors in data entry (Thimbleby and Gimblett), formalising predictability of a user interface (Masci et al.), work on accommodating fine-grained analysis of cognitive mismatch in interactive systems via model checking (Rukšėnas and Cur- zon) and an approach for supporting mobile application development by using models as inputs to an emulator (Bowen and Hinze). Previous workshops in this series were held in places as diverse as Eindhoven (November 2009), Lancaster (September 2007) and Macau (October 2006). This year FMIS is co-located with FM 2011, the 17th International Symposium on Formal Methods. The main conference includes many other workshops and also tutorials covering all aspects of formal methods, and it is heartening to see that “side” of FMIS in such health. That FM and its workshops are being held at LERO (the Irish SE research centre in Limerick) seems very appropriate, and we are pleased that FMIS attracted enough support (presenters and authors as well as participants) to be invited into the FM fold once again. As ever, we wish to thank all the members of the Programme Committee for their time and expertise in considering and discussing the submitted papers. We also wish to thank the FM or- ganisers for inviting us and supporting us. Thanks also The University of Waikato for supporting us. We must, of course, most importantly, also thank the authors for their contributions! Finally, thanks to ECEASST for publishing, once again our proceedings. The programme was, as ever, interesting, engaging and, hopefully, has provoked some lively exchanges. We hope that you find the papers here both entertaining and useful! Judy Bowen and Steve Reeves FMIS 2011 co-Chairs The University of Waikato Hamilton, New Zealand 1 / 1 Volume 45 (2011)