Abdelkrim Chebieb
email: k_chebieb@esi.dz

Yamine Ait Ameur
email: yamine@enseeiht.fr

A formal model for plastic human computer interfaces

Keywords: formal modeling and veriÞcation, ontology based modeling, plastic user interfaces, adaptive systems

The considerable and signiÞcant progress achieved in the design and development of new interaction devices between man and machine has enabled the emergence of various powerful and efficient input and/or output devices. Each of these new devices brings speciÞc interaction modes. With the emergence of these devices, new interaction techniques and modes arise and new interaction capabilities are offered. New user interfaces need to be designed or former ones need to evolve. The design of so called plastic user interfaces contributes to handling such evolutions. The key requirement for the design of such a user interface is that the new obtained user interface shall be adapted to the application and have, at least, the same behavior as the previous (adapted) one. This paper proposes to address the problem of user interface evolution due to the introduction of new interaction devices and/or new interaction modes. More, precisely, we are interested by the study of the design process of a user interface resulting from the evolution of a former user interface due to the introduction of new devices and/or new interaction capabilities. We consider that interface behaviors are described by labelled transition systems and comparison between user interfaces is handled by an extended deÞnition of the bi-simulation relationship to compare user interface behaviors when interaction modes are replaced by new ones.

Introduction

A user interface is often designed, after some reÞnement steps, for predeÞned interaction devices and platforms. Each device, platform and environment is characterized by its own interaction modes. When a user interface (UI) is designed to run on several target platforms 1) and to support different interaction modes and/or devices, it can be considered as satisfying the plasticity property (also qualiÞed to be a plastic UI). Indeed, a plastic UI shall be able to switch, statically (at design time) or dynamically (at runtime), from a given platform to another. The target platform may support (exactly, less or more) interaction capabilities than the original one corresponding to (equivalent, degraded or upgraded) user interface.

With the emergence of new devices, new interaction techniques and modes arise. Indeed, when such devices are deployed to interact with hardware controllers, games, critical applications like medicine or aircraft cockpits, classical software applications, etc., new interaction capabilities are enabled. Therefore, either new user interfaces need to be designed and veriÞed for the obtained system or the former user interface needs to evolve. In other words, some of these user interfaces result from the evolution of the former user interface due to the introduction and/or to the substitution of one or more devices by other ones. In some cases, other user interfaces may require to build a completely new user interface taking into account the introduced new devices including their new interaction modes. As a consequence, the obtained user interface (being either a new one or the evolution of a former one) requires to be (partly or fully) re-designed, re-veriÞed and re-validated although this new user interface (to be deÞned) still interacts with the same application. The key requirement for the design of such a user interface is that the new obtained user interface shall be adapted to the application and have, at least, the same behavior as the previous one.

The previously identiÞed requirement advocates for the design of so called plastic user interfaces. In this case, the design relies on the concept of plasticity and plastic user interfaces [START_REF] Thevenin | Plasticity of user interfaces: framework and research agenda[END_REF]. Plasticity is an important property to ensure the safety and usability of interactive systems which is one of ISO/IEC 9126-1 usability quality of service criteria [START_REF] Coutaz | HCI and software engineering for user interface plasticity[END_REF]. It aims at supporting user interface adaptation to several running situations by providing another design model of the whole or part of the user interface. In a dynamic setting, this feature is particularly useful to pursue interacting with the system even if a failing situation occurs [START_REF] Navarre | A formal approach for user interaction reconÞguration of safety critical interactive systems[END_REF].

The description of the behavior of user interfaces is a major concern in user interface engineering areas. Several approaches, notations, techniques, processes and methods have been proposed in the literature. Compared to classical software engineering, the design of user interfaces pays a lot of attention to the usability of the designed interface. One of the techniques allowing a designer to handle this usability characteristic in the behavior description is user task speciÞcation and analysis. Indeed, a set of user tasks is deÞned beside or within the user interface speciÞcation in order to describe expected and/or unexpected user interface behaviors. Tasks are deÞned by different actors involved in the description of the user interface (e.g., ergonomists, psychologists, users corresponding to speciÞc proÞles like pilots for cockpits interfaces, etc.). DeÞned user tasks contribute to the veriÞcation and validation of the user interface, they deÞne use cases and scenarios. Validation and veriÞcation activities consist in checking that the deÞned user tasks are supported or not supported by the designed user interface. This checking is ensured by any validation and/or veriÞcation technique like testing, simulation, experimentation, formal proofs, model checking, etc.

This paper proposes to address the problem of user interface evolution due to the introduction of new interaction devices and/or new interaction modes. More, precisely, we are interested by the study of the design process of a user interface resulting from the evolution of a former user interface due to the introduction of new devices and/or new interaction capabilities. This paper claims to handle the plasticity charac-teristic of user interfaces by answering to the question: does a target user interface U T resulting from the evolution (by introducing new interaction devices or interaction modes) of a source user interface U S behave as U S ? To provide with answers to this question, one should be able to formally compare the behaviors of each of the considered user interfaces U S and U T .

In order to set up our proposal for handling plastic interfaces and checking the capability of a user interface to be replaced by another one, we consider that

• user interfaces are viewed as task models, and formally described as state transitions systems,

• devices and associated interaction modes are formally represented within a knowledge model carried out by a domain ontology,

• and Þnally, the problem of interfaces behaviors comparison is handled using the classical techniques for comparing state transitions systems. A revisited deÞnition of the classical bi-simulation relationship is provided.

This paper is structured as follows. Section 2 addresses the design of human centered computer interfaces, it gives an overview of the different techniques developed to deÞne user tasks models. Section 3 focuses on the concept of user interface plasticity. It reviews the basic deÞnitions and surveys the state of the art in the design of plastic user interfaces. It also shows how devices and interaction modes can be modeled as an explicit knowledge domain, i.e., an ontology. In Section 4, the core principles of the proposed approach are presented. Then, Sections 5 and 6 revisit the deÞnition of the bisimulation relationship needed to compare user task models. The whole formal model for verifying plastic user interfaces and the plasticity property is presented in Section 7 where the different steps leading to analyze formally plastic user interfaces are composed into a sequence of methodological steps. Section 8 is devoted to the development of our approach on two illustrative case studies. The use of a model checker for formal veriÞcation of plastic user interfaces is described in this section as well. Finally, Section 9 concludes this work and gives some future research directions.

Design of human computer interfaces: task modelling

During the user interfaces speciÞcation, design, validation and experimentation processes, task modeling allows user interfaces developers to capture usability characteristics through the deÞnition of scenarios of use. These processes heavily rely on the deÞnition of user tasks to be supported by the user interface under design. The described tasks shall be handled by the user interface whatever are the environment and the platform where this user interface is set up. This requirement deÞnes the notion of abstract task to be handled by every user interfaces designed to interact with the considered system. The usability of the user interface is checked by asserting that the deÞned user tasks are handled by the interface. In case of evolution of the user interface (e.g., new interaction device or mode), the deÞned tasks shall be checked again to ensure interface adaptation. Therefore, as mentioned above, task models suit for plasticity of user interfaces checking.

Note that other notations and modeling languages are available for design and speciÞcation of user interfaces. In this paper, we focus on task models. In the remainder of this section, we review the main research work related to formal user tasks modeling and give an overview of the concur task tree (CTT) user task modeling language deÞning a process algebra and used in our approach for tasks description.

User task modeling

Task modeling, initially used for requirement analysis and knowledge speciÞcation, is the starting point of user interface design and development best practices [START_REF] Calvary | The cameleon reference framework. Deliverable D1 of the Cameleon project[END_REF]. It is the backbone of user interface development process. Indeed, task modeling has been used in several situations : to derive several user interfaces like in TERESA [START_REF] Mori | Tool support for designing nomadic applications[END_REF], to determine facets in agent multi facets (AMF) [START_REF] Samaan | Prise en Compte du Modèle d'Interaction dans le Processus de Construction et d'Adaptation d'Applications Interactives[END_REF], to determine task view point in multi-path development [START_REF] Limbourg | Usixml: a language supporting multi-path development of user interfaces[END_REF], etc. Their common objective is to develop usable and useful systems [START_REF] Coutaz | HCI and software engineering for user interface plasticity[END_REF].

The study of task modeling languages and techniques has drawn user interaction researcher's attention since the 80's. Tasks may be described at different levels:

• an abstract level for the description of the task actions to be performed through the user interface and at

• a concrete level depending on the available devices and interaction modes within a given platform or environment.

The expressive power of task modeling languages resides in their capability to describe different levels of the task: abstract level, syntax (or structural) level and concrete (or keystroke) level. Indeed, according to [START_REF] Palanque | Formal Methods in Human-Computer Interaction[END_REF], in general a task model is composed of three layers. First, a top layer describes the task to be achieved at the abstract level. Second, a mid layer models the dialogue and indicates the user actions (cognitive decisions), system action and interactive actions (shared between a user and a machine or a system). Finally, the third (bottom) layer is a concretization. It models the physical actions (keystroke interactions) needed to perform the described task depending on available interaction devices of the platform where the system is expected to run.

Several techniques, notations and editing tools are dedicated to process and analyze task models. The most known in the literature are UAN [START_REF] Hartson | The UAN: a user-oriented representation for direct manipulation interface designs[END_REF][START_REF] Rix | Developping User Interfaces: ensuring Usability Through Product & Process[END_REF], XUAN, Xuan, HTA [START_REF] Dix | Human-Computer Interaction[END_REF], CTT [START_REF] Paternò | Concurtasktrees: a diagrammatic notation for specifying task models[END_REF][START_REF] Paternò | Integrating model checking and HCI tools to help designers verify user interface properties[END_REF], MAD [START_REF] Scapin | Towards a method for task description: MAD[END_REF] and MAD* [START_REF] Scapin | Analyse des tâches et aide ergonomique à la conception: l'approche mad*[END_REF] and its tool KMADE [START_REF] Sybille | Increasing the expressive power of task analysis: systematic comparison and empirical assessment of tool-supported task models[END_REF].

