Abdelkrim Chebieb
email: kchebieb@esi.dz

Yamine Ait-Ameur
email: yamine@enseeiht.fr

Formal verification of plastic user interfaces exploiting domain ontologies

This paper presents a formal model to check the interaction plasticity on a user interface (UI). An interaction is seen as an implementation (achievement) of a user task by means of interaction devices and modes of a given platform. The interaction plasticity is the ability of UI to support several interactions to perform the same task. In this work, two task models, containing different sets of interactions, are observed to check if they describe interactions that perform the same task. Each task model is represented by a labelled state-transitions system (lts). Due to the use of different interaction modes and devices, the obtained lts have different set of labels. Weak bisimulation relationship is revisited to handle these transition systems by defining a relation on labels. This relation is borrowed from an ontology of interaction modes and devices. Model checking techniques are set up to automatically establish such a bi-simulation. A case study is used to illustrate how the approach works.

I. INTRODUCTION

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 (qualified to be a plastic UI). Indeed, a plastic UI shall be able to switch, statically (at design time) or dynamically (at run time), from a given platform to another. The target platform may support (exactly, less or more) interaction capabilities than the original one. Plasticity is an important concern particularly for critical systems (the interaction continuity must be guaranteed when changes occur on the platform).

Two relevant characteristics relate to plasticity: adaptivity and adaptability. 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.

A user interface handles a set of possible user tasks, realized by a given user, when interacting with the system, through this user interface by means of the available interaction devices. A task model is commonly defined to describe the interaction realizing these tasks. It highlights both the tasks to be achieved (abstract part of the task model) and how these tasks are effectively realized (concrete part of the model).

The design of a multi-platform interfaces entails building a task model for each platform. The abstract part of this task model remains identical for each platform while the concrete level is adapted to each specific platform according to its interaction modes and/or devices. The main drawback of this approach is the need to perform task model verification 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 hardware side of the UI (lose and/or gain of interaction devices in the platform), is identified 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].

This paper presents a novel approach supporting the formal verification of the plasticity property of a user interface. This approach sets up a formal technique to check if two task models describe the same system interaction. More precisely, task models are formalized as labelled state-transitions systems (lts). Then, the equivalence of two task models is checked by establishing a bi-simulation relationship between their corresponding lts. The novelty of the approach lies in the capability to handle the comparison of lts with different labels (labels from interactions, issued from different equivalent devices, for example) thanks to the definition of a relational bi-simulation relationship. This relation exploits the relations between labels, borrowed from an ontology of interaction devices and modes. These relations make it possible to rewrite the lts to get new lts, defined on a common set of labels on which it becomes possible to check classical bi-simulation.

This paper is structured as follows. The next section presents a synthetic state of the art of the HCI plasticity, related to our work. We give a vision of the plasticity as a knowledge domain to justify the use of ontologies. Then our formal model to handle plasticity, based on the comparison of task models, modeled as labelled transition systems and the bi-simulation relationship is presented. Finally a case study, illustrating how the proposed approach works is sketched.

II. STATE OF THE ART

A. Design of Plastic UI

