Abstract This paper proposes a unified formal framework, Formal Framework For FLUID (F3FLUID), for the development of safety‐critical interactive systems. This framework is based on the Formal Language of User Interface Design (FLUID) pivot modeling language defined in the FORMEDICIS project, which enables high‐level system requirements for interactive systems to be specified in the FLUID language. This modeling language is specifically designed for handling concepts of safety‐critical interactive systems, including domain knowledge. A FLUID model is used as a source model for the generation of several target models in different modeling languages to support the formal verification methods, such as theorem proving and model checking. In this paper, we use the Event‐B modeling language for checking functional behaviors, user interactions, safety properties, and domain properties. A FLUID model is transformed into an Event‐B model, and then, the Rodin tool is used to check the internal consistency with respect to the given safety properties. We illustrate the operational semantics of the FLUID language, and the transformation strategy of FLUID models into Event‐B models, including the tool development. We use the ProB model checker to analyze the temporal properties and to animate the formalized specification. In addition, an interactive cooperative objects (ICOs) model is derived from the Event‐B model for animation, visualization and validation of dynamic behaviors, visual properties, and task analysis. Finally, an industrial case study, complying with the ARINC 661 standard, Multi‐Purpose Interactive Applications (MPIA), is used to illustrate the effectiveness of our F3FLUID framework for the development of safety‐critical interactive systems.

Training operators of complex interactive systems is a difficult task that involves multiple actors, requires specific competencies and may be extremely costly in terms of time and resources. For instance, an initial training has to be performed in order to bring operators to a desired level of declarative and procedural knowledge. A successful operator will be granted a qualification to operate the system that was used for (or targeted by) the training. However, depending on the nature and the diversity of the operations performed on a daily basis, this initial training may decay and some knowledge may become deprecated. Recurrent training needs to be organised on a regular basis in order to keep operators qualified for the work. Such training differs from initial training and requires taking into account information about how humans learn and forget, what has been performed by operators since last training and the expected required level of knowledge. Trainers need to encompass all this generic information (to all operators) and specific information (to each individual) to define both initial and recurrent training programs. One particularly cumbersome task is the gathering of what happened during operations for each operator in order to minimize recurrent training program to knowledge that might have been forgotten as it was not used in recent operations. We propose a tool-supported task-model approach fed by information of the real work of operators in order to identify complete, relevant and efficient training for operators. These contributions have been applied to the civil aviation domain demonstrating multiple induced benefits.

Abstract Feedback and feedforward are two fundamental mechanisms that support 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. For interactive applications where making a mistake has more impact than just reduced user comfort, correct feedforward is an essential step toward correctly informed, and thus safe, usage. Our approach, Fortunettes, is a generic mechanism providing a systematic way of designing feedforward addressing both action and presentation problems. Including a feedforward mechanism significantly increases the complexity of the interactive application hardening developers’ tasks to detect and correct defects. We build upon an existing formal notation based on Petri Nets for describing the behavior of interactive applications and present an approach that allows for adding correct and consistent feedforward.

The goal of software testing is to detect defects with the objective of removing them at a later stage in the development process. Interactive software development follows the User Centered Design approach that promotes continuous involvement of users both at design and evaluation phases. This process is meant to produce usable interactive software by gathering functional and non-functional requirements related to both user needs and context of use. However, taking into account these potentially very-complex-to-implement requirements increases the complexity of the software that is likely, without appropriate methods and tools, to encompass a large number of defects. One of the limitations of UCD approaches is that it provides no guidance on the engineering of the interactive application, which thus usually embeds numerous defects resulting in failures at the origin of user frustrations and performance drops. Even though a classification of interactive application defects has been proposed, interactive application testers remain only superficially supported in detecting them. This paper defines a model-based approach to engineer the testing activity for interactive applications. It proposes a process that bridges the gap between UCD artefacts and interactive software implementation by the production of a dedicated formal model exploited for testing purposes only. The application of the process is demonstrated on an interactive cockpit WIMP application. Finally, threats to validity (capability of the approach to detect defects and to ensure an acceptable coverage testing of the interactive application) are addressed by a longitudinal study on 61 variants of a simple application developed by 61 different developers. ?

Feedback is commonly used to explain what happened in an interface. What if questions, on the other hand, remain mostly unanswered. In this paper, we present the concept of enhanced widgets capable of visualizing their future state, which helps users to understand what will happen without committing to an action. We describe two approaches to extend GUI toolkits to support widget-level feedforward, and illustrate the usefulness of widget-level feedforward in a standardized interface to control the weather radar in commercial aircraft. In our evaluation, we found that users require less clicks to achieve tasks and are more confident about their actions when feedforward information was available. These findings suggest that widget-level feedforward is highly suitable in applications the user is unfamiliar with, or when high confidence is desirable.

Ensuring that an interactive application allows users to perform their activities and reach their goals is critical to the overall usability of the interactive application. Indeed, the effectiveness factor of usability directly refers to this capability. Assessing effectiveness is a real challenge for usability testing as usability tests only cover a very limited number of tasks and activities. This paper proposes an approach towards automated testing of effectiveness of interactive applications. To this end we resort to two main elements: an exhaustive description of users' activities and goals using task models, and the generation of scenarios (from the task models) to be tested over the application. However, the number of scenarios can be very high (beyond the computing capabilities of machines) and we might end up testing multiple similar scenarios. In order to overcome these problems, we propose strategies based on task models manipulations (e.g., manipulating task nodes, operator nodes, information...) resulting in a more intelligent test case generation approach. For each strategy, we investigate its relevance (both in terms of test case generation and in terms of validity compared to the original task models) and we illustrate it with a small example. Finally, the proposed strategies are applied on a real-size case study demonstrating their relevance and validity to test interactive applications.

