|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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 [Chebieb-AitAmeur-17] Abdelkrim Chebieb and Yamine Ait Ameur. "A Formal Model for Plastic Human Computer Interfaces". Frontiers of Computer Science, March 2017. Available on-line at: http://link.springer.com/article/10.1007/s11704-016-5460-3 |
| 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 |
Back to the CADP case studies page