A formal model for plastic human computer interfaces
Abdelkrim CHEBIEB, Yamine AIT AMEUR
A formal model for plastic human computer interfaces
The considerable and significant 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 specific 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 definition of the bi-simulation relationship to compare user interface behaviors when interaction modes are replaced by new ones.
formal modeling and verification / ontology based modeling / plastic user interfaces / adaptive systems
[1] |
Thevenin D, Coutaz J. Plasticity of user interfaces: framework and research agenda. In: Proceedings of INTERACT. 1999, 110–117
|
[2] |
Coutaz J, Calvary G. HCI and software engineering for user interface plasticity. In: Jacko J A, ed. HCI Handbook: Fundamentals, Evolving Technologies, and Emerging Applications, 3rd ed. Boca Raton, FL: CRC Press, 2012, 1195–1220
|
[3] |
Navarre D, Palanque P, Basnyat S. A formal approach for user interaction reconfiguration of safety critical interactive systems. In: Proceedings of International Conference on Computer Safety, Reliability, and Security. 2008, 373–386
CrossRef
Google scholar
|
[4] |
Calvary G, Coutaz J, Bouillon L, Florins M, Limbourg Q, Marucci L, Paternò F, Santoro C, Souchon N, Thevenin D, Vanderdonckt J. The cameleon reference framework. Deliverable D1 of the Cameleon project, 2002
|
[5] |
Mori G, Paternò F, Santoro C. Tool support for designing nomadic applications. In: Proceedings of the 8th International Conference on Intelligent User Interfaces. 2003, 141–148
CrossRef
Google scholar
|
[6] |
Samaan K. Prise en Compte du Modèle d’Interaction dans le Processus de Construction et d’Adaptation d’Applications Interactives. Dissertation for the Doctoral Degree. Lyon: Ecole Centrale de Lyon, 2006
|
[7] |
Limbourg Q, Vanderdonckt J, Michotte B, Bouillon L, López-Jaquero V. Usixml: a language supporting multi-path development of user interfaces. Engineering HCI and Interactive Systems, 2005, 134–135
|
[8] |
Palanque P, Paternò F. Formal Methods in Human-Computer Interaction. New York: Springer-Verlag, 1997
|
[9] |
Hartson H R, Siochi A C, Hix D. The UAN: a user-oriented representation for direct manipulation interface designs. ACM Transactions on Information Systems (TOIS), 1990, 8(3): 181–203
CrossRef
Google scholar
|
[10] |
Rix D, Hartson H. Developping User Interfaces: ensuring Usability Through Product & Process. New York: JohnWiley & Sons, inc., 1993
|
[11] |
Dix A, Finlay J, Abowd G, Beale R. Human-Computer Interaction. Upper Saddle River: Prentice Hall, 1993
|
[12] |
Paternò F, Mancini C, Meniconi S. Concurtasktrees: a diagrammatic notation for specifying task models. In: Proceedings of the IFIP TC13 Interantional Conference on Human-Computer Interaction. 1997, 362– 369
CrossRef
Google scholar
|
[13] |
Paternò F, Santoro C. Integrating model checking and HCI tools to help designers verify user interface properties. In: Palanque P, Paternò F, eds. Interactive Systems Design, Specification, and Verification. Lecture Notes in Computer Science, Vol 1946. Berlin: Springer, 2001, 135–150
CrossRef
Google scholar
|
[14] |
Scapin D, Pierret-Golbreich C. Towards a method for task description: MAD. Work with Display Units, 1989, 89: 371–380
|
[15] |
Scapin D, Bastien J. Analyse des tâches et aide ergonomique à la conception: l’approche mad*. Analyse et conception de l’IHM, 2001, 85–116
|
[16] |
Sybille C, Dominique S, Patrick G, Mickael B, Francis J. Increasing the expressive power of task analysis: systematic comparison and empirical assessment of tool-supported task models. Interacting with Computers, 2010
|
[17] |
Chebieb K, Mansour D, Ait-Ameur Y. Analyse et evaluation de propriétés dans les ihm. In: Proceedings of the 7th International Symposium on Programming and Systems. 2001, 241–252
|
[18] |
Ait Ameur Y, Kamel N. A generic formal specification of fusion of modalities in a multimodal HCI. Building the Information Society, 2004, 415–420
CrossRef
Google scholar
|
[19] |
Palanque P, Bastide R. Petri net based design of user-driven interfaces using the interactive cooperative objects formalism. In: Paternó F, eds. Design, Specification and Verification of Interactive Systems. Focus on Computer Graphics. Berlin: Springer, 1994, 383–400
|
[20] |
Navarre D, Palanque P, Ladry J F, Barboni E. ICOs: a model-based user interface description technique dedicated to interactive systems addressing usability, reliability and scalability. ACM Transactions on Computer-Human Interaction, 2009, 16(4): 18
CrossRef
Google scholar
|
[21] |
Paternò F, Mori G, Galiberti R. CTTE: an environment for analysis and development of task models of cooperative applications. In: Proceedings of CHI ’01 Extended Abstracts on Human Factors in Computing Systems. 2001, 21–22
CrossRef
Google scholar
|
[22] |
Ait Ameur Y, Baron M, Kamel N, Mota J M. Encoding a process algebra using the event B method: application to the validation of human-computer interactions. International Journal on Software Tools for Technology Transfer, 2009, 11(3): 239–253
CrossRef
Google scholar
|
[23] |
Mohand-Oussaïd L, Aït-Sadoune I, Aït-Ameur Y. Modelling information fission in output multi-modal interactive systems using event-B. In: Proceedings of the 1st International Conference on Model and Data Engineering. 2011, 200–213
CrossRef
Google scholar
|
[24] |
Duke D, Harrison M D. Event model of human-system interaction. IEEE Software Engineering Journal, 1995, 10(1): 3–10
CrossRef
Google scholar
|
[25] |
Brun P. XTL: a temporal logic for the formal development of interactive systems. Formal Methods for Human-Computer Interaction, 1997, 121–139
|
[26] |
D’Ausbourg B. Using model checking for the automatic validation of user interface systems. In: Proceedings of Eurographics Workshop on Design, Specification, and Verification of Interactive Systems. 1998, 242–260
CrossRef
Google scholar
|
[27] |
Ait Ameur Y, Kamel N. A generic formal specification of fusion of modalities in a multimodal HCI. In: Jacquart R, eds. IFIP World Computer Science. 2004, 415–420
CrossRef
Google scholar
|
[28] |
Milner R. A Calculus of Communicating Systems. Secaucus, NJ: Springer-Verlag New York, Inc., 1982
|
[29] |
Lotos I S O. A formal description technique based on the temporal ordering of observational behaviour. International Organisation for Standardization-Information Processing Systems—Open Systems Interconnection, Geneva, 1988
|
[30] |
Dictionary C. Cambridge Dictionaries Online, 2002
|
[31] |
Vanderdonckt J, Grolaux D, Van Roy P, Limbourg Q, Macq B, Michel B. A design space for context-sensitive user interfaces. In: Proceedings of IASSE, 2005, 207–214
|
[32] |
Johnson J A, Nardi B A, Zarmer C L, Miller J R. ACE: building interactive graphical applications. Communications of the ACM, 1993, 36(4): 40–55
CrossRef
Google scholar
|
[33] |
Kawai S, Aida H, Saito T. Designing interface toolkit with dynamic selectable modality. In: Proceedings of the 2nd Annual ACM Conference on Assistive Technologies. 1996, 72–79
CrossRef
Google scholar
|
[34] |
Crease M. A toolkit of resource-sensitive, multimodal widgets. University of Glasgow, 2001
|
[35] |
Bier E A, Stone M C, Pier K, Buxton W, DeRose T D. Toolglass and magic lenses: the see-through interface. In: Proceedings of the 20th Annual Conference on CGIT. 1993, 73–80
CrossRef
Google scholar
|
[36] |
Stuerzlinger W, Chapuis O, Phillips D, Roussel N. User interface façades: towards fully adaptable user interfaces. In: Proceedings of the 19th Annual ACM Symposium on User Interface Software and Technology. 2006, 309–318
CrossRef
Google scholar
|
[37] |
Demeure A, Calvary G, Coninx K. Comet(s), a software architecture style and an interactors toolkit for plastic user interfaces. In: Graham T, Palanque P, eds. Interactive Systems. Design, Specification, and Verification. Lecture Notes in Computer Sciences, Vol 5136. 2008, 225–237
CrossRef
Google scholar
|
[38] |
Jabarin B, Graham T C M. Architectures for widget-level plasticity. In: Proceedings of International Workshop on Interactive Systems. Design, Specification, and Verification of Interactive Systems. 2003, 451–460
CrossRef
Google scholar
|
[39] |
Stanciulescu A. Methodology for Developing Multimodal User Interfaces of Information Systems. Leuven: Presses univ. de Louvain, 2008
|
[40] |
Samaan K, Tarpin-Bernard F. The AMF architecture in a multiple user interface generation process. In: Proceedings of Developing User Interfaces with XML. 2004
|
[41] |
Dery-Pinna A M, Fierstone J, Picard E. Component model and programming: a first step to manage human computer interaction adaptation. In: Proceedings of International Conference on Human-Computer Interaction with Mobile Devices and Services. 2003, 456–460
CrossRef
Google scholar
|
[42] |
De Oliveira K M, Bacha F, Mnasser H, Abed M. Transportation ontology definition and application for the content personalization of user interfaces. Expert Systems with Applications, 2013, 40(8): 3145–3159
CrossRef
Google scholar
|
[43] |
Sonnenberg J. Service and user interface transfer from nomadic devices to car infotainment systems. In: Proceedings of the 2nd International Conference on Automotive User Interfaces and Interactive Vehicular Applications. 2010, 162–165
CrossRef
Google scholar
|
[44] |
Dees W. Usability of nomadic user interfaces. In: Jacko J, eds. Human- Computer Interaction. Towards Mobile and Intelligent Interaction Environments Lecture Notes in Computer Science, Vol 6763. Berlin: Springer, 2011, 195–204
CrossRef
Google scholar
|
[45] |
Masson D, Demeure A, Calvary G. Examples galleries generated by interactive genetic algorithms. In: Procedings of the 2nd Conference on Creativity and Innovation in Design. 2011, 61–71
CrossRef
Google scholar
|
[46] |
Pierre D, Marc D, Philippe R. Ubiquitous widgets: Designing interactions architecture for adaptive mobile applications. In: Proceedings of International Conference on Distributed Computing in Sensor Systems. 2013, 331–336
CrossRef
Google scholar
|
[47] |
Demeure A. Modèles et outils pour la conception et l’exécution d’Interfaces Homme-Machine Plastiques. Dissertation for the Doctoral Degree. Grenoble: Université Joseph Fourier, 2007
|
[48] |
Gruber T R. A translation approach to portable ontology specifications. Knowledge Acquisition, 1993, 5(2): 199–220
CrossRef
Google scholar
|
[49] |
Jean S, Pierra G, Ait Ameur Y. Domain ontologies: a database-oriented analysis. In: Filipe J, Cordeiro J, Pedrosa V, eds.Web Information Systems and Technologies. Lecture Notes in Business Information Processing, Vol 1. Berlin: Springer, 2007, 238–254
CrossRef
Google scholar
|
[50] |
Demeure A, Calvary G. Le modèle d’évolution en plasticité des interfaces: apport des graphes conceptuels. In: Actes de la 15ème conférence francophone IHM 2003. 2003, 80–87
|
[51] |
Rekimoto J. Pick-and-drop: a direct manipulation technique for multiple computer environments. In: Proceedings of the 10th Annual ACM Symposium on User Interface Software and Technology. 1997, 31–39
CrossRef
Google scholar
|
[52] |
Constantine L L. Canonical abstract prototypes for abstract visual and interaction design. In: Proceedings of International Workshop on Design, Specification, and Verification of Interactive Systems. 2003, 1–15
CrossRef
Google scholar
|
[53] |
Milner R. Communication and Concurrency. Upper Saddle River, NJ: Prentice-Hall, Inc., 1989
|
[54] |
Chebieb A, Ait-Ameur Y. Formal verification of plastic user interfaces exploiting domain ontologies. In: Proceedings of the 9th International Symposium on Theoretical Aspects of Software Engineering. 2015, 79–86
CrossRef
Google scholar
|
[55] |
Ait Ameur Y, Ait Sadoune I, Mota J M, Baron M. Validation et vérification formelles de systèmes interactifs multi-modaux fondées sur la preuve. In: Proceedings of the 18th International Conference of the Association Francophone d’Interaction Homme-Machine. 2006, 123–130
CrossRef
Google scholar
|
[56] |
Buxton W. A three-state model of graphical input. In: Proceeding of Human-Computer Interaction-INTERACT. 1990, 449–456
|
[57] |
Card S, Mackinlay J D, Robertson G. The design space of input devices. In: Proceedings of the ACM Conference on Human Factors in Computing Systems, Multi-Media. 1990, 117–124
CrossRef
Google scholar
|
[58] |
Frohlich D. The design space of interfaces. In: Proceeding of the 1st Eurographics Workshop on Multimedia Systems, Interaction and Applications. 1991
|
[59] |
Dragicevic P, Fekete J D. Support for input adaptability in the icon toolkit. In: Proceedings of the 6th International Conference on Multimodal Interfaces. 2004, 212–219
CrossRef
Google scholar
|
[60] |
CADP-Team. http://cadp.inria.fr, 2013
|
[61] |
Ait-Ameur Y, Chebieb A. A formal model to check systems substitutability: an application to interactive systems. Technical Report. 2013
|
[62] |
Clavel M, Duràn F, Eker S, Lincoln P, Martì-Oliet N, Meseguer J, Quesada J. Maude: specification and programming in rewriting logic. TheoreticalComputer Science, 2002, 285(2): 187–243
CrossRef
Google scholar
|
[63] |
Haarslev V, Möller R. Description of the RACER system and its applications. Description Logics, 2001, 49
|
[64] |
Bijan S E P. Pellet: an owl DL reasoner. In: Proceedings of International Workshop on Description Logics. 2004, 6–8
|
/
〈 | 〉 |