Engineering interactive systems for safety critical applications such as in avionic digital cockpits (and more generally Graphical User interfaces) is a challenge from a dependability viewpoint. The dependability of the user interface and its related hardware and software components must be consistent with the criticality of the functions to be controlled and their required DAL levels. This paper proposes a stepwise refinement approach going from systematic identification of failure modes of these systems to their detection via formally defined assertions. The last steps of the approach present how the assertions can be included into the monitoring part of self-checking interactive components and how they can be deployed on an architecture compliant with the ARINC 653 specification, ensuring temporal and spatial segregation, thus detecting errors and preventing failures due to both physical and transient software faults. We present how these contributions have been applied to the Flight Control Unit Backup interactive application which is available in A380 interactive cockpits.

In the last few years, glass cockpits are being replaced by interactive cockpits to provide a higher level of integration of both command and information display. Due to their event driven nature, interactive systems offer more display and control capabilities but they require specific error detection and fault tolerance techniques to reach a high level of dependability. This paper proposes a model-based approach for adding fault tolerance mechanisms to interactive cockpits. While several mechanisms are considered and presented, the contribution is focused on the formal description of self-checking widgets, being the basis for interactive cockpits.

Representing the behaviour of multimodal interactive systems in a complete, concise and non-ambiguous way is still a challenge for formal description techniques (FDT). Depending on the FDT, multimodal interactive systems feature specific characteristics that are either cumbersome or impossible to capture with classical FDT. This is due to the multiple (potentially synergistic) use of modalities and the strong temporal constraints usually encountered in this kind of systems that have to be dealt with exhaustively if FDT are used. This paper focuses on the requirements for the modelling and construction of fusion engines for multimodal interfaces. It proposes a formal description technique dedicated to the engineering of interactive multimodal systems able to address the challenges of fusion engines. Such benefits are presented on a set of examples illustrating both the constructs and the process.

The design of real-life complex systems calls for advanced software engineering models, methods, and tools in order to meet critical requirements such as reliability, dependability, safety, or resilience that will avoid putting the company, the mission, or even human life at stake. When such systems encompass a substantial interactive component, the same level of confidence is required towards the human-computer interface. Conventional empirical or semiformal techniques, although very fruitful, do not provide sufficient insight on the reliability of the human-system cooperation, and offer no easy way to, for example, quantitatively and qualitatively compare two design options with respect to that reliability. The aim of this article is to present a user interface description language (called ICOs) for the engineering and development of usable and reliable user interfaces. The CASE tool supporting the ICOs notation (called Petshop) is a Petri nets-based-tool for the design, specification, prototyping, and validation of interactive software. In that environment models (built with the formal description technique ICOs) of the interactive application can be interactively modified and executed. This is used to support prototyping phases (when the models and the interactive application evolve significantly to meet late user requirements, for instance) as well as the operation phase (after the system is deployed). The use of ICOs and PetShop is presented on several large-scale systems such as a multimodal ground segment application for satellite control, an air traffic control interactive application, and an application for new generation of interactive cockpits in large civil aircraft such as Airbus A380 or Boeing 787. The article emphasizes the demonstration of the expressive power of the notation and how it can support the description of various aspects of user interfaces, namely interaction techniques (both WIMP and post-WIMP), interactive components (such as widgets), and the behavioral part of interactive applications such as the dialog and the functional core. It also demonstrates that PetShop provides dedicated support for prototyping activities of behavioral aspects at the various levels of the architecture of interactive systems. While the focus is on past work done on various large-scale applications, the article also highlights why and how ICOs and Petshop are able to address challenges raised by next-generation user interfaces.

This paper is an extended version of the final version of a paper accepted at EHCI-DSVIS 2004, Lecture Notes in Computer Science n°3425

This paper presents the use of a model-based approach for the formal description of real-time embedded multimodal systems. This modeling technique has been used in the field of military fighter aircrafts. The paper presents the formal description techniques, its application on the case study of a multimodal command and control interface for the Rafale aircraft as well as its relationship with architectural model for interactive systems.

This paper presents a design framework for safety critical interactive systems, based on a formal description technique called the ICO (Interactive Cooperative Object) formalism. ICO allows for describing, in a formal way, all the components of highly interactive (also called post-WIMP) applications. The framework is supported by a case tool called PetShop allowing for editing, verifying and executing the formal models. The first section describes why such user interfaces are challenging for most description techniques, as well as the state of the art in this field. Section 3 presents a development process dedicated to the framework. Then, we use a case study in order to recall the basic concepts of the ICO formalism and the recent extensions added in order to take into account post-WIMP interfaces' specificities. Section 5 presents the case tool PetShop and how the case study presented in the previous section has been dealt with. Lastly, we show how PetShop can be used for interactive prototyping.

CORBA is now established as one of the main contenders in object-oriented middleware.Beyond the definition of this standard for distributed object systems, the Object Management Group (OMG) has specified several object services (Common Object Services, COS) that should foster the interoperability of distributed applications.Based on experiment, the goal of this paper is to show that the OMG's style of specification of the CORBA services is not suited to guarantee that implementers will produce interoperable and substitutable implementations.To illustrate our point, we give an account of an experiment based upon the formal specification of one COS, namely the CORBA Event Service.This formal specification highlights several ambiguities and under-specifications in the OMG document.We then test several commercial and public domain implementations of the CORBA Event Service, in order to assess how the implementers have dealt with these underspecifications.We show that the choices made by the implementers lead to incompatible implementations.We finally suggest a solution to overcome the problem of specification of object services, which satisfies the views of both implementers and users.Specifically, we suggest that the specification of such services be made using a formal description technique, and that implementers be provided with test cases derived from the formal specification.