Formal modeling and veriÞcation of user tasks

The use of formal methods for the validation of user interfaces and particularly task models has been studied by several authors. Various techniques, tools and models have been proposed as a solution to support human centered design such as task modeling [START_REF] Paternò | Concurtasktrees: a diagrammatic notation for specifying task models[END_REF], task achieving veriÞcation [START_REF] Chebieb | Analyse et evaluation de propriétés dans les ihm[END_REF] multimodal user interface [START_REF] Ameur | A generic formal speciÞcation of fusion of modalities in a multimodal HCI[END_REF], and user driven design [START_REF] Palanque | Petri net based design of user-driven interfaces using the interactive cooperative objects formalism[END_REF]. Tasks descriptions are formally modeled by labelled transition systems (lts). This representation makes it possible to target several formal veriÞcation techniques. Indeed, to encode task models as labelled transition systems, Petri Nets [START_REF] Navarre | ICOs: a model-based user interface description technique dedicated to interactive systems addressing usability, reliability and scalability[END_REF], process algebra, based on the LOTOS with CTT and CTTE [START_REF] Paternò | Concurtasktrees: a diagrammatic notation for specifying task models[END_REF][START_REF] Paternò | CTTE: an environment for analysis and development of task models of cooperative applications[END_REF], state based methods with B and Event-B [START_REF] Ameur | Encoding a process algebra using the event B method: application to the validation of human-computer interactions[END_REF][START_REF] Mohand-Oussaïd | Modelling information Þssion in output multi-modal interactive systems using event-B[END_REF] or Z [START_REF] Duke | Event model of human-system interaction[END_REF], model checking and temporal logics by [START_REF] Brun | XTL: a temporal logic for the formal development of interactive systems[END_REF][START_REF] Ausbourg | Using model checking for the automatic validation of user interface systems[END_REF][START_REF] Ameur | A generic formal speciÞcation of fusion of modalities in a multimodal HCI[END_REF], etc., are some of the approaches that have been proposed in the literature so far. These approaches show the attention carried out by research to the problem of formal modeling and ver-iÞcation of task models for both WIMP or post-WIMP user interfaces.

The concur task tree (CTT) notation

CTT is a notation for task model speciÞcation used to design interactive applications. It provides a designer with a notation to describe tasks expressions combining temporal operators of a process algebra à la CCS (Calculus of Communicating Systems [START_REF] Milner | A Calculus of Communicating Systems[END_REF]) and atomic tasks (user physical or keystroke actions on interaction devices). A CTT task model describes a hierarchy of tasks represented by a tree-like structure, where each node represents a composition operator and each leaf is an atomic task. It requires identiÞcation of temporal relationships between sub-tasks of the same tree level. These operators are borrowed from the LOTOS process algebra [START_REF] Lotos | A formal description technique based on the temporal ordering of observational behaviour[END_REF]. The available CTT composition operators describe activation (T i ≫ T j ), choice (T i [ ] T j ) order independence (T i | =| T j ), interleaving T i ||| T j , parallel tasks (T i || T j ) and iteration (T * ).

Figure 1 corresponds to the decomposition tree describing the T

3 [ ](T 7 | =| T 8 ) ≫ (T 5 ||| T 6 ) task expression. [ ] T 0 T 1 T 2 T 5 T 6 T 8 T 7 T 3 T 4
Fig. 1 Example of CTTE task model

Plastic user interfaces

The concept of interface plasticity is deÞned by Thevenin et al. [START_REF] Thevenin | Plasticity of user interfaces: framework and research agenda[END_REF] as the capacity of a user interface to adapt itself or to be adapted to the context of use (environment, platform and user proÞle) while preserving usability.

Some characteristics of plasticity

The capability of a user interface to adapt itself or to be adapted is possible only if the user interface is adaptable and adaptive. These two relevant characteristics, i.e., adaptivity and adaptability, relate to plasticity. Adaptivity concerns a UI capable to adapt itself to a target platform, while adaptability characterizes a UI that allows a user to adapt it to a target platform. Adaptation of the UI impacts not only its software part, but also the involved devices and interaction modes, available for this platform. Following [START_REF] Dictionary | Cambridge Dictionaries Online[END_REF], Adaptability is the capacity to change and adaptivity is the capacity to accept changes.

According to [START_REF] Vanderdonckt | A design space for context-sensitive user interfaces[END_REF], a user interface is adaptable when it allows a user or a designer the possibility to adapt it. It is adaptive when it adapts itself to occurring changes. A user interface is often designed for predeÞned interaction devices and platforms, and each platform and environment is characterized by its own interaction modes. Plasticity is an important property to ensure the safety and usability of interactive systems which is one of ISO/IEC 9126-1 usability quality of service criteria [START_REF] Coutaz | HCI and software engineering for user interface plasticity[END_REF]. It aims at supporting UI adaptation to several running situations by re-modeling a part of or the whole user interface. This is particularly useful to continue interacting with the system even if failing situations occur [START_REF] Navarre | A formal approach for user interaction reconÞguration of safety critical interactive systems[END_REF]. The continuity of the interaction is an important concern to be taken into account when a user interface is de-signed.

Previous work

Nowadays, it is well accepted that plasticity is an important characteristic [START_REF] Thevenin | Plasticity of user interfaces: framework and research agenda[END_REF], to be addressed during the user interface design process. Studying plasticity of user interfaces has drawn the attention of researchers. The work [START_REF] Coutaz | HCI and software engineering for user interface plasticity[END_REF] records that several plastic UI design approaches focused on the software parts of a user interface, at the expense of interaction and dialogue parts.

Previous research work addressing plasticity suggested technical solutions to address the problem of user interface adaptation.

One can mention solutions based on speciÞc software developments at the adaptation level like the Adaptive toolkit ACE [START_REF] Johnson | ACE: building interactive graphical applications[END_REF], FRUITS [START_REF] Kawai | Designing interface toolkit with dynamic selectable modality[END_REF], Multimodal Widgets [START_REF] Crease | A toolkit of resource-sensitive, multimodal widgets[END_REF]. The adaptation capabilities are implemented at software level.

Beside software, some techniques promoting the implementation of interaction adaptation at runtime as a feature of the operating system, like in ToolGlasses [START_REF] Bier | Toolglass and magic lenses: the see-through interface[END_REF] or FACADE [START_REF] Stuerzlinger | User interface façades: towards fully adaptable user interfaces[END_REF] were suggested. The objective of these approaches is to support adaptation of the UI at runtime without any modiÞcation of its internal code. The key idea consists in embedding, inside software components, integrated to the software part of the user interface, the various characteristics of interaction modalities and devices present on different platforms. The operating system integrates these adaptive components. Here, adaptive user interfaces (the user is in charge of the adaptation by supplying these components) are promoted but not adaptable interfaces.

In 2003, the European project Cameleon [START_REF] Calvary | The cameleon reference framework. Deliverable D1 of the Cameleon project[END_REF] initiated by the Human Computer Interaction community proposed a consensual reference framework deÞning the development process of plastic user interfaces in order to cover all aspects of human computer interaction (both software and human aspects). This reference framework promotes handling of plasticity characteristics, at early stages of the user interface development process. The key idea consists in designing a user interface once and equipping it with several interaction modes and devices. Successive suitable transformations to Þt the characteristics (interaction techniques, modalities, environment, etc.) are applied on the designed user interface. These transformations lead to various target platforms. Several techniques and toolboxes result from this approach. The most signiÞcant ones are USIXML [START_REF] Limbourg | Usixml: a language supporting multi-path development of user interfaces[END_REF], COMET [START_REF] Demeure | Comet(s), a software architecture style and an interactors toolkit for plastic user interfaces[END_REF], WAHID [START_REF] Jabarin | Architectures for widget-level plasticity[END_REF] and MultiModel Widgets [START_REF] Stanciulescu | Methodology for Developing Multimodal User Interfaces of Information Systems[END_REF]. USIXML is an XML-based framework, where a user interface is spec-iÞed once and multiple implementations, for various target platforms, may be produced from this description. In the COMET environment [START_REF] Demeure | Comet(s), a software architecture style and an interactors toolkit for plastic user interfaces[END_REF], a UI is speciÞed at a logical level and multiple rendering technologies can be used to implement it, using a variety of widgets, thanks to a rich toolbox of UI component running in a wide range of platforms. Similar solutions are also provided by WAHID [START_REF] Jabarin | Architectures for widget-level plasticity[END_REF] and MultiModel Widgets [START_REF] Stanciulescu | Methodology for Developing Multimodal User Interfaces of Information Systems[END_REF].

The adaptation of presentation and rendering was also studied. The AMF [START_REF] Samaan | The AMF architecture in a multiple user interface generation process[END_REF] approach deÞnes a set of interaction patterns in a multi-agent setting. Each pattern is deÞned so that it adapts user interface input/output according to the described interaction mode. In a similar approach, the user interface Module Adaptation approach of [START_REF] Dery-Pinna A M, Fierstone | Component model and programming: a Þrst step to manage human computer interaction adaptation[END_REF] supports GUI adaptation to the context of use (platform, environment, user proÞle). The user rearranges the application's user interface. Hiding and/or showing presentation elements of the interface are performed according to a matching algorithm with user interaction preferences and requirements.

More recently, taking into account the context of use has been addressed, particularly the user proÞle and environment. In [START_REF] Oliveira | Transportation ontology deÞnition and application for the content personalization of user interfaces[END_REF], a UI is adapted according to user proÞles, stored in an ontology. User proÞles are also in the center of nomadic adaptable UI design [START_REF] Sonnenberg | Service and user interface transfer from nomadic devices to car infotainment systems[END_REF][START_REF] Dees | Usability of nomadic user interfaces[END_REF], exploited in MAGALLEN [START_REF] Masson | Examples galleries generated by interactive genetic algorithms[END_REF] to synthesize UI prototypes. In the ubiquitous widgets approach [START_REF] Pierre | Ubiquitous widgets: Designing interactions architecture for adaptive mobile applications[END_REF], user interactions are captured and transmitted by speciÞc components, called IBC (Interactor Business Component) used to implement adaptive UI widgets.

