Abstract

The complete specification of interactive applications is now increasingly considered a requirement in the field of software for safety-critical systems due to their use as the main control interface for such systems. The reason for putting effort in the use and the deployment of formal description techniques lies in the fact that they are the only means for both modeling in a precise and unambiguous way all the components of an interactive application (presentation, dialogue, and functional core; Pfaff, 1985) and proposing techniques for reasoning about (and also verifying) the models (Palanque & Bastide, 1995). Formal description techniques are usually applied to early phases in the development process (requirements analysis and elicitation) and clearly show their limits when it comes to evaluation (testing). When the emphasis is on validation, iterative design processes (Hix & Hartson, 1993) are generally put forward with the support of prototyping as a critical tool (Rettig, 1994). However, if used in a nonstructured way and without links to the classical phases of the development process, results produced using such iterative processes are usually weak in terms of reliability. They can also be unacceptable when interfaces for safety-critical applications are concerned. If we consider interfaces such as the ones developed in the field of air traffic control (ATC), a new characteristic appears, which is the dynamics of interaction objects in terms of existence, reactivity, and interrelations (Jacob, 1999). In opposition to WIMP (windows, icons, menus, and pointing) interfaces, in which the interaction space is predetermined, these interfaces may include new interactors (for instance, graphical representations of planes) at any time during the use of the application (Beaudouin-Lafon, 2000). Even though this kind of problem is easily mastered by programming languages, it is hard to tackle in terms of modeling. This is why classical description techniques must be improved in order to be able to describe in a complete way highly interactive applications. Document type: Part of book or chapter of book