Database of Case Studies Achieved Using CADP

Verification of Plastic User Interfaces Exploiting Domain Ontologies

Organisation: INPT-ENSEEIHT-IRIT, Toulouse (FRANCE)

Method: ConcurTaskTrees
LNT

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Human-Computer Interaction.

Period: 2015

Size: 17 states, 32 transitions.

Description: A plastic user interface (UI) is designed to run on several target platforms and to support different interaction modes and/or devices. In addition, a plastic UI is capable to adapt from a given platform to another. Plasticity is an important concern for critical systems, because interaction continuity must be preserved during platform switches. An UI handles a set of possible user tasks, commonly defined by a task model. A plastic UI requires a task model for each platform, with the drawback that a task model has to be verified and validated for each platform.

This case-study investigates the formal verification of the plasticity property of an UI, proposing a technique to formally check if two task models describe the same system interaction. More precisely, each task model is first formalized as a labelled state-transitions system (LTS). Then the equivalence of two task models is checked by establishing a bisimulation relationship between their corresponding LTSs. The main challenge is that the LTS might have different labels. Exploiting an ontology of interaction devices and modes, it is possible to define rewrite operations that yield LTSs with a common set of labels, enabling the application of classical bisimulation.

The approach is illustrated on a web application, sending an SMS from a PC or from a Smartphone, showing that two task models are equivalent modulo an interaction domain ontology. First the task models are formally described as ConcurTaskTrees (CTT). Then they are translated into LNT. For this step, it is helpful that the operators of CTT are inspired by those of process algebras (precisely those of LOTOS). Third, the corresponding LTSs are generated and labels rewritten according to rewrite rules based on an ontology of interaction. Finally, bisimulation equivalence of the renamed LTSs is checked using the BISIMULATOR tool.



Conclusions: Bisimulation extended with a relation among labels, derived from an ontology of interaction, is helpful to formally assess plasticity of user interfaces.

Publications: [Chebieb-AitAmeur-15] Abdelkrim Chebieb and Yamine Aït Ameur. "Formal Verification of Plastic User Interfaces Exploiting Domain Ontologies". Proceedings of the International Symposium on Theoretical Aspects of Software Engineering (TASE 2015), Nanjing, China, pp. 79-86, IEEE Computer Society, September 2015.
Available on-line at: http://dx.doi.org/10.1109/SCC.2015.23

Contact:
Yamine Aït-Ameur
INPT-ENSEEIHT-IRIT
2, rue Charles Camichel, B.P. 7122
31071, Toulouse Cedex 7
FRANCE
Email: yamine@enseeiht.fr



Further remarks: This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Tue Mar 15 12:13:59 2016.


Back to the CADP case studies page