FMIS 2019

Program

Also available at EasyChair: https://easychair.org/smart-program/FMIS2019/index.html

09h00-10h00 - Session 1 - AFFORD Keynote (joint session)

• Experiences on Streamlining Formal Methods Tools (Paolo Masci, NIA)

10h00-10h30 - Coffee break

10h30-12h30 - Session 2

• A Survey on Formal Methods for Interactive Systems (Pascal Béger, Sébastien Leriche and Daniel Prun)
• Fortune Nets: Formal, Petri nets-based, Engineering of Fortunettes (David Navarre, Philippe Palanque, Sven Coppers, Kris Luyten and Davy Vanacken)
• Model-Based Testing of Post-WIMP Interactions Using Petri-nets (Alexandre Canny, David Navarre, José Creissac Campos and Philippe Palanque)
• Synthesizing Glue Code for Graphical User Interfaces from Formal Specifications (Keerthi Adabala and Rüdiger Ehlers)

12h30-14h00 - Lunch

14h00-15h00 - Session 3 - FMIS Keynote

• Examples of the application of formal methods to interactive systems (Michael D. Harrison, Newcastle)

15h00-15h30 - Coffee break

15h30-17h00 - Session 4

• Formal Modelling of Safety-Critical Interactive Devices using Coloured Petri Nets (Sapna Jaidka, Steve Reeves and Judy Bowen)
• Preliminary Thoughts on User Interfaces for Logic-based Medical Image Analysis (Vincenzo Ciancia and Mieke Massink)
• Modelling Human Reasoning in Practical Behavioural Contexts using Real-time Maude (Antonio Cerone and Peter Csaba Ölveczky)

17h00-17h30 - Plenary discussion and closing

Keynote speakers

• Michael Harrison - Examples of the application of formal methods to interactive systems

Formal methods in interactive systems can be used to analyse how systems support use with a clarity that is not possible with more traditional development approaches. However, the processes involved are complicated and do not fit well with those whose primary concern is user interfaces. The paper reflects on the tools that are used and the problems that hinder their accessibility and comments on tool developments that could lead to wider use of these techniques. The role that existing methods and tools can play in analysing interactive systems will be explored through concrete examples involving the use of the PVS theorem proving assistant and the IVY toolset.

Examples will focus on:

• the formulation and validation of models of interactive systems;
• the expression of use related requirements, particularly in the context of usability engineering and safety analysis;
• the generation of proofs that requirements hold true and making sense when proof fails.

Examples will be taken from existing standalone medical devices including examples from part of a safety analysis of a device leading to product.

• Paolo Masci - Experiences on Streamlining Formal Methods Tools [AFFORD keynote - joint session]

Successful application of formal methods technologies to the development of a system is not just a matter of skillful use of formal methods tools and mathematical analysis techniques. It requires also establishing a constructive dialogue between formal methods experts and a multi-disciplinary team of engineers, domain experts, and end users of the system.

This dialogue is necessary to gain confidence that:

• Formal models correctly capture the characteristics and functionalities of the system under development;
• Formal properties correctly capture the intended meaning of requirements given in natural language;
• Counter-examples produced in formal analysis results point out genuine design issues that need fixing, and not artifacts due to approximations used in the model.

The current generation of formal methods tools are not designed to facilitate this dialogue. They provide text-based front-ends, rich of mathematical details that non-experts of formal methods find hard to understand. These elements create communication barriers that can result in important delays in the development life-cycle, and overall reduced benefits from using formal methods.

This talk discusses a pragmatic approach to streamlining existing formal methods tools. The approach builds on the idea of extending formal methods tools with rapid prototyping capabilities. By this means, formal methods experts can create realistic prototypes that resemble the visual appearance of the system being developed. The behavior of the prototypes is driven by executable formal models. The prototypes can be used to produce interactive demos and scenario-based simulations suitable to discuss all aspects of the formal analysis effort, effectively eliminating the need to show the textual output produced by formal methods tools. Success stories based on the PVSio-web toolkit (www.pvsioweb.org) will be presented to illustrate the benefits of the approach. PVSio-web introduces prototyping capabilities in the PVS verification system. The toolkit has been used successfully over the past five years to support formal analysis of commercial devices and integration of formal methods in existing software development processes. It allowed effective communication of the formal analysis effort to a range of different stakeholders, including device developers, human factors specialists, regulatory agencies, procurement staff, and end users of the final system.