Most of the previously discussed approaches to handle plasticity focused on the software part of the user interface. They led to the deÞnition of techniques for the adaptation of software components of the interface. Few approaches addressed interaction handling adaptation of the dialogue between the user and the interface. This last aspect is handled by the third generation approaches. In these approaches, user proÞles and the environment of the user interface are taken into account for adaptation. Ontologies are used to store user proÞles in approaches like [START_REF] Oliveira | Transportation ontology deÞnition and application for the content personalization of user interfaces[END_REF][START_REF] Masson | Examples galleries generated by interactive genetic algorithms[END_REF].

Our approach

Our approach advocates the formalization of both user task models and interaction substitutions in order to handle formal veriÞcation of plasticity of user interfaces.

Plasticity and user task models

From the overview of the different approaches to handle plas-ticity in user interfaces of Section 3, it appears that • a lack of interest is paid to the design and validation of a dialogue between a user and an interface when achieving a given user task with several interaction devices and different platforms representing "the context of use" as deÞned by Coutaz [START_REF] Coutaz | HCI and software engineering for user interface plasticity[END_REF];

• no existing approach has addressed the problem of formally modeling the plasticity property in order to allow user interface designers to check this property at design time.

In this paper, we consider that,

• if the adaptation of the interaction is achieved through the adaptation of the task model, usually used to describe the interaction, then plasticity would be addressed at the interaction level rather than at the software part of a user interface;

• if the task models and substitutions of interactions occurring in task models are formalized, then it becomes possible to formally verify the plasticity of a given user interface.

Plasticity seen as an explicit knowledge domain

Several approaches to address the diversity and the heterogeneity of interaction devices and modes have been proposed. These approaches rely on the deÞnition of a set of potential interaction devices and modes that can be used as substitutes for other ones in a given situation or context. Most of the sig-niÞcant approaches are based on 1) modeling interaction styles using pattern descriptions similarly to the agent multi-facets approach (AMF) [START_REF] Samaan | Prise en Compte du Modèle d'Interaction dans le Processus de Construction et d'Adaptation d'Applications Interactives[END_REF]. AMF proposes to specify different interaction techniques in a set of patterns to be used in adaptation strategies;

2) the deÞnition and the use of a catalogue of human computer interaction development technologies following [START_REF] Demeure | Modèles et outils pour la conception et l'exécution d'Interfaces Homme-Machine Plastiques[END_REF]. COMET [START_REF] Demeure | Comet(s), a software architecture style and an interactors toolkit for plastic user interfaces[END_REF] suggests to build a catalogue of user interface development technologies consulted by COMET at runtime to deÞne which adaptation style applies;

3) producing target user interfaces by transformation of a source one. For example, genetic algorithms based approaches were applied in MAGALLEN [START_REF] Masson | Examples galleries generated by interactive genetic algorithms[END_REF] to produce user interfaces prototypes by a mutation mecha-nism tuned by a given user proÞle. These approaches choose the suited interaction technique, mode or device among a set of different candidate ones.

Therefore, whatever is the chosen adaptation strategy (at design time or at runtime) or the adaptation mode (by a user [START_REF] Samaan | Prise en Compte du Modèle d'Interaction dans le Processus de Construction et d'Adaptation d'Applications Interactives[END_REF][START_REF] Navarre | ICOs: a model-based user interface description technique dedicated to interactive systems addressing usability, reliability and scalability[END_REF] or automatically [START_REF] Demeure | Comet(s), a software architecture style and an interactors toolkit for plastic user interfaces[END_REF][START_REF] Masson | Examples galleries generated by interactive genetic algorithms[END_REF]), it is necessary to deÞne and model the description of the different concepts needed to achieve this adaptation (user interface development models, interaction modes, interaction devices, mappings and correspondences between different interaction devices and/or modes, etc.).

We claim that domain ontologies [START_REF] Gruber | A translation approach to portable ontology speciÞcations[END_REF][START_REF] Jean | Domain ontologies: a database-oriented analysis[END_REF] are good candidates for modeling such concepts and mappings between these concepts. According to [START_REF] Gruber | A translation approach to portable ontology speciÞcations[END_REF], domain ontologies are knowledge models that provide with an explicit speciÞcation of the concepts of a domain. They can be viewed as a dictionary of concepts and of properties that hold among these concepts [START_REF] Jean | Domain ontologies: a database-oriented analysis[END_REF]. The interest of ontololgies is to provide explicit semantic deÞnitions of concepts independently of any context of use.

A Þrst attempt to use ontological approach in plastic user interface design was carried out by [START_REF] Limbourg | Usixml: a language supporting multi-path development of user interfaces[END_REF]. It consists of integrating ontology reasoning in USIXML to be able to describe multi-path development approaches. The ontology provides deÞnitions of concepts manipulated by different models of a user interface design according to the Cameleon framework [START_REF] Calvary | The cameleon reference framework. Deliverable D1 of the Cameleon project[END_REF]. This approach exploits terminological aspects available in the ontology. A more recent approach uses domain ontologies to adapt information system user interfaces to a user proÞle in the transportation domain [START_REF] Oliveira | Transportation ontology deÞnition and application for the content personalization of user interfaces[END_REF].

Two key requirements

Two characteristics of a user interface must be taken into account to ensure the plasticity of user interfaces. One relates to the implementation of the presentation software components and the other to the interaction techniques offered by the devices. These characteristics are handled in the bottom part of a user tasks model associated to a given user interface.

• Req 1 -Adaptation of the implementation techniques At presentation level, adaptation requires that the implementation of the presentation components is supported by the used implementation technologies available in the target environment and/or platform to best adapt the user interface [START_REF] Coutaz | HCI and software engineering for user interface plasticity[END_REF].

Indeed, implementation techniques differ from one platform to another according to the underlying oper-ating system, graphic display technology, interaction modes, etc. Two adaptation techniques are identiÞed. The presentation side of the UI can be adapted either -by remodeling or redesigning the interface, for example, in the case of a substitution of a set of radio buttons by a menu [START_REF] Demeure | Le modèle d'évolution en plasticité des interfaces: apport des graphes conceptuels[END_REF];

-or by the transfer (move) to a target platform of a part of the interface (redistribution), for example in the painter application of [START_REF] Rekimoto | Pick-and-drop: a direct manipulation technique for multiple computer environments[END_REF] where the color palette is implemented in a personal digital assistant (PDA) while a drawing board is implemented on a personal computer (PC) platform.

The Þrst adaptation technique requires to replace presentation widgets according to alternatives allowed by the underlying operating system of the target platform.

The second adaptation technique requires 1) to chose which part of the interface can be distributed according to interaction techniques allowed by the target operating systems (is it possible to run this part of the UI ?),

2) the environment of execution (does the environment of the target platform allow the execution? are light, sound, etc. available ?) and

3) the opportunity to migrate a part of the whole application (for example in the painter application, the color palette is the part of the UI which can be separated from the drawing board as it is the case in the real world).

• Req 2 -Adaptation of the interactions offered by the devices At interaction level, adaptation requires the knowledge of how a given interaction device can be replaced by another one in order to allow users to pursue interacting with the system. This interaction shall continue even if failures occur [START_REF] Navarre | A formal approach for user interaction reconÞguration of safety critical interactive systems[END_REF].

The physical actions offered by an interaction device may differ from one interaction device to another, but they may often produce the same effect on the user interface components. In fact, the effect produced by a physical action corresponds to an abstract interaction that may be realized by different interactions offered by the physical device. For instance, a click on the left mouse button produces the same effect as a press on the keyboard ENTER key. From the abstract task point of view, it corresponds to the GO action as deÞned in a canonical abstract interaction [START_REF] Constantine | Canonical abstract prototypes for abstract visual and interaction design[END_REF].

The replacement of an interaction of a source device by the ones of another target device requires the substitution of the physical actions performed within the source device by those of the target device which produce the same effects on the user interface. As a consequence, to handle plasticity, matching mechanisms between an action and the effect it produces on the user interface are needed.

Our approach

As stated in Section 2, most of the work in the Þeld of UI plasticity focussed on the Þrst requirement (Req 1 ) related to the implementation techniques adaptation which gained a relative maturity.

We focus on the second requirement (Req 2 ) related to the adaptation of the interaction where we consider that a lack of interest still exists.

Moreover, the design life cycle of a multi-platform interface entails building a task model for each platform. The abstract part (top level) of this task model remains identical for each platform while the concrete part (bottom level) is adapted to each speciÞc platform according to its interaction modes and/or devices. The main drawback of this approach is the need to perform task model veriÞcation and validation for each platform. In other words, check if the different task models still describe the same task. Adaptation of task model, due to the variations on the platform and/or on the hardware side of the UI (lose and/or gain of interaction devices in the platform), is identiÞed as a "main axis" of the "design space for UI adaptation" in [START_REF] Thevenin | Plasticity of user interfaces: framework and research agenda[END_REF].

In the context of user interface plasticity, our approach aims to address the problem of adaptation of the interaction to different platforms. When several strategies of interaction techniques are often allowed to implement a given task (top level of a task model) on several platforms, we propose to use formal techniques to check if these strategies are equivalent. We compare task models corresponding to each strategy, leading to compare user behavior in each strategy.

