Microsoft Word - FMIS2013_Preface.doc Electronic Communications of the EASST Volume 69 (2013) 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 Proceedings of the 5th International Workshop on Formal Methods for Interactive Systems (FMIS 2013) Preface Judy Bowen and Steve Reeves 3 Pages ECEASST 2 / 3 Volume 69 (2013) Preface Judy Bowen and Steve Reeves University of Waikato As for the four previous editions, this fifth edition of the International Workshop on Formal Methods for Interactive Systems (FMIS 2013) is a forum for the presentation and discussion of research into the interface between formal methods and interactive system design. The first paper discusses an integration of evolving and prototyping of interactive systems by a “lightweight” use of formal modelling. Models describe aspects of current and envisaged worlds from different viewpoints (in terms of tasks, of actions on artifacts or of other design constraints). They guide the under-design of the evolving prototype. (Dittmar and Schachtschneider) In the second paper, the authors adopt a stochastic approach and conduct a quantitative investigation of driver behaviour. They use Markovian process algebra PEPA (Probabilistic Evaluation Process Algebra) to describe the overall system model. The system component describing the topology and dynamic of the traffic is composed in parallel with the system component describing the driver state and its evolution, based on empirical evidence. (Cerone and Zhao) The next paper explores how model checking can be complemented with a theorem proving approach for a large subset of the important properties of a system. The paper briefly addresses the translation of MAL models and CTL properties into PVS (Harrison et al.) The fourth paper introduces and talks about PVSio-web, which extends the simulation component of the PVS proof system with functionalities for rapid prototyping. The tool presents itself as a classic image-editing environment with functionalities such as area selection and hyperlink creation, thus reducing the barriers that prevent non-experts in formal methods from using PVS. Designers load a picture of the layout of UI of the device under development, specify interactive areas over the layout, and link them to a PVS specification. (Oladimeji et al.) Fifthly, we have a paper that shows how models built using the Interactive Cooperative Objects formalism (ICOs) are amenable to formal verification. The emphasis is on the behavioural part of the description of the interactive systems and more precisely on the properties at the interaction technique level. (Silva et al.) Our final paper is concerned with a refinement process that demonstrates that a precise requirement is satisfied by the specification of a given device. It focuses on a particular class of requirements that relate to the user interface of the device. For user interface requirements, Preface Proc. FMIS 2013 3 / 3 refinement is made more complex by the fact that systems can use different interaction devices that have very different characters. (Rukšėnas et al.) Previous workshops in this series were held in Limerick (at LERO, and as part of FM 2011, the 17th International Symposium on Formal Methods, June 2011), Eindhoven (November 2009), Lancaster (September 2007) and Macau (October 2006). The latest version of FMIS was co-located with EICS 2013, the 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, held at City University in June 2013. 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 EICS organizers 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!