header photo

Raquel Araújo de Oliveira

Research

Keywords: user interfaces, plasticity, formal verification, interactive systems, model checking, equivalence checking, industrial systems

The advent of ubiquitous computing and the increasing variety of platforms and devices change user expectations in terms of user interfaces. Systems should be able to adapt themselves to their context of use, i.e., the platform (e.g. a PC or a tablet), the users who interact with the system (e.g. administrators or regular users), and the environment in which the system executes (e.g. a dark room or outdoor). The capacity of a UI to withstand variations in its context of use while preserving usability is called plasticity.

Plasticity provides users with different versions of a UI. Although it enhances UI capabilities, plasticity adds complexity to the development of user interfaces: the consistency between multiple versions of a given UI (one for each context of use) should be ensured; functionalities that are critical to the system should be preserved in all UI versions; and ergonomic properties the UI is expected to cope with should be satisfied in all its versions. Given the large number of possible versions of a UI, it is time-consuming and error prone to check these requirements by hand. Some automation must be provided to verify plasticity.

This complexity is further increased when it comes to UIs of safety-critical systems. Safety-critical systems are systems in which a failure has severe consequences (e.g. death or injury to people, environmental harm, loss or damage to equipment). The complexity of such systems is reflected in the UIs, which are now expected not only to provide correct, intuitive, non-ambiguous and adaptable means for users to accomplish a goal, but also to cope with safety requirements aiming to make sure that systems are reasonably safe before they enter the market.

Several techniques to ensure quality of systems in general exist, which can also be used to safety-critical systems. Formal verification provides a rigorous way to perform verification, which is suitable for safety-critical systems.  Our contribution is an approach to verify safety-critical interactive systems provided with plastic UIs using formal methods. Using a powerful tool-support, our approach permits:

  • The verification of sets of properties over a model of the system. Using model checking formal technique, our approach permits the verification of  usability and validity properties over the system formal specification. Usability properties verify whether the system follows ergonomic properties to ensure a good usability. These are generic properties that can be applied to any interactive system. Validity properties verify whether the system follows the requirements that specify its expected behavior. These are specific properties that are related to the modeled system, aiming at verifying if the implemented system is conform to the requirement document and/or to safety regulations that constraint the system;
  • The comparison of different versions of UIs. Using equivalence checking formal technique, our approach verifies to which extent UIs present the same interaction capabilities and appearance. We can show whether two UI models are equivalent or not. When they are not equivalent, the UI divergences are listed, thus providing the possibility of leaving them out of the analysis. In this case, the two UIs are equivalent modulo such divergences. Furthermore, the approach shows that one UI can contain at least all interaction capabilities of another (UI inclusion). Three abstraction techniques support the comparison: omission, generalization and elimination.

Although formal methods have considerably evolved in the past years, relatively few case studies of formal methods to industrial systems were reported. We also present in this thesis three industrial case studies in the nuclear power plant domain which the approach was applied to, providing  additional examples of successful use of formal methods in industrial systems.