To achieve this goal, we represent each task model by an automaton, i.e., a labelled state transition system, and check equivalence (more precisely, behavioral equivalence) of task models by bi-simulation relationship. Since the interaction devices used in these different adaptation strategies are often different, the obtained labelled transition-systems have different sets of labels (interaction events). This leads to compare different behaviors expressed by labelled state transition systems with different sets of labels. However, the classical deÞnition of the bi-simulation relationship of Milner in [START_REF] Milner | Communication and Concurrency[END_REF] does not handle different sets of labels. Thus, it cannot be used directly to compare different labelled state transition systems issued from two different task models associated to different platforms. Therefore, to compare different user task models associated to different user interfaces platforms, the labelled state transition systems need to be reworked before the classical bi-simulation relationship is applied.

In our approach [START_REF] Chebieb | Formal veriÞcation of plastic user interfaces exploiting domain ontologies[END_REF], we advocate the deÞnition of an ontology model including descriptions of user tasks, interaction modes and interaction devices. The subsumption and equivalence relationships are used to deÞne substitutable tasks, interaction modes and devices.

This approach [START_REF] Chebieb | Formal veriÞcation of plastic user interfaces exploiting domain ontologies[END_REF] relies on equivalence checking. It consists of two main steps:

• First, unifying task models using a domain knowledge model expressing semantic equivalences between interaction devices and/or interaction modes;

• Second, equivalence checking of uniÞed task models by checking observational equivalence by means of weak bi-simulation relationship.

By reworking task models, we mean the identiÞcation of equivalent interactions (those offered by the physical devices and/or their composition). Because of the continuous evolution and the emergence of new interaction devices and the associated interaction techniques, we advocate the use of domain ontologies to formalize equivalence matchings between device interactions and/or their compositions. These matchings are expressed by explicit links between physical actions allowed by an interaction device and all the possible effects they may produce. Moreover, we also require to categorize these effects at the abstract level of interaction in order to characterize each physical interaction by an abstract one. The availability of this tacit knowledge for software adapters may enhance automatic UI adaptation and even self-adaptation at runtime.

Comparing labelled transition systems

The proposed approach relies on the capability to compare labelled transition systems in order to establish behavioral equivalence of such systems. Different relationships have been introduced in the literature to deÞne various kinds of lts comparison from a behavioral point of view. Indeed, simulation is used to link a lts that includes the behavior of another lts. Symmetrically, bi-simulation deÞnes a binary equivalence relation on lts states. This equivalence may be an exact equiv-alence through strong bi-simulation and observational or behavioral with weak bi-simulation. In general, weak relationships are used to identify labelled transition systems that share a same behavior.

In this section, we recall the basic deÞnitions related to labelled transition systems and their comparison. These deÞnitions were set up by the fundamental and seminal work of Milner [START_REF] Milner | A Calculus of Communicating Systems[END_REF][START_REF] Milner | Communication and Concurrency[END_REF] for observational equivalence.

Basic deÞnitions

DeÞnition 1 A labeled transition system L is a structure L = S , s 0 , E, -→ where S is a set of states, s 0 ∈ S denotes an initial state, E is a set of labels and -→ ⊆ S × E × S is a transition relation between states.

Notations When specifying systems by labelled transition systems, labels denote actions and the speciÞc label τ ∈ E is used to denote internal actions, i.e., non observable actions. We note E * to represent the set of all possible sequences of labels of E and LT S as the set of all labelled transition systems.

* -→ s ′ e -→ t ′ τ * -→ t.

Relations on states

Let T = S , s 0 , E, -→ be a lts.

DeÞnition 3 (Simulation relationship on states) Let ≺ ⊆ S × S be a binary relationship on states. ≺ is a Simulation when for any states p, p ′ , q ∈ S and for any a ∈ E, if (p, q) ∈ ≺ and p a -→ p ′ , then there exists q ′ ∈ S such that q a -→ q ′ and (p ′ , q ′ ) ∈ ≺.

We say that state q simulates p according to ≺. Note that simulation is not a symmetric relationship. DeÞnition 4 (Weak simulation relationship on states) Let ∼ ⊆ S × S be a binary relationship on states. ∼ is a weak simulation when for any states p, p ′ , q ∈ S and for any a ∈ E, if (p, q) ∈ ∼ and p a =⇒ p ′ , then there exists q ′ ∈ S such that q a =⇒ q ′ and (p ′ , q ′ ) ∈ ∼.

We say that state q simulates p according to ∼. Note that weak simulation is not a symmetric relationship.

DeÞnition 5 (Strong bi-simulation relationship on states)

A bi-simulation is a symmetric relation of simulation. Let ⊆ S × S be a binary relationship on states and p, q ∈ S such that (p, q) ∈ .

is a strong bi-simulation relationship if

• p a -→ p ′ implies that there exists q ′ ∈ S such that q a -→ q ′ and (p ′ , q ′ ) ∈ ;

• q a -→ q ′ implies that there exists p ′ ∈ S such that p a -→ p ′ and (p ′ , q ′ ) ∈ . DeÞnition 6 (Weak bi-simulation relationship on states) Let ≈ ⊆ S ×S be a binary relationship on states and p, q ∈ S such that (p, q) ∈ ≈.

≈ is a weak bi-simulation relationship if

• p a -→ p ′ implies that there exists q ′ ∈ S such that q a =⇒ q ′ and (p ′ , q ′ ) ∈ ≈;

• q a -→ q ′ implies that there exists p ′ ∈ S such that p a =⇒ p ′ and (p ′ , q ′ ) ∈ ≈.

Extensions to labelled transition systems

The previous deÞnitions are extended to labelled transition systems. Let lts = S , s 0 E, -→ and lts ′ = S ′ , s ′ 0 E, -→ be two labelled transition systems with the same set of labels E and S ∩ S ′ = ∅.

Informally, this extension of these relations to labelled transition systems consists in requiring the existence of a corresponding relation on the initial states of these labelled transition systems.

DeÞnition 7 (Simulation relationship on lts) Let ≺ ⊆ S × S ′ be a simulation relationship. We deÞne ≺ lts ⊆ LT S × LT S as a simulation relationship between two labelled transition systems.

Then (lts, lts ′ ) ∈ ≺ lts if (s 0 , s ′ 0 ) ∈ ≺. Informally, the relation ≺ lts on lts is a simulation relationship if it is possible to build a state simulation relation (≺) that includes their initial states.

We say that lts ′ simulates lts. DeÞnition 8 (Weak simulation relationship on lts) Let ∼ ⊆ S × S ′ be a weak simulation relationship. We deÞne ∼ lts ⊆ LT S × LT S as a weak simulation relationship between two labelled transition systems.

Then (lts, lts ′ ) ∈ ∼ lts if (s 0 , s ′ 0 ) ∈ ∼. Informally, the relation ∼ lts on lts is a weak simulation relationship if it is possible to build a state weak simulation relation (∼) that includes their initial states.

We say that lts ′ weakly simulates lts.

DeÞnition 9 (Strong bi-simulation relationship on lts) Let ⊆ S × S ′ be a strong bi-simulation relationship. We deÞne lts ⊆ LT S × LT S as a strong bi-simulation relationship between two labelled transition systems.

Then (lts, lts ′ ) ∈ lts if (s 0 , s ′ 0 ) ∈ . Informally, the relation lts on lts is a strong bi-simulation relationship if it is possible to build a state strong bisimulation relation ( ) that includes their initial states.

We say that lts ′ and lts are bi-similar.

DeÞnition 10 (Weak bi-simulation relationship on lts) Let ≈ ⊆ S × S ′ be a weak bi-simulation relationship.

We deÞne ≈ lts ⊆ LT S × LT S as a weak bi-simulation relationship between two labelled transition systems.

Then (lts, lts ′ ) ∈ ≈ lts if (s 0 , s ′ 0 ) ∈ ≈. Informally, the relation ≈ lts on lts is a weak bi-simulation relationship if it is possible to build a state weak bi-simulation relation (≈) that includes their initial states.

We say that lts ′ and lts are weakly bi-similar.

Revisiting lts comparison

The previously deÞned relationships support the comparison of labelled transition systems that act on the same set of labels. The situation where the need of comparing labelled transition systems with different sets of labels may occur. For example, interactive systems, addressed in this paper, are one of the cases where different interaction possibilities are offered to interact with a given system.

In this section, we deÞne another bi-simulation relationship that relaxes the classical deÞnition. It relates labelled transition systems with different sets of labels.

The proposed deÞnition relies on the introduction of a relation on labels. This relation links pairs of labels. It is exploited to transform the labelled transitions systems to be compared labelled transition systems by substituting labels so as they get the same set of labels.

Rewriting labels and transforming labelled transition systems

Let lts = S , s 0 E, -→ and lts ′ = S ′ , s ′ 0 E, -→ be two transition systems such that S ∩ S ′ = ∅, E E ′ and E ′ E.

Let A be another set of labels different from the ones of

E ∪ E ′ , in other words, A ∩ (E ∪ E ′ ) = ∅ DeÞnition 11 (Bi-directional relation on labels) Γ ⊆ (E -E ′ ) × (E ′ -E) is a relation on labels of two labelled transition systems. It satisÞes ∀ α ∈ E -E ′ , ∃ β ∈ E ′ -E we have (α, β) ∈ Γ; ∀ β ∈ E ′ -E, ∃ α ∈ E -E ′ we have (α, β) ∈ Γ.
Left and right projection functions Pro j l and Pro j r are associated to Γ. Informally, the relation Γ on labels deÞnes a total relation on the labels that do not belong to E ∩ E ′ , i.e., the labels that are not shared by the two labelled transition systems.

DeÞnition 12 (Rewriting function on labels) The function

Φ : E × E ′ -→ (A ∪ E ∪ E ′ ∪ {τ}) on labels of two labelled transition systems is deÞned by ∀ (α, β) ∈ Γ ∃ γ ∈ A ∪ E ∪ E ′ ∪ {τ} such that Φ(α, β) = γ.
Four main rules can be associated to the deÞnition of the rewriting function. -transition relations are redeÞned with the new labels