Studying plasticity of user interfaces has drawn the attention of researchers. [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. Below, we briefly review significant works achieved to handle plasticity.

The earliest approaches to address user interface adaptation, like ACE [START_REF] Johnson | Ace: building interactive graphical applications[END_REF], FRUITS [START_REF] Kawai | Designing interface toolkit with dynamic selectable modality[END_REF] and Multi-modal Widgets [START_REF] Crease | Caring, sharing widgets: a toolkit of sensitive widgets[END_REF], DOI 10.1109/TASE.2015. [START_REF] Buxton | A three-state model of graphical input[END_REF] proposed to implement adaptation capabilities directly at software level. The leading idea consists in embedding the various characteristics of interaction modalities and devices present on different platforms inside a set of interface components, used to implement the UI.

Adaptation at runtime was addressed by techniques, handled by ToolGlasses [START_REF] Bier | Toolglass and magic lenses: the see-through interface[END_REF] and FACADE [START_REF] Stuerzlinger | User interface faades: towards fully adaptable user interfaces[END_REF]. Their objective is to support adaptation of the UI at runtime without any modification of its internal code. Adaptation characteristics were integrated as a feature of the operating system so that the user can, for example, move a part of the UI, of a given application, from a window to an other when this application runs. These approaches propose adaptive UI but not adaptable ones (users adapt UI at runtime).

Handling plasticity characteristics, at early stages of the UI development process, was advocated with the emergence of the reference framework of the CAMELEON project [START_REF] Calvary | The cameleon reference framework[END_REF]. The leading idea is to design a UI once and apply successive suitable transformations to fit the characteristics (interactions techniques, modalities, environment...etc) of various target platforms. Several techniques and toolboxes resulted from this approach. The most significant 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 (a)[END_REF]. USIXML is an XML-based framework, where a UI is specified 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 specified 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 (a)[END_REF].

The rendering adaptation was also studied. In AMF [START_REF] Samaan | The amf architecture in a multiple user interface generation process[END_REF], patterns of interaction techniques are defined in a multi-agent setting. Each pattern is used to adapt the UI input/output according to the interaction mode it describes. Similarly, the UI Module Adaptation approach of [START_REF] Dery-Pinna | Component model and programming: a first step to manage human computer interaction adaptation[END_REF] allows a user to adapt the GUI to the context of use (platform, environment, user profile) by rearranging the application's user interface. Here, the user is allowed hide and/or to show elements of the interface, which match user interaction preferences and requirements.

More recently, taking into account the context of use, has been addressed, particularly the user profile and environment. In [START_REF] De Oliveira | Transportation ontology definition and application for the content personalization of user interfaces[END_REF] a UI is adapted, according to user profiles, stored in an ontology. User profiles 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 special components, called IBC (Interactor Business Component) which are used to implement adaptive UI widgets.

This review of existing work shows that there is a need to focus on the interaction between the user and the interface in the plastic UI development process. Moreover, the verification of the plasticity property of UI should be formally and explicitly addressed in the same development process.

B. Making domain knowledge explicit to handle plasticity

According to [START_REF] Coutaz | HCI and Software Engineering for User Interface Plasticity[END_REF], the rapid evolution of IT technologies increased the ubiquity of user interfaces (outside its classical platforms). The diversity of technologies and platforms, equipped with various interaction devices and modalities, is an important factor in the design space of plastic user interfaces [START_REF] Vanderdonckt | A design space for context-sensitive user interfaces[END_REF].

Various approaches in the literature propose to handle this diversity: model-driven approaches, operating system (runtime) approaches and toolboxes approaches [START_REF] Demeure | The comets inspector: Towards run time plasticity control based on a semantic network[END_REF]. A review of the proposed approaches highlights the need to identify different technologies (interaction devices, rendering technologies, implementation techniques and languages etc.) which equips computing platforms of the market. The most known are interaction patterns used with AMF [START_REF] Samaan | Task models and interaction models in a multiple user interfaces generation process[END_REF], directory of UI development technologies in COMET environment [START_REF] Demeure | Comet(s), a software architecture style and an interactors toolkit for plastic user interfaces[END_REF] and user profile-based UI transformation algorithm MAGALLEN [START_REF] Masson | Examples galleries generated by interactive genetic algorithms[END_REF]. In AMF different interaction techniques are specified as patterns and used in adaptation strategies. The COMET environment proposes to maintain a directory of known rendering technologies. This directory is explored by a COMET (plastic component) to determine which rendering technology is suitable to a given target platform. MAGALLEN proposes to apply a genetic algorithm to implement a user profile-based transformation mechanisms. In these approaches, the design of the UI is seen as an exploration of the design space to find a suitable UI to fit the suited user profile.

Cataloguing devices, interaction modes, platforms, etc. and the relations that hold among them, helps the designer to develop plastic interfaces. The first attempt to model this knowledge is USIXML [START_REF] Limbourg | Usixml: A language supporting multi-path development of user interfaces[END_REF]. A definition of the concepts, manipulated by different models of a UI design process, is provided and modelled thanks to an ontological meta-model. This meta-model drives the generation of a user interface with various rendering target platforms. However, the ontology is terminological one, based on words and terms instead of being a conceptual ontology. We also quote the work of [START_REF] De Oliveira | Transportation ontology definition and application for the content personalization of user interfaces[END_REF], where the same kind of ontology was used to adapt the user interface of an information system, according to the user profile in transportation domain.

Our claim is that user interface adaptation cannot be achieved without the use of a repository, storing all the knowledge about existing interaction techniques, devices and technologies. We believe that conceptual ontologies [START_REF] Jean | Domain Ontologies: A Database-Oriented Analysis[END_REF] are well adapted to support such descriptions.

C. An ontology for plasticity: our view

In our approach, we advocate the use of conceptual domain ontologies, which rely on the description of concepts characteristics and on ontological reasoning (subsumption computation), in order to determine whether a given concept or an expression of concepts may replace (equivalence, subsumption or entailment) by another concept or expression on concepts. Therefore, our ontology model includes user-tasks expressions and interaction devices (See figure 3). Instances of the concepts (See figure 9) of our ontology are a formalization of task models, describing interaction techniques similar to those modeled by the patterns of AMF [START_REF] Samaan | Task models and interaction models in a multiple user interfaces generation process[END_REF], or by ICON [START_REF] Dragicevic | Support for input adaptability in the icon toolkit[END_REF], or in the taxonomy of interaction devices of [START_REF] Buxton | A three-state model of graphical input[END_REF]. The ontology we propose plays a role of a dictionary of interaction techniques [START_REF] Berti | A taxonomy for migratory user interfaces[END_REF] [27], representing the various ways to perform various user tasks by various interaction devices. In other words, task models, stored by the instances of our ontology, describe patterns of interactions techniques, used to perform almost known user tasks, in a similar manner with those sketched in [START_REF] Constantine | Canonical abstract prototypes for abstract visual and interaction design[END_REF] (select, copy, text input ...etc).

Finally, note that the definition of an ontology beside of the UI design models provides with a loosely coupled approach, authorizing the evolution of the ontology independently of the models and vice versa.

III. OUR APPROACH

Our goal is to verify that two task models, describing two different interactions, are two implementations of the same task with different interaction devices. In this approach, task models are represented by labelled state transition systems (lts) and are compared, using the bi-simulation relationship. If these lts are bi-similar then the task models they represent describe the same user task. Because physical actions of these task models are not the same, due for e.g. to the use of different devices, labels in the corresponding lts may not be the same. At this level, ontology reasoning is triggered to check whether the actions corresponding to these labels have the same semantics. If so, they are rewritten so as the lts share the same set of labels and offer the possibility of a bi-simulation checking. When possible, lts labels are rewritten, thanks to the relations available in the formalizing part of the HCI knowledge domain, related to the user interaction devices and techniques.

Our approach is based on a stepwise methodology, involving the following steps. 1) Build an lts for each task model. 2) Exploit domain ontology relationships to obtain lts sharing the same set of labels. 3) Check bi-simulation for the lts obtained at the previous step. Let us recall some useful definitions.

