Tool Support for Interactive Prototyping of Safety-Critical Interactive Applications

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.

FORMAL METHOD FOR AUTOMATED TRANSFORMATION OF LOTOS SPECIFICATIONS TO ESTELLE SPECIFICATIONS

ISO and IEC have jointly developed two Formal Description Techniques (FDTs) for specifying distributed real time systems such as computer/telecommunications protocols. These are Lotos and Estelle. In this paper, a formal method for automated transformation of a Lotos specification to an Estelle specification is presented. The method is applicable to various Lotos specification styles and to various communications protocols of ISO OSI layers. Our method has applications in conformance testing of such systems and building common semantic model for the various FDTs. In this paper, we develop an algorithm for constructing a 'Data Oriented'-Restricted Behavior Tree T that represent both the control flow aspects and the data flow aspects of the system. Then, we develop an algorithm for constructing the Estelle specifications from T. A minimization rule is also developed to optimize the size of the Estelle specification by reducing both the number of states and the number of transitions.