′ = S ′ , s ′ 0 E, -→ are respectively rewritten to lts ⊤ = S ⊤ , s ⊤ 0 E ⊤ , -→ ⊤ and lts ⊤ ′ = S ⊤ ′ , s ⊤ ′ 0 E ⊤ ′ , -→ ⊤ ′ accord
-→ ⊤ ⊆ S ⊤ × E ⊤ × S ⊤ and -→ ⊤ ′ ⊆ S ⊤ ′ × E ⊤ ′ × S ⊤ ′
, where

-→ ⊤ = {s e -→ t ∈-→| ∀e ′ ∈ E ′ . (e, e ′ ) Γ} -{s e -→ t ∈-→| ∀e ′ ∈ E ′ . (e, e ′ ) ∈ Γ} ∪ {s a -→ t | ∃(e, e ′ ) ∈ Γ ∧ Φ(e, e ′ ) = a}, -→ ⊤ ′ = {s ′ e ′ -→ t ′ ∈-→ ′ | ∀e ∈ E. (e, e ′ ) Γ} -{s ′ e ′ -→ ′ t ′ ∈-→ ′ | ∀e ∈ E. (e, e ′ ) ∈ Γ} ∪ {s ′ a -→ ′ t | ∃(e, e ′ ) ∈ Γ ∧ Φ(e, e ′ ) = a}.
lts ⊤ and lts ⊤ ′ are labelled transition systems with the same set of labels, since E ⊤ = E ⊤ ′ .

Comparison of labelled transition systems with different sets of labels

Let lts, lts ′ , Γ, Φ be a structure where lts and lts ′ are two labelled transition systems such that

S ∩ S ′ = ∅, E E ′ and E ′ E, -Γ ⊆ E × E ′ is a relationship on labels according to Def- inition 11,
-Φ is a label rewriting function according to DeÞnition 12.

DeÞnition 14 (Relational simulation relationship on lts) ≺ Γ,Φ lts ⊆ LT S × LT S is a relational simulation relationship on labelled transition systems if there exists a simulation relationship on labelled transition systems between the transformed lts. We write (lts, lts ′ ) ∈≺ Γ,Φ lts ⇐⇒ (lts ⊤ , lts ⊤ ′ ) ∈≺ lts .

DeÞnition 15 (Relational weak simulation relationship on lts) ∼ Γ,Φ lts ⊆ LT S × LT S is a relational weak simulation relationship on labelled transition systems if there exists a simulation relationship on labelled transition systems between the transformed lts. We write (lts, lts ′ ) ∈∼ Γ,Φ lts ⇐⇒ (lts ⊤ , lts ⊤ ′ ) ∈∼ lts .

DeÞnition 16 (Relational strong bi-simulation relationship on lts) Γ,Φ lts ⊆ LT S ×LT S is a relational strong bi-simulation relationship on labelled transition systems if there exists a strong bi-simulation relationship on labelled transition systems between the transformed lts. We write (lts, lts ′ ) ∈ Γ,Φ lts ⇐⇒ (lts ⊤ , lts ⊤ ′ ) ∈ lts .

DeÞnition 17 (Relational weak bi-simulation relationship on lts) ≈ Γ,Φ lts ⊆ LT S × LT S is a relational weak bi-simulation relationship on labelled transition systems if there exists a weak bi-simulation relationship on labelled transition systems between the transformed lts. We write (lts, lts ′ ) ∈≈ Γ,Φ lts ⇐⇒ (lts ⊤ , lts ⊤ ′ ) ∈≈ lts .

From the deÞnitions of the relationships introduced in the previous deÞnitions, it becomes possible to compare labelled transition systems with different sets of labels.

About Γ and Φ

The deÞnition of Γ and Φ are of great importance to de-Þne label mappings and label rewritings. The formal setting described above requires the existence of a 1) relation Γ between the labels associated to one labelled transition system which do not occur in the other one;

2) transformation function Φ which associates to each pair of labels in Γ another label different from those of the two considered labelled transition systems.

The deÞnitions of Γ and Φ given above are minimal deÞnitions. Strengthening these deÞnitions with additional constraints and properties remains possible. This strengthening shall preserve the capability to rewrite the labels. In this case, new properties on the labels of labelled transition systems and thus of the labelled transition systems themselves can be deduced.

A formal model for designing plastic interfaces

The classical simulation and bi-simulation relationships are deÞned on a single set of labels. Their deÞnitions compare transitions with the same labels. The need of comparing systems with close or equivalent behaviors that do not use the same transition labels may occur in several situations particularly in the case of system substitution and thus in the case of plastic user interface. Systems for which relational simulation or relational bisimulation relationships are useful are those systems whose behavior may lead to equivalent states but which use different actions. Plastic interactive systems described in Section 3 correspond to such systems. These systems use different interaction modes and devices to achieve the same user tasks. As stated in Section 2, by plasticity we mean the capability to achieve a given interactive task using different interactive modes and/or devices. In other words, two interactive systems may realise the same action using different interaction modes or devices. Relational bi-similarity can be used to check that these two systems are equivalent modulo the relations on the labels.

In the remainder of this section, we put into practice the relational bi-simulation and show how it is set up to check the plasticity property of interactive systems. An ontology is de-Þned in order to semantically model relations on labels. We also give a stepwise methodology to support this checking process.

Task models as labelled transition systems

A task model allows a designer to describe tasks to be supported by the designed user interface. A task model gives the details of both a static aspect which corresponds to the structure of the task (a decomposition tree in our case) and a dynamic aspect which corresponds to behavior of the user and the system (labelled transition systems in our case) during the achievement of the task.

Various experiences reported in the literature have represented task models by labelled transition systems. For instance, in [START_REF] Paternò | Integrating model checking and HCI tools to help designers verify user interface properties[END_REF] lts have been derived from a task model to simulate user behavior in order to verify task achievement. In [START_REF] Ameur | Validation et vériÞcation formelles de systèmes interactifs multi-modaux fondées sur la preuve[END_REF], lts built from a task model are used to formally verify properties of multi-modal user interfaces. In both experiences, the set of states is built from attributes available in the user interface components and the set of transitions is built from user actions.

A task model expresses a hierarchical decomposition of the task into subtasks up to physical actions (keystroke). At the same time, it speciÞes a temporal interleaving of these subtasks and actions (consecutive, parallel, alternative, iterative composition operations). In other terms, it describes the behavior of the user interacting with the interface entailing a modiÞcation in its state. This behavior is captured by a formal model described as a labelled state-transition system made of user actions composing the task and of the interface reaction. User actions are modeled by transitions and the interface reactions are denoted by the states of the system.

Task models written in CTT task modeling notation of Section 3 are particularly suitable to be represented by a labelled transition system. A lts describes the behavior of the interaction between the user and the system, when achieving a task. Physical actions (leaves) of the task model become transition labels and temporal operators are compositions of transitions.

Figure 2 shows a lts derived from the task model example depicted in Fig. 1 of Section 2. Its set of labels {T 3 , T 4 , T 5 , T 6 , T 7 , T 8 } is built from the user actions of the task model (the user actions are in the leaves of the task tree of the Fig. 1) and the set of states {S 0 , S 1 , . . . , S 8 } is composed of some relevant user interface components attributes impacted by these actions.

Fig. 2 The lts representing task model

An ontology of interaction

The labels of a transition system derived from an interactive task model (e.g., a CTT task model) represent actions performed on the interactive system either by the human (user) or by the machine. The semantics of these actions can be de-Þned within and ontology which also gives a label classiÞcation.

We deÞne an ontology providing hierarchical categories of interactive actions or devices. As shown on the UML class diagram model depicted on Fig. 3, the basic concepts of our ontology are the interaction device, the interactive task and the user interaction respectively denoted by DEV, INTTASK, INTR in Fig. 3.

Basic concepts

1. The interaction device (DEV) concept deÞnes a hierarchical category of devices, well known in the human computer interaction domain, which may be used to perform tasks. This category is inspired from the taxonomy of interaction devices deÞned by Buxton [START_REF] Buxton | A three-state model of graphical input[END_REF], Card et al. [START_REF] Card | The design space of input devices[END_REF] and Frohlich [START_REF] Frohlich | The design space of interfaces[END_REF].

2. The interactive task (INTTASK) concept refers to the user interaction at abstract level in the same manner as "abstract interaction" deÞned in [START_REF] Constantine | Canonical abstract prototypes for abstract visual and interaction design[END_REF] (select, copy, text input, etc.).

The user interaction (INTR) concept describes patterns

of interaction techniques as well as those deÞned in [START_REF] Navarre | A formal approach for user interaction reconÞguration of safety critical interactive systems[END_REF] for user interaction reconÞguration. They are similar to those used to deÞne interaction strategies for AMF agents [START_REF] Samaan | Prise en Compte du Modèle d'Interaction dans le Processus de Construction et d'Adaptation d'Applications Interactives[END_REF] and to those deÞned for input adaptability in the ICON toolkit [START_REF] Dragicevic | Support for input adaptability in the icon toolkit[END_REF]. A user interaction can be basic • A basic interaction (ATOMIC-UA) deÞnes an atomic physical user action (keystroke). It is linked to an element (ELMT) of the interaction device concept on which it has effects. A user action may affect the behavior of the user interface. For example, a click (atomic user action) on a left button (element) of the mouse (interaction device) triggers the GO behavior of the user interface.

• A composite interaction (COMPOSITE) describes the case of an interaction composed of a set of user actions using the composition operators of sequence (SEQ), concurrence (PARA), choice (CHOI) and iteration (ITER). Each interaction materializes a way to perform an interactive task with a set of user actions offered by the interaction devices available on a user interface platform.

Basic relations

Our ontology acts like a dictionary of interaction techniques that formalize a set of patterns deÞning different implementations of a single interactive task, depending on various interaction devices existing in the human computer interaction domain. It offers different kinds of relations between user actions. As usual for ontologies, two main relationships between concepts are introduced: equivalence and subsumption.