A. Task modeling with CTT and labelled transition system

CTT [START_REF] Paternò | Concurtasktrees: A diagrammatic notation for specifying task models[END_REF] notation provides the capability to describe complex user tasks, combining temporal composition operators (inspired from LOTOS process algebra [START_REF] Lotos | A formal description technique based on the temporal ordering of observational behaviour[END_REF]), and atomic tasks (user physical actions on interaction devices). A tree structure is associated to each CTT task model. Figure 1 shows a CTT tree with: -Iteration T ⋆ : T is activated zero or more times. In our approach, an 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 the automaton, representing the task model of the figure 1

B. The bi-simulation relationship

The notion of bi-simulation was initially defined by Milner [START_REF] Milner | A Calculus of Communicating Systems[END_REF] to compare processes (called observational equivalence). This relation defines equivalence on states of lts. Depending on the kind of considered actions (internal τ or observable), two kinds of observational equivalence exist: strong bi-simulation, for observable actions, and weak bi-simulation which considers both observable and internal τ (stuttering) actions [START_REF]Communication and concurrency[END_REF].

We consider the definition of bi-simulation for two different lts. Let lts = S, s 0 E, -→ and lts ′ = S ′ , s ′ 0 E, -→ ′ be two transition systems with the same set of labels E and S ∩ S ′ = ∅.

Definition 2: Strong bi-simulation. Strong bi-simulation relation ∼⊆ S × S ′ , is a bi-simulation equivalence defined on states. For a given action e, a transition e -→ and two states p i and q i , we say that

