ABSTRACT. Our research team is specialized in human-computer systems and their engineering, with focus on interactive software systems for aeronautics (from cockpits to control towers). This context stands out by the need for certification, such as DO-178 or ED-12. Today, formal methods are pushed forward, as one of the best tools to achieve the verification and validation of properties, leading to the certification of these systems. Interactive systems are reactive computer systems that process information from their environment and produce a representation of their internal state. They offer new rich interfaces with sophisticated interactions. Their certification is a challenge, because the validation is often a human based process (mainly test based) since traditional formal tools are not always suitable to the verification of graphical properties in particular. In this paper, we explore the scientific work that has been done in formal methods for interactive systems over the last decade, in a systematic study of publications in the International Workshop on Formal Methods for Interactive Systems. We describe an analytical framework that we apply to classify the studied work into classes of properties and used formalisms. We then discuss the emerging findings, mainly the lack of papers addressing the formal specification or validation of perceptibility properties. We conclude with an overview of our future work in this area.

ABSTRACT. Feedback and feedforward are two fundamental mechanisms supporting users’ activities while interacting with computing devices. While feedback can be easily solved by providing information to the users following the triggering of an action, feedforward is much more complex as it must provide information before an action is performed. Automatic feedforward presents in a systematic way to the users what can be done without requiring any dedicated action (e.g. greying out an interactive object that is not available). Automatic feedforward is often availa-ble in well-designed interfaces. User-triggered feedforward provides localized, contextual information to the users related to the actions that they envision triggering (e.g. painting temporarily a selected object in yellow while hovering the yellow button for painting objects). User-triggered feedforward is usually not available in user interface, as it requires computing the future state of the application (if a given action is performed) and presenting this future state on the UI. Fortunettes is a generic mechanism providing a systematic way of designing feedforward addressing both action and presentation problems. Including feed-forward mechanism significantly increases the complexity of the interactive application hardening developers’ tasks to detect and correct defects. This paper pro-poses the use of a formal notation for describing the behavior of interactive applications and how to exploit that formal model to extend the behavior to offer feed-forward. We use a small login example to demonstrate the process and the results.

ABSTRACT. Model-Based Testing (MBT) relies on models of a System Under Test (SUT) to derive test cases for said system. While Finite State Machine (FSM), workflow, etc. are widely used to derive test cases for WIMP applications (i.e. applications depending on 2D widgets such as menus and icons), these notation lack the ex-pressive power to describe the interaction techniques and behaviors found in post-WIMP applications. In this paper, we aim at demonstrating that thanks to ICO, a formal notation for describing interactive systems, it is possible to gener-ate test cases that go beyond the state of the art by addressing the MBT of ad-vanced interaction techniques in post-WIMP applications.

ABSTRACT. The glue code of a graphical user interface (GUI) is responsible for reacting to user input by changing the state of the user interface and triggering the computation to be performed.

Here, we present an approach to synthesize such glue code. Our approach combines several ideas that work best in combination. We start from specifications in linear temporal logic (LTL) that express the desired interaction between the UI and the backend of the program. Our synthesis approach employs ideas from automata theory to the special case of user interfaces. Traditional synthesis approaches target hardware that is clocked, which is not appropriate for UIs.

ABSTRACT. Formal modelling is now widely applied for creating models of safety-critical interactive systems. Most approaches built so far either focus on the user interface or on the functional part of a safety-critical interactive system. This paper aims to apply formal methods for modelling and specifying the user interface, interaction and functional aspects of a safety-critical system in a single model using Coloured Petri Nets. We have used Coloured Petri Nets because of its expressive graphic representation and the ability to simulate the system behaviour. The technique is illustrated through a case study of the Niki T34 Infusion Pump.

ABSTRACT. Spatial logic and spatial model checking may provide domain experts with a convenient and very concise way to specify contouring and segmentation operations, grounded on the solid mathematical foundations of Topological Spatial Logics. Recent results in the domain of brain tumour segmentation have shown that this approach has the potential to reach comparable accuracy and computational efficiency as other state-of-the-art techniques in this domain. One of the open challenges, specific for this approach, is how such a technique could be best embedded into the common workflow of clinicians and radiologists. In particular, domain experts involved in research would profit from a set-up and user interface that would also support collaboration and exchange of expertise among medical physicists, engineers and technicians. We briefly describe some related work, setting, aims, and challenges for such an integrated interface.

ABSTRACT. In this paper we present an approach for modelling human reasoning using rewrite systems and we illustrate our approach in the context of human behaviour through a car driving example. Reasoning inference rules and descriptions of human activities are expressed using the Behavior and Reasoning Description Language (BRDL). The BRDL model is then translated into Real-time Maude. The object-oriented and equational logic aspects of Maude are exploited in order to define alternative semantic variations of BRDL that implement alternative theories of memory and cognition.