1) Equivalence This relation means that two user actions linked to an element of an interactive device (or two sets of user actions based on two user interactions) have the same effects on an interactive system. In other words, the equivalence relationship expresses that an interactive task can be performed by one of the two single user actions or one of two user interactions.

2) Subsumption This relationship deÞnes a hierarchical relationship encoded by inheritance. When a user action subsumes a set of other user actions Us, then the effect of this user action entails the ones belonging to this set of actions Us. Subsumption relation expresses the fact that an interactive task can be performed either by a single user action or by a set of user actions composing a user interaction.

Rewriting rules for labels

When rewriting labels of lts derived from user actions, the relation linking an interactive task and the user interaction is exploited as follows.

• Rule 1 If two single user actions are equivalent, they may be rewritten with the label corresponding to the interactive task they perform.

Example 1 Press

Enter key and click left button are equivalent since both of them correspond to a GO behavior on the UI. They may be rewritten as the GO label corresponding to the interactive task they perform.

• Rule 2 If a single user action u subsumes a set of user actions Us composing a user interaction, then this single user action may be rewritten with as the label corre-sponding to the interactive task it performs. Moreover, all the user actions of the set of user interaction Us is rewritten with a single label corresponding to the same label as the one of interactive task.

Example 2

The user action point tablet screen entails the GO behavior equivalent to the ones entailed by the sequence of user actions move mouse SEQ click. We say that the former subsumes the later and both single action point tablet screen and the interaction may be rewritten as the single label GO.

• Rule 3 If a pair of two sets of user actions (two user interactions) are equivalent they may be rewritten in the same manner as a single label corresponding to the interactive task they perform.

Example 3

The composite user interaction press mouse button down in parallel with move mouse followed by release mouse button up deÞnes the selection of a set of icons on a screen. The same behavior can be obtained by the composite user interaction performed by the user action press of the shift key down in parallel with the press of direction key followed by the release of the shift key up. This means that the two composite user interactions are equivalent. Therefore, both of them may be rewritten to the single label Multi-Selection corresponding to the interactive task they perform.

Methodology

The whole material required to check the plasticity of a user interface is now set up. Checking the plasticity property consists in checking that two different interactive systems allows a user to achieve the same tasks using different interactive modes and/or different devices.

• Basic principle The proposed approach consists in formalizing the considered interactive systems by labelled transition systems, and then checking a relational bi-simulation on these two systems, provided that a relation on labels of their corresponding labelled transition systems is available.

To check the plasticity property of a pair (Syst source , Syst target ), we have set a stepwise methodology consisting in the following steps:

1) Design Design the pair (lts source , lts target ) of labelled transition systems formalising (Syst source , Syst target ).

2) Irrelevant action identiÞcation For (lts source , lts target ), identify the possible internal actions that are not relevant for the interaction. The labels corresponding to these actions in (lts source and/or lts target ) are set to τ.

3) Rewriting Using a relation on labels of the lts, the labels of lts source and lts target that are different are rewritten. At this stage, the two lts source and lts target have the same labels.

4) Checking Check weak bi-simulation between the obtained lts.

In other words, two interactive systems satisfy the plasticity properties if they are linked by a relational bi-simulation relationship according to a given relation on labels.

Validation on the case study

This section shows how our approach to check user interface plasticity applies on two case studies. The Þrst one addresses the case of a web interface to send an SMS (short message sending) and the second one deals with a mobile casual game application. In both cases, the four-step methodology we de-Þned in the previous section (design, irrelevant action identi-Þcation, rewriting, checking) is deployed.

Desktop web application UI adapted to smart phone

Our case study concerns an interface of a web application for sending an SMS (short message sending). The user interface is composed of a set of six (06) web forms to be Þlled in order to send an SMS. First, the user opens a session to login to his own space (Þrst web form), then he composes his message (second and third web forms) and sends the composed SMS (forth and Þfth web forms). Finally he exits his own space (sixth web form). The CTT task model depicted in Fig. 4 describes the different user actions involved by the task consisting in sending an SMS. The following subtasks are introduced. 1) Login (subtask TA) where a user introduces his/her login identiÞer (T 1 ) and his/her password (T 2 ) in any order and submit these two entered values (T 3 ).

2) Compose is devoted to build the SMS (subtask TB). The user launches a message editor (T 4 ), edits his/her message (T 5 ) by typing the text of the message (T 8 ), enters the phone number of the recipient (T 7 ) (in any order) and then decides whether he/she sends the written message (T 9 ), saves it (T 10 ) or cancels it (T 11 ).

3) Send task is deÞned to model sending of the composed message. The user requests a send action to the system (T 12 ) and conÞrms the transaction (T 13 ) or not (T 14 ). In case the sending of the message is not conÞrmed, the user chooses either to save the message (T 15 ) or to can- In the rest of this section, we focus on the subtask EditMsg task corresponding to T 5 in Fig. 4. Our objective is to compare the interaction technique used to perform this task on a personal computer (a platform with a mouse and a keyboard only) on the one hand and two interaction techniques used to carry out the same task on a smart phone (a platform with a keyboard only) and on a Touch-Pad (a platform with touch screen only) on the other hand. The four-step methodology we have deÞned is set up.

Design

Let lts source , lts targetPh and lts targetT p be the labelled state transition systems modeling the subtask EditMsg on the syst source , syst targetPh and syst targetT p systems corresponding to a personal computer, a smartphone and a Touch-Pad, respectively.

The CTT task model associated to the EditMsg on the personal computer syst source is depicted in Fig. 5. This task model is compared to the two identiÞed target task models.

The Þrst task model corresponds to the interaction task performed on a smart phone syst targetPh . The subtask EditMsg for a smartphone is described by the CTT task model of Fig. 6.

Fig. 5 The EditMsg task model of the interaction on the PC platform Fig. 6 The EditMsg task model of the interaction on a smart phone platform Last, the second target task model represents the interaction performed on a Touch Pad. Figure 7 depicts the corresponding CTT task model. In order to build the different labelled state transition systems corresponding to each platform, we associate a label for each user action available in each of the CTT task models.

Table 1 describes all the correspondences between user actions of the CTT task models and the labels in the corresponding lts. The following labelled state transition systems are obtained for the EditMsg user task.

1) The lts lts source representing the interaction on the personal computer platform is given by the labelled statetransition system of Fig. 8.

Fig. 8 The EditMsg lts for a PC platform

2) The task model corresponding to the interaction on a smartphone platform is represented by the labelled state transition system lts targetPh of Fig. 9.

Fig. 9 The EditMsg lts for a smartphone platform

3) Finally, the labelled state transition system lts targetT p representing the interaction on the Touch Pad platform is represented in Fig. 10.

Fig. 10 The EditMsg lts for a Touch Pad platform At this stage we obtain two pairs (lts source , lts targetPh ) to compare the interaction used on a personal computer with the one on a smartphone and (lts source , lts targetT p ) to compare personal computer interaction with the interaction on a Touch Pad.

In the remaining steps, we will address the case of (lts source , lts targetPh ) only to compare the interaction used on a personal computer with the one on a smartphone.

Irrelevant actions identiÞcation

The next step identiÞes the possible internal actions considered as non relevant to perform the suited interaction. The labels corresponding to these actions in both lts source or lts targetPh are set to τ.

The set of actions {MoveMouse, BTNPress DUDirBtn, BT-NPress LRDirBtn} iterated on the deÞned labelled state transition system is not relevant for the interaction. Indeed, the presence of these iterated actions in the CTT task model expresses a cursor movement to reach a target Þeld in a given form. Moving a cursor can be done repeatedly without any relevant effect from interaction point of view. So, only one move of the cursor is considered and the occurrences of labels of the set {e 7 , e 6 , e 8 } are set to τ. Another pair of labelled state transition systems (lts Pct , lts Pht ) is obtained after irrele-vant actions removal.

The labelled state transition system lts Pct depicted in Fig. 11 corresponds to the lts source (Fig. 8) where the iterated occurrences of the label e 7 (transitions on states 2, 5, 8 and 11) are set to τ. The labelled state transition system lts Pht of Fig. 12 corresponds to the labelled state transition system lts targetPh (Fig. 9) where the iterated occurrences of labels e 6 and e 8 are set to τ. The set of labels of the labelled state transition systems lts Pct and lts Pht obtained after removing irrelevant actions are still different sets. A rewriting step, exploiting relations on labels borrowed the ontology is required to obtain two labelled state transition systems with a single set of labels.

Let E and E ′ be the two sets of labels of lts Pct and lts Pht respectively.

Let LabDi f f be the set of different labels of lts Pct and lts Pht . It is deÞned by Let E p the set of labels of lts Pct to be rewritten.

LabDi f f = (E ∪ E ′ ) -(E ∩ E ′ ) = {e
E p = E ∩ LabDi f f = {e 5 , e 7 }.
Let E ′ h be the set of labels of lts Pht to be rewritten.

E ′ h = E ′ ∩ LabDi f f = {e 6 , e 8 , e 10 }.
The relation Γ (see DeÞnition 11) provided by our ontology is the equivalence and/or subsumption relationships. These relations mean that user actions and/or user interactions with the same effect (equivalent or subsumed effect) can be replaced by the interactive task corresponding to this effect. The result of this substitution operation is a set A = {g, m} containing two labels neither in E nor in E ′ . These two labels must be rewritten according to the identiÞed ontological relation in order to get a same set of labels. Figure 13 shows instances of the ontology we have used to deÞne such relations. When applied, the rewriting function φ (DeÞnition 12) produces the labels deÞned in Table 2. In Table 2,

• the label g corresponding to the interactive task "GO" is a substitute for the ones corresponding to the user actions Click LBTN and BtnPress CentBtn. Indeed, this label represents the effect of the two actions,

• the label m corresponding to the interactive task "Move-Cursor" is a substitute for the labels corresponding to the user actions Move Mouse, BtnPress DUDirBtn and BtnPress LRDirBtn.

After rewriting the labels of lts Pct and lts Pht , the new labelled state transition systems lts Pctr are obtained. They are respectively depicted in Figs. 14 and15.

This rewriting step produces two lts with the same set of labels {e 1 , e 3 , m, g, τ}.

Checking

The Þnal step checks behavior equivalence on the obtained labelled state transition systems. Observational equivalence between the two obtained labelled state transition systems is checked. This checking supports the behavior comparison of interactive systems that do not have the same interaction modes and/or devices. To do so we use the weak bisimulation relationship deÞned in Section 5. The Þnal result showed that lts Pct and lts Pht are weakly bi-similar. Thus we can formally assert that the interactions described by the task models of Figs. 5 and 6 perform the same task, and thus the devices and the interactions may be substituted. The equiva-Fig. [START_REF] Paternò | Integrating model checking and HCI tools to help designers verify user interface properties[END_REF] Instances of our ontology concepts used to rewrite labels Fig. [START_REF] Scapin | Towards a method for task description: MAD[END_REF] The EditMsg lts for a PC platform after rewriting labels Fig. [START_REF] Scapin | Analyse des tâches et aide ergonomique à la conception: l'approche mad*[END_REF] The EditMsg lts for a smartphone platform after rewriting labels lence of the corresponding rewritten labelled state transition systems modulo the relational weak bi-simulation relationship means that these two interaction techniques can substitute each other.

The previous case study has been checked within the CADP (construction and analysis of distributed processes) model checker [START_REF]CADP-Team[END_REF]. It offers a set of tools for compiling, verifying and validating Lotos [START_REF] Lotos | A formal description technique based on the temporal ordering of observational behaviour[END_REF] process models. One of its important features is the capability to compare labelled state transition systems modulo an equivalence or preorder rela-tion. The comparison is supported by the CADP Aldebaran bi-simulator library. If the submitted labelled state transition systems are not equivalent, a diagnostic Þle is generated to show the failed transition.

The labelled state transition systems of our case study are Þrst described in LotosNt [START_REF]CADP-Team[END_REF] (Fig. 16), a simpliÞed version of the Lotos language, then they are transformed to full Lotos programs. Labelled sate-transitions systems in BCG (binary coded graphs) format are generated for each Lotos description. Finally the two BCG automata are compared with the bi-simulator modulo observational equivalence relation.

Smartphone game application UI adapted to PC platform

The second case study concerns an interface of a mobile casual game application called "Marble Legend". It is a single player game where a user scores when he/she eliminates series of marbles of the same color. In this game, the user must create three or more consecutive marbles of a given color. Marbles of the same color are thrown by a shooting source (a frog). The ultimate goal of the game is to eliminate all marbles before they reach a central hole where they are sucked by a monster. The user interface of this application is composed of seven screens displayed according to the evolution of the game. First, the user selects, from the main menu, either to Fig. 16 A section of LotosNt code corresponding to lts Pct tune the game or to play in one of the two proposed game modes: adventure or challenge modes (Þrst screen). Once the game mode is selected (second and third screens), the user eliminates series of marbles before the time limit associated to the current game level is reached (fourth screen). When the user completes the game actions of the current level, score rates are displayed. Then, the user selects either to replay the current level (for example to increase his/her score), to move to the next level or to return back to the main menu (Þfth screen). In case the user fails in this level (i.e., the marbles are sucked by the monster), he/she is forced either to retry again or to leave the current level and return to the main menu (sixth screen). At any time, for a given level, the user can pause the game. He/she can also select either to continue, restart the current level or return back to the main menu (seventh screen). The CTT task model depicted in Fig. 17 describes the different user actions involved by the task consisting in playing the marble game. The following subtasks are detailed below.

1) Tune (subtask TA) allows a user to parameterize the game environment: tune of sound mode (T 1 ), ambient music (T 2 ) or colors for scenes (T 3 ) independently.

2) Play is dedicated to the description of the game playing (subtask TB). The user selects one game mode (T 4 ) and then tries to complete the game for the corresponding level before the allowed time limit (T 5 ). Therefore, T 5 is decomposed as follows. The user starts the current level (launches T 9 ). He/she shoots colored marbles, issued from the outlet of the source (the frog), in the direction of the lines of marbles before they are sucked into the central hole representing the mouth of the monster (T 10 ). At any time, for a given level, the user may change marble color or reverse the emission order of marbles at the shooting source (T 11 ). The user can also turn the game temporary to pause (T 12 ). He/she may decide to continue, stop the game at the current level or return back to the main menu.

3) Finally, the Interrupt (subtask TC) is triggered when the game is interrupted either if the game level is completed, failed or stopped by the user. The user may move to the next level in case of success (T 7 ), retry again the current game level in case of failure (T 6 ) or exit the game (T 8 ). The remainder of this section, focuses on the TryStage subtask (T 5 in Fig. 17). Our objective is to study the plasticity of the interaction technique used to perform this task. We address the cases of a smart phone (with only a touch screen) and a personal computer (with a mouse). We show how the plasticity property of the TryStage task (T 5 in Fig. 17) can be modeled for both two platforms: the source platform is a smartphone and the target one is a personal computer. The four-step methodology we have deÞned is deployed for this case.

Design

Let lts source and lts targetPc be two labelled state transition systems modeling the subtask TryStage (T 5 in Fig. 17).

• lts source is the labelled state transition systems associated to the source system syst source (i.e., a smartphone platform). It models the interaction task T 5 on the smartphone platform. The CTT task model associated to the TryStage task T 5 on the smartphone syst source is depicted in Fig. 18.

• lts targetPc is the one associated to the target system syst targetPc (i.e., a personal computer). It models the in-teraction task T 5 on the PC platform. The target CTT task model for this task is depicted in Fig. 19.

In order to build the different labelled state transition systems corresponding to each CTT task model of both platforms, a label is associated to each user action of these CTT task models. Table 3 describes all these correspondences. From the CTT models of Figs. 18 and 19, the following labelled state transition systems are obtained for the TryStage user task T 5 .

1) The lts lts source representing the interaction on the smart phone platform is given by the labelled state-transition system of Fig. 20.

2) The lts lts targetPc representing the interaction on the personal computer platform is represented in Fig. 21. At this stage we obtain a pair of (lts source , lts targetPc ). We need to compare these lts in order to be able to check the plasticity property of the interaction task T 5 when using a smartphone or a PC platform.

Irrelevant actions identiÞcation

The next step identiÞes the possible internal actions considered as not relevant to perform the suited interaction. The labels corresponding to these actions in both lts source or lts targetPc are set to τ. The action Move Mouse on the deÞned labelled state transition system is not relevant for the interaction. Indeed, the presence of this action in the CTT task model expresses a cursor movement to reach a target Þeld in a given form. Moving a cursor can be done repeatedly without any relevant effect from interaction point of view. Therefore, the occurrences of the label e 1 are set to τ. Another pair of lts (lts spt , lts Pct ) is obtained after irrelevant action removal. Note that the lts lts spt , corresponding to the lts source (Fig. 20) remains unchanged since it does not contain any occurrence of the label e 1 . The lts lts Pct of Fig. 22 corresponds to the lts lts targetPc (Fig. 21) obtained after the occurrences of labels e 1 have been set to τ.

Rewriting

The set of labels of the two lts lts spt and lts Pct obtained after Fig. 22 Irrelevant actions set to τ in lts for a PC platform removing irrelevant actions are still different sets. A rewriting step, exploiting relations on labels borrowed from the ontology is required to obtain two labelled state transition systems with a single set of labels. Let E and E ′ be the two sets of labels of lts spt and lts Pct respectively. Let LabDi f f be the set of different labels of lts spt and lts Pct . It is deÞned by

LabDi f f = (E ∪ E ′ ) -(E ∩ E ′ ) = {e 2 , e 3 , e 4 }.
Let E s be the set of labels of lts spt to be rewritten.

E s = E ∩ LabDi f f = {e 4 }.
Let E ′ p be the set of labels of lts Pct to be rewritten.

E ′ p = E ′ ∩ LabDi f f = {e 2 , e 3 }.
The relation Γ (see DeÞnition 11) provided by our ontology is the equivalence and/or subsumption relationships. These relations mean that user actions and/or user interactions with the same effect (equivalent or subsumed effect) can be replaced by the interactive task corresponding to this effect. The result of this substitution operation is a singleton A = {g} containing a label neither in E nor in E ′ . This label must be rewritten according to the identiÞed ontological relation in order to get a same set of labels. Figure 23 shows instances of the ontology we have used to deÞne such relations. When applied, the rewriting function φ (see DeÞnition 12) produces the labels deÞned in Table 4. The label g, introduced in Table 4, corresponds to the interactive task GO. It deÞnes a substitute for the labels corresponding to the user actions Click and Point (see Table 3). Indeed, this label factorizes and represents the effect of the two actions.

After rewriting the labels of lts spt and lts Pct , the new labelled state transition systems lts sptr and lts Pctr are obtained. After this rewriting step, the two lts have the same set of labels which is {g, τ}.

Checking

As for the previous case study, the Þnal step concerns checking the behavior equivalence on the obtained labelled state transition systems. In the same manner, observational equivalence between the two obtained labelled state transition systems is checked. The Þnal result shows that lts spctr and lts Pctr are weakly bi-similar. Therefore, we can formally assert that the interactions described by the task models of Figs. 18 and 19 perform the same task, and thus the devices and the interactions may be substituted. In other words, the equivalence of the corresponding rewritten labelled state transition systems modulo the relational weak bi-simulation relationship means that these two interaction techniques can substitute each other.

Like in the previous case study, the CADP model checker [START_REF]CADP-Team[END_REF] is used to compare labelled state transition systems. Thus, the labelled state transition systems of our second case study are Þrst described within in LotosNt [START_REF]CADP-Team[END_REF] (see Fig. 26), then they are transformed to full Lotos programs. Labelled sate-transitions systems in BCG format are generated for each Lotos description. Finally the two BCG automata are compared with the bi-simulator modulo observational equivalence relation.