(p i , q i ) ∈ ∼ if ∀p i e -→ p j ∈-→: ∃q i e -→ ′ q j ∈-→ ′ ∧(p j , q j ) ∈∼ ∀q i e -→ ′ q j ∈-→ ′ : ∃p i e -→ p j ∈-→ ∧(q j , p j ) ∈∼
By extension of this definition, two lts are strongly bi-similar, noted ≃ lts , if their initial states are bi-similar i.e. (s 0 , s ′ 0 ) ∈ ∼ (a strong bi-simulation including initial states can be built).

Definition 3: Weak bi-simulation. Weak bi-simulation relationship noted ≈ ⊆ S × S ′ , is a bi-simulation equivalence defined on states. For a given action e, a transition e -→ and two states p i and q i , we say that

(q i , q i ) ∈ ≈ if ∀p i e -→ p j ∈-→ ∃q i τ ⋆ .e.τ ⋆ -→ ′ q j ∈-→ ′ ∧(p j , q j ) ∈≈ ∀p i τ -→ p j ∈-→ ∃q i -→ τ ⋆ q j ∈-→ ′ ∧(p j , q j ) ∈≈ ∀q i e -→ ′ q j ∈-→ ′ ∃p i τ ⋆ .e.τ ⋆ -→ p j ∈-→ ∧(q j , p j ) ∈≈ ∀q i τ -→ ′ q j ∈-→ ′ ∃p i τ ⋆
-→ p j ∈-→ ∧(q j , p j ) ∈≈ By extension two lts are weakly bi-similar, noted ≅ lts , if their initial states are weakly bi-similar i.e. (s 0 , s ′ 0 ) ∈≈ (a weak bi-simulation including initial states can be built).

Bi-simulation relationships are defined on a single set of labels and compare transitions with the same labels. To check plasticity, comparing lts with different sets of transition labels is required.

C. A formal model for designing plastic interfaces

The representation of task models by Interactive systems, proposed in our approach, leads to lts with different sets of labels, corresponding to interaction actions. Relational bisimulation relationship, defined below, relaxes the classical definition to handle different sets of labels. This definition introduces a relation, Γ on pairs of labels, used to rewrite different labels.

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 ′ , ∃ β ∈ E ′ -E such that (α, β) ∈ Γ ∀ β ∈ E ′ -E, ∃ α ∈ E -E ′ such that (α, β) ∈ Γ
The left and right projection functions P roj l and P roj r are associated to Γ.

Informally, Γ links labels belonging to the set of labels that are not in E∩E ′ . Note that for plasticity checking purpose, this relation will be borrowed from the defined domain ontology. The defined lts ⊤ and lts ⊤ ′ are labelled transition systems with the same set of labels, since

E ⊤ = E ⊤ ′ .
Definition 7: Relational weak bi-simulation relationship on lts. 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 definition 4, -Φ is a label rewriting function according to definition 5. Then, ≅ Γ,Φ lts ⊆ LT S × LT S is 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 It becomes possible to compare labelled transition systems with different sets of labels.

Definition 8: Plasticity property. For two user interfaces U I 1 and U I 2 , modeled by two task models, corresponding to the labelled transition systems lts 1 , lts 2 ; and an ontology Ont, defining the relation Γ Ont ; and a rewriting function Φ Ont ; we say that U I 1 and U I 2 satisfy plasticity property if lts 1 ≅ ΓOnt,ΦOnt lts lts 2 . Note that if Γ = ∅ ∧ E1 = E2 the plasticity property does not hold.

D. An ontology of interaction

