INPT-ENSEEIHT-IRIT, Toulouse (FRANCE)
CADP (Construction and Analysis of Distributed Processes)
17 states, 32 transitions.
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.
Bisimulation extended with a relation among labels, derived from an
ontology of interaction, is helpful to formally assess plasticity of
Abdelkrim Chebieb and Yamine Aït Ameur.
"Formal Verification of Plastic User Interfaces Exploiting Domain
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
2, rue Charles Camichel, B.P. 7122
31071, Toulouse Cedex 7
|Further remarks:||This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|