Conclusion

This paper presents a formal approach to check the plasticity property of user interfaces. Our work helps user interface designers to Þnd a suitable alternative when interaction devices, of a user interface running platform, change.

Obtained results

We have proposed an approach supporting the veriÞcation of the equivalence of task models designed to describe two interaction techniques to achieve the same task with different interaction devices. The abstract part (representing the ab-stract task independently from any platform, and any environment) remains the same but several implementations are possible depending on the interaction devices (input/output) within the platform where the system or its interface (case of distributed systems) is running (concrete task). We started from a task model [START_REF] Paternò | CTTE: an environment for analysis and development of task models of cooperative applications[END_REF] representing the user task to carry out within the system and then we extracted the underlying labelled state transition system. We have exploited checking of the equivalence of heterogeneous labelled state transition systems or lts with different sets of labels deÞned in [START_REF] Ait-Ameur | A formal model to check systems substitutability: an application to interactive systems[END_REF]. Classical weak bi-simulation is extended by the use of an explicit relation to link labels of lts so that these lts can be rewritten to lts with the same set of labels and compared modulo weak bi-simulation. The deÞned approach has been applied to compare task models representing several interaction techniques in the Þeld of plastic user interfaces. A domain ontology of interaction techniques and devices has been proposed to provide the relation which links labels of the lts representing task models at interaction level. The application of our approach has been illustrated on two case studies through which we have shown how to check with formal tools if a task model designed for an application on a personal computer platform is equivalent to the task model designed for the same application but for another platform, a smartphone, a Touch Pad or a PC. This approach is particularly useful, for instance, to compare design strategies to face input/output hardware failure in critical interactive systems.

Discussion

The approach we have proposed relies on two pillars. The Þrst one is the use of an ontology to model domain properties. These properties are made explicit in the formalized task models. The second one relates to the use of formal methods to check behavior equivalence. Weak bi-simulation is used for this purpose. The interest of the developed approach is the separation of concerns. Indeed, the ontology of interaction may evolve independently of the task models deÞnition without altering the deÞned approach for checking user interfaces plasticity. The proposed approach is modular, it uses the ontology to deÞne relations on labels. The ontology may evolve independently of any application in order to integrate new devices and/or interaction modes. However, the work we have presented still require some methodological improvements out of the scope of this paper.

• The Þrst one consists requiring the existence of an agreed, shared and consensual ontology for the humancomputer interface domain which plays the role of a shared standard. This ontology, if available, shall describe unambiguously, interaction devices, interaction modes, and basic tasks, etc. Standardization bodies or UI designers communities can deÞne and manage such ontologies.

• Then, like for the devices and interaction modes, the rewriting of labels obeys to domain-speciÞc rules that shall be expressed in this ontology. A designer may be able to identify equivalences or subsumptions between the concepts of the human computer interaction devices so that he/she can select which label may replace a given one.

• The use of model checking and exhaustive state exploration for the veriÞcation of weak bi-simulation may lead to the explosion of the number of explored states. The complexity of the approach relies on the complexity of the weak bi-simulation checking and ontology reasoning algorithms. One may observe that the approach we have developed does not require model checking as unique veriÞcation procedure. Scalable techniques, like proof based methods, can be set up to handle this veriÞcation.

Some perspectives

This work opens several research perspectives. First, as for classical ontology engineering, the ontology used in this pa-per shall be consensual and agreed by the UI developers' community. Second, the deÞnition of the rewriting function should be automated. We are currently investigating how this function can be encoded within rewriting systems like Maude [START_REF] Clavel | Maude: speciÞcation and programming in rewriting logic[END_REF] or within logic reasoners like Racer [START_REF] Haarslev | Description of the RACER system and its applications[END_REF] or Pellet [START_REF] Bijan | Pellet: an owl DL reasoner[END_REF].

Third, more complex applications should be addressed in order to show how this approach scales up to other interactive systems. Finally, we believe that the provided relational bi-simulation relationship opens research paths for studying adaptive systems in general. Moreover, we also plan to study the case of degradation of an interactive system and use this approach for process adaptation of plastic user interfaces. Furthermore, the application of this approach in software adaptation and the comparison of web services composition or orchestration strategies can be envisaged.

DeÞnition 2 A 1 -→ s 2 e 2 -

 212 transition (s, e, s ′ ), also written, s e -→ s ′ denotes the transition from state s to state s ′ with label e. E * is the set of all sequences of labels. Let t = e 1 , e 2 , e 3 , . . . , e n ∈ E * be a sequence of labels. A path or a trace s 1 t -→ s n is a sequence of transitions of the form s 1 e → s 3 . . . s n-1 e n-1 -→ s n . It can be a Þnite trace or an inÞnite one. We write e ⋆ -→ to denote a sequence of zero or more transitions of label e in E. We also write s e =⇒ t the trace s τ

1 ) 2 ) 3 )

 123 Substitution ∃ e ∈ A such that Φ(a, b) = e to denote that labels a and b are replaced by a new label e in A. Right replacement : for a ∈ E ∃ b ∈ E ′ such that Φ(a, b) = a to denote that a label b ∈ E ′ of lts ′ is replaced by a label a ∈ E of lts. Left replacement : for b ∈ E ′ ∃ a ∈ E such that Φ(a, b) = b to denote that a label a ∈ E of lts is replaced by a label b ∈ E ′ of lts ′ . 4) Hiding : for a ∈ E, b ∈ E ′ with Φ(a, b) = τ, we denote the case of a pair of labels that should be hidden on both labelled transition systems lts and lts ′ after rewriting. DeÞnition 13 (Transforming labelled transition systems) The labelled transition systems lts = S , s 0 E, -→ and lts

  ing to the label relation Γ and to the rewriting function on labels Φ with -same sets of states S ⊤ = S and S ⊤ ′ = S ′ ; -same initial states s ⊤ 0 = s 0 and s ⊤ ′ 0 = s ′ 0 ; -sets of labels where different labels are rewritten thanks to the Φ rewriting function E ⊤ = (E -Pro j l (Γ))∪A∪{τ} and E ⊤ ′ = (E ′ -Pro j r (Γ)) ∪ A ∪ {τ};

Fig. 3

 3 Fig. 3 The ontology model represented as a UML class diagram

Fig. 4

 4 Fig. 4 Send SMS abstract task model

Fig. 7

 7 Fig. 7 The EditMsg task model of the interaction on a Touch Pad platform

Fig. 11

 11 Fig. 11 Irrelevant actions set to τ for the PC platform

Fig. 12

 12 Fig.[START_REF] Paternò | Concurtasktrees: a diagrammatic notation for specifying task models[END_REF] Irrelevant actions set to τ for the smartphone platform

  [START_REF] Mori | Tool support for designing nomadic applications[END_REF] , e 6 , e 7 , e 8 , e 9 , e 10 }.

Fig. 17 "

 17 Fig. 17 "Marble Legend" game abstract task model

Fig. 18 Fig. 20 TheFig. 21 The

 182021 Fig. 18 The TryStage task model for a smartphone platform

Fig. 23

 23 Fig.[START_REF] Mohand-Oussaïd | Modelling information Þssion in output multi-modal interactive systems using event-B[END_REF] Instances of our ontology concepts used to rewrite labels

Fig. 24

 24 Fig.[START_REF] Duke | Event model of human-system interaction[END_REF] The TryStage lts for a smartphone platform after rewriting labels

Fig. 25

 25 Fig.[START_REF] Brun | XTL: a temporal logic for the formal development of interactive systems[END_REF] The TryStage lts for a PC platform after rewriting labels

Fig. 26 A

 26 Fig. 26 A section of LotosNt code corresponding to lts spt

Table 1

 1 Mapping between user actions and corresponding labels

	CTT's actions	SigniÞcation	lts's labels
	KeyPress CHR	Press the keyboard's character key	e 1
	Point CHR	Point a character virtual key on a tactile screen e 2
	KeyPress NUM	Press the keyboard's digital key	e 3
	Point NUM	Point a digital virtual key on a tactile screen	e 4
	Click LBTN	Click the mouse's left button	e 5
	BtnPress DUDirBtn Press keypad's Down/Up direction button	e 6
	Move Mouse	Move the mouse	e 7
	BtnPress LRDirBtn Press keypad's Left/Right direction button	e 8
	Point Scrn	Point the tactile screen	e 9
	BtnPress CentBtn	Press keypad's central button	e 10

Table 2

 2 Label rewriting table

	User actions	lts's labels Substitution action φ Application
	(Click LBTN, BtnPress CentBtn)	(e 5 , e 10 )	GO	φ(e 5 , e 10 ) = g
	(Move Mouse, BtnPress DUDirBtn)	(e 7 , e 6 )	MoveCursor	φ(e 7 , e 6 ) = m
	(Move Mouse, BtnPress LRDirBtn)	(e 7 , e 8 )	MoveCursor	φ(e 7 , e 8 ) = m

Table 3

 3 Mapping between user actions and corresponding labels

	CTT's actions	SigniÞcation	lts's labels
	Move Mouse	Move the mouse	e 1
	Click LBTN	Click the mouse's left button	e 2
	Click RBTN	Click the mouse's right button	e 3
	Point Scrn	Point the tactile screen	e 4

Table 4

 4 Label rewriting table

	User actions	lts's labels Substitution action φ Application
	(Click LBTN, Point Scrn) (e 2 , e 4 )	GO	φ(e 2 , e 4 ) = g
	(Click RBTN, Point Scrn) (e 3 , e 4 )	GO	φ(e 2 , e 4 ) = g

[START_REF] Thevenin | Plasticity of user interfaces: framework and research agenda[END_REF] The word platform is used to characterize the system on which the described UI is available. It gathers the software part, the hardware devices and the offered interaction capabilities of this system