A domain ontology of both tasks and interaction devices is defined to supply Relational bi-simulation with the relation Γ and the rewriting function Φ on labels. The different actions performed on an interactive system, together with their associated devices, can be categorized within an ontology. Classes and properties related to interaction devices and modes are categorized in a subsumption relationship. Figure 3 shows a class diagram, representing the core concepts of the obtained ontology. It defines hierarchical categories of interactive actions and/or devices. The main concepts of this ontology are the interaction device (DEV), the interactive task (INTTASK) and the user interaction (INTR). Interaction device (DEV) describes the various categories of devices. It is mainly based on most known taxonomies of interaction devices, published in the literature [START_REF] Berti | A taxonomy for migratory user interfaces[END_REF], [START_REF] Buxton | A three-state model of graphical input[END_REF], [START_REF] Card | The design space of input devices[END_REF] and [START_REF] Frohlich | The design space of interfaces[END_REF]. The concept Interactive task (INTTASK) refers to the abstract interaction, as defined in [START_REF] Constantine | Canonical abstract prototypes for abstract visual and interaction design[END_REF] -examples of instances of this class are select, copy, text input etc. User interaction (INTR) class represents the patterns of interactions techniques as defined in [START_REF] Navarre | A formal approach for user interaction reconfiguration of safety critical interactive systems[END_REF], [START_REF] Samaan | Task models and interaction models in a multiple user interfaces generation process[END_REF] and [START_REF] Dragicevic | Support for input adaptability in the icon toolkit[END_REF]. It can be either a basic interaction, corresponding to a user action (ATOMIC-UA), or a composite action, defining the behavior of the user and the machine during the interaction in terms of user actions. The actions composition operators are the sequence (SEQ), concurrent (PARA), choice (CHOI) and iteration (ITER). Each interaction materializes an alternative way to perform an interactive task (INTTASK) with a set of user actions, allowed by interaction devices (DEV) available within a computing platform.

Among the different kinds of ontological relations between user actions, offered by our ontology, the equivalence and the subsumption (is a) relationships are exploited by our approach. The former means that two user interactions INTR are equivalent when they materialize the same interactive task INT TASK. The latter describes the situation where an atomic task can be performed either by an atomic action ATOMIC UA or by a composite task COMPOSITE. Particularly, the relation linking the concept INT TASK and the concept INTR is exploited when rewriting labels of the lts in the following manner:

• A label, derived from equivalent ATOMIC UA, is replaced by the label, derived from the INTR they perform (materialize). Equivalence is a substitution.

• A label, derived from INT TASK, replaces two sets of equivalent COMPOSITE interactions (both realize the same INT TASK)

• A label, derived from INTR, can replace a set of labels derived from an ATOMIC UA or COMPOSITE interactive task if it is subsumed by a single ATOMIC UA that realizes the same INT TASK. Subsumption is a left or right replacement.

Finally, as for classical ontology engineering, the ontology, defined above, shall be consensual and agreed by the user interface developers' community. This aspect is out of scope of our paper and the presented ontology can be subject to evolution or amendment without impacting the defined approach.

E. A Methodology for checking user interface plasticity

The main goal in our proposed approach is to check that a pair of different interactive systems allows a user to perform the same tasks, using different interactive techniques with available interactive devices and modes. Considered interactive systems are formalized as labelled transition systems, and then a relational bi-simulation on these systems is checked, provided that a relation on labels of their corresponding labelled transition systems is available -using our ontology. Informally, our approach states that a transition system is said plastic if it can be at least implemented by two interactive systems, which are linked by a relational bi-simulation relationship, according to a given relation on labels. Our stepwise methodology, to check that a pair of interactive systems (Syst source , Syst target ), consists of the following steps:

1-Design. Formalize interactive systems (Syst source , Syst target ) as a pair (lts source , lts target ) of labelled transition systems.

2-Irrelevant action identification. In the obtained lts, at the previous step, identify the 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. Identify the pairs of labels that are different in lts source and lts target , obtained at the previous step. Then, rewrite these pairs of labels, using the relation on labels of the lts, defined in the interaction ontology. At this step, the two lts source and lts target have the same labels.

4-Checking. Check classical weak bi-simulation between LTS lts source and lts target , obtained at the previous step. If they are bi-similar, then we can assert that they encode the same task model.

IV. APPLICATION TO A CASE STUDY

In order to illustrate the previously described formal method for checking UI plasticity, we consider the case of checking if a web application, initially designed to send SMS on a personal computer (PC), runs on a Smartphone as well. Below, we show how two task models, describing two user interfaces, concretizing the same task on these two concrete different platforms (PC and Smartphone).

A. Tasks description

Figure III-E shows the CTT task model, describing how the application UI allows a user to send an SMS. The user opens a session to access his own space (subtask T A). Then, he writes a message and sends it (subtask T B). Finally, he logs out from his own space (subtask T C). The leaves of the defined task model are actions that a user must carry out to achieve each subtask. To login, a user gives his identifier (T 1 ) and password (T 2 ) in any order and submits them (T 3 ). Then, he triggers the message editor (T 4 ), edits his message (T 5 ) by entering the text of the message (T 8 ) and the phone number of the recipient (T 7 ) (in any order). Then, he decides whether he sends the entered message (T 6 ) or saves it (T 10 ) or cancels it (T 11 ). To send the message, the user must request the system (T 12 ) and confirm the action (T 13 ). If he does not confirm sending the message (T 14 ), he chooses to save it (T 15 ) or to cancel the whole operation (T 16 ). Finally, the user closes the session (T 17 ).

B. Design

In order to keep this paper in a reasonable length, we only describe the subtask EditMsg (T 5 ). We show how our formal approach applies to establish the similitude (equivalence) of this subtask, when deployed on a PC or on a Smartphone. The Task model of figure 5 describes how to carry out the task (T 5 ) on the PC platform. The model of figure 6 shows how the same task is achieved on a Smartphone. As a consequence, two interactive systems (Syst source , Syst target ), corresponding respectively to the PC and to the Smartphone platforms, are described.

From the task models of figures 5 and 6, a pair (lts P c , lts P h ) of lts, formalizing the behavior of (Syst source , Syst target ), are obtained. As mentioned above, CTT models are formalized as LOTOS process algebra expressions and thus an lts can be associated to each CTT expression.

The lts lts P c and lts P h of figures 7 and 8 correspond to Syst source and Syst target , respectively. They describe the interactive system, running on a PC and on a Smartphone respectively.

C. Identification of irrelevant actions

The labels, corresponding to irrelevant actions in the task model with respect to the plasticity, are identified from the ontology. In this case study, the iterated user actions, corresponding to moving the mouse in the screen on the PC {MoveMouse}, or moving buttons on the Smartphone {BTNPressDUDirBtn, BTNPressLRDirBtn}, are considered as irrelevant. Only one iteration is considered in this case and the other iterations are set to τ for their corresponding labels (e 7 , e 6 , e 8 ) in lts P c and/or lts P h . Note that these actions could have been kept as they are if one may consider the number of times buttons are pressed, for example.

D. Rewriting

The next step consists in rewriting the different lts, involved in the task models, corresponding to (lts P c , lts P h ), in order to produce new lts that share the same set of labels. Let E P c and E P h be the set of labels, corresponding to lts P c and lts P h , respectively. LabDif f is the set of labels of lts P c and lts P h , which are different.

LabDif f = (E P c ∪ E P h ) -(E P c ∩ E P h ) = {e 5 , e 6 , e 7 , e 8 , e 9 , e 10 }

The set of labels E r s and E r t to be rewritten for lts P c , and lts P h , respectively, are defined below. At this level, according to the defined methodology, the rewriting function can be applied. This function is defined in table II. Figure 9 shows an excerpt of the ontology instances, used for this case study. Labels (g, m) appear after rewriting. The label g, corresponding to the interactive task (INT TASK) GO, replaces the labels corresponding to User Actions (AT OM IC U A), Click that acts on LBTN, and BtnPress that acts on CentBtn; because it represents the effect of the two actions. The label m, corresponding to the interactive task (INT TASK) MoveCursor, replaces the labels corresponding to user actions (AT OM IC U A), Move that acts on Mouse, BtnPress that acts on DUDirBtn, and BtnPress that acts on LRDirBtn.

E r P c = E P c ∩ LabDif f E r P h = E P h ∩ LabDif f = {e 5 ,

E. Checking

Once the previous steps are achieved, the labelled transition systems lts P ctr of figure 10 and the lts P htr of figure 11 are obtained for both the PC and the Smartphone, respectively. They share the same set of labels {e 1 , e 3 , m, g, τ }. It becomes possible to verify that the obtained lts are bisimilar by checking the observational equivalence relationship between them, i.e. by checking the weak bi-simulation relationship, previously defined. The final result shows that lts P ctr and lts P htr are weakly bi-similar. Therefore, we can conclude that the task models, described on a PC and on a Smartphone, can substitute each other, ensuring thus the plasticity property.

F. Tool support

The CADP c (Construction and Analysis of Distributed Processes) model checker [START_REF]Cadp web site[END_REF] has been set up to model tasks and check bi-simulation. This toolbox provides resources for compiling and checking Lotos [START_REF] Lotos | A formal description technique based on the temporal ordering of observational behaviour[END_REF] programs. In our approach, the lts are first, formalized in LotosNt [START_REF]Cadp web site[END_REF] (see figure 12), a simplified version of LOTOS. They are transformed into LOTOS programs. Then, an internal representation, by labelled transition system (automaton) in BCG format, is generated for each LOTOS program. Finally, the bi-simulation of the two BCG automata is checked, thanks to the BISIMULATOR module, using observational equivalence relationship option.

V. CONCLUSION

This paper presented a formal modeling approach to check the plasticity property of user interfaces. The objective is to allow UI developers check whether different user interfaces, running on different computing platforms, with different interaction techniques, and various available interaction devices, support the same user tasks. The approach relies on the formalization of task models by lts, where states record the UI changes and transitions are labelled with user actions. They offer a powerful model to describe behavioral aspects of task models. Our idea, to handle plasticity of user interfaces, comes from the fact that, once task models are formalized as lts, we observe that different paths with different actions of two task models may lead to equivalent states. This notion of equivalence is hard to establish because the actions, labeling the transitions, are not exactly the same ones. There is a need to express equivalence relations on such actions when such a relation holds. Therefore, one needs to make explicit the knowledge that some interaction devices, modes or actions have the same effect. This information represents an axiomatization of the interaction domain. We have chosen to model such a knowledge with domain ontologies, that are well adapted for the description of domain knowledge independently of any context of use. The proposed approach is based on two formal verification techniques. First, it exploits the bisimulation relationship to compare behaviors, expressed by lts. Second, the computation of the subsumption and equivalence relationships, within an ontology provided with equivalent or subsuming instances, that can be used to safely rewrite transition labels. The interest of the proposed approach is its loose coupling between the tasks models -the user interfaceand the ontology. Indeed, both may evolve independently.

Moreover, this approach can be used for handling plasticity at both design and runtime. On the one hand, checking bisimulation overall labelled transitions systems, ensures that a global task model can substitute another one. On the other hand, the fact that the bi-simulation relationship is defined on pairs of states ensures that two bi-similar states are equivalent. Thus, it becomes possible to switch from one state of an lts to its bi-similar state, of another lts, at runtime. A case study of a web application, sending an SMS from a Pc or from a Smartphone, showed how our approach works. It illustrates two equivalent task models modulo an interaction domain ontology.

Finally, this work opens several research perspectives. First, as for classical ontology engineering, the ontology used in this paper shall be consensual and agreed by the UI developers' community. Second, the definition of the rewriting function should be automated. We are currently investigating how this function can be encoded within rewriting systems like Maude. 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 bisimulation relationship opens research paths for studying adaptive systems in general.

Fig. 1 .

 1 Fig. 1. Example of CTTE task model

Definition 1 :

 1 Labelled Transition System. A Labeled Transition System (lts) is a structure S, E, -→ where S is a set of states, E is a set of actions (operation labels) and -→ ⊆ S×E×S is the transition relation. We write s e -→ s ′ to express the transition from state s to s ′ with action e. Internal actions are hidden with the label τ .

Fig. 3 .

 3 Fig. 3. The ontology model represented as an UML class diagram E ′ E. Let A be another set of labels different from the those of E ∪ E ′ , in other words A ∩ (E ∪ E ′ ) = ∅ Definition 4: Bi-directional relation on labels. Γ ⊆ E -E ′ × E ′ -E is a relation on labels of two labelled transition systems defined by∀ α ∈ E -E ′ , ∃ β ∈ E ′ -E such that (α, β) ∈ Γ ∀ β ∈ E ′ -E, ∃ α ∈ E -E ′ such that (α, β) ∈ ΓThe left and right projection functions P roj l and P roj r are associated to Γ.Informally, Γ links labels belonging to the set of labels that are not in E∩E ′ . Note that for plasticity checking purpose, this relation will be borrowed from the defined domain ontology.

Definition 5 :

 5 Rewriting function on labels. Let Φ : E × E ′ -→ (A ∪ E ∪ E ′ ∪ {τ }) be a function on labels of two labelled transition systems. Φ is defined by ∀ (α, β) ∈ Γ ∃ γ ∈ A such that Φ(α, β) = γ The definition of the rewriting function entails four different applications. 1-Substitution. If ∃ e ∈ A such that Φ(a, b) = e then labels a and b are replaced by a new label e in A. 2-Right replacement. If ∃ b ∈ E ′ such that Φ(a, b) = a then label b ∈ E ′ is replaced by a label a ∈ E. 3-Left replacement. If ∃ a ∈ E such that Φ(a, b) = b then label a ∈ E is replaced by a label b ∈ E ′ . 4-Hiding. Φ(a, b) = τ denotes the case of a pair of labels that should be hidden on both labelled transition systems after rewriting. Remark. When an ontology is used, substitution means that a subsuming concept is available and left (resp. right) replacement means that the left (resp. right) label is subsumed by the right (resp. left) one. Hiding means that the label is not relevant for plasticity. If Γ is empty, then no plasticity is possible. Definition 6: Transforming labelled transition systems. lts = S, s 0 E, -→ and lts ′ = S ′ , s ′ 0 E, -→ ′ are respectively rewritten to lts ⊤ = S ⊤ , s ⊤ 0 E ⊤ , -→ ⊤ and lts ⊤ ′ = S ⊤ ′ , s ⊤ ′ 0 E ⊤ ′ , -→ ⊤ ′ according to the label relation Γ and to the rewriting function on labels Φ as follows . -S ⊤ = S and S ⊤ ′ = S ′ i.e. same sets of states. -s ⊤ 0 = s 0 and s ⊤ ′ 0 = s ′ 0 i.e. same initial states. -E ⊤ = (E -P roj l (Γ)) ∪ A ∪ {τ } and E ⊤ ′ = (E ′ -P roj r (Γ)) ∪ A ∪ {τ } sets of labels enriched with the rewritten labels thanks to the Φ rewriting function. -transition relations are redefined on the new labels -→ ⊤ ⊆ 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}

Fig. 5 .

 5 Fig. 5. The EditMsg subtask ( T 5 ) deployed on a PC

Fig. 4 . 3 Fig. 7 .

 437 Fig. 4. Send SMS abstract Task Model

3 Fig. 8 .

 38 Fig. 8. lts on Smartphone platform

(

  e5, e10) GO φ(e5, e10) = g (e7, e6) MoveCursor φ(e7, e6) = m (e7, e8) MoveCursor φ(e7, e8) = m

Fig. 9 .

 9 Fig. 9. Instances of our ontology concepts used to rewrite labels

3 Fig. 10 .

 310 Fig. 10. lts on PC platform after rewriting labels

3 Fig. 11 .

 311 Fig. 11. lts on Smartphone platform after rewriting labels

  Fig. 12. A section of LOTOS NT code corresponding to lts P ctr

-

  Activation (≫): t 1 ≫ t 2 for t 1 followed by t 2 . -Choice ([ ]): t 3 [ ] t 4 non-deterministic choice on t 3 or t 4 . -Order independence (|=|): t 7 |=| t 8 for (t 7 ≫ t 8 )[ ](t 8 ≫ t 7 ). -Interleaving (|||): t 5 ||| t 6 parallel activation of t 5 and t 6 .

  .

						t 5
	0	t 3 t 7	1	t 8	4 3	t 6 t 5 t 6	6 7
	t 8		2	t 7	5	t 5 t 6	8
	Fig. 2. lts corresponding to a task model

TABLE I

 I

	.	USER ACTIONS AND CORRESPONDING LABELS
	CTT's atomic ac-	Signification	lts's
	tions			Labels
	KeyPress CHR		Press the keyboard character key	e1
	KeyPress NUM		Press the keyboard digital key	e3
	Click LBTN		Click the mouse left button	e5
	BtnPress DUDirBtn	Press keypad Down/Up	e6
			direction button
	Move Mouse		Move the mouse	e7
	BtnPress LRDirBtn	Press keypad Left/Right	e8
			direction button
	BtnPress CentBtn	Press keypad central button	e10

  e 7 } = {e 6 , e 8 , e 10 }

	TABLE II.	LABEL REWRITING TABLE
	lts's Labels	Substitution	φ
		action	Application

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.