Browsing by Author "Mohand Oussaïd, Linda"
Now showing 1 - 7 of 7
Results Per Page
Sort Options
- ItemA formal model for output multimodal HCI(Springer Vienna, 2015-07) Mohand Oussaïd, Linda; Ait Sadoune, Idir; Ait Ameur, Yamine; Ahmed-Nacer, MohamedMultimodal human–computer interaction (HCI) combine modalities at an abstract specification level in order to get information from the user (input multimodality) and to return information to the user (output multimodality). These multimodal interfaces use two mechanisms: first, the fusion of information transmitted by the user on different modalities during input interaction and second, the fission or decomposition of information produced by the functional core in order to distribute the composite information on the different modalities during output interaction. In this paper, we present a generic approach to design output multimodal interfaces. This approach is based on a formal model, composed of two models: semantic fission model for information decomposition process and allocation model for modalities and media allocation to composite information. An Event-B formalization has been proposed for the fission model and for allocation model. This Event-B formalization extends the generic model and support the verification of some relevant properties such as safety or liveness. An example of collision freeness property verification is presented in this paper.
- ItemA generic formal model for fission of modalities in output multi-modal interactive systems(2009) Mohand Oussaïd, Linda; Ait Ameur, Yamine; Ahmed-Nacer, MohamedOutput multi-modal human-machine interfaces combine semantically output medias and modalities in order to increase interaction machine capabilities. The aim of this paper is to present a formal model supporting formal specifications of output multi-modal interactive systems. As a consequence, the expected usability and robustness properties can be expressed and checked. This paper proposes a generic model which permits to specify the output multimodal interfaces following the CASE design space.
- ItemFormal modelling of output multi-modal HCI in Event-B. Modalities and media allocation(CERIST, 2013-12-15) Mohand Oussaïd, Linda; Ait Sadoune, Idir; Ait Ameur, YamineMulti-modal Human-Computer Interfaces (HCI) allow interface designers to combine interactive modalities in order to increase interactive systems robustness and usability. In particular, output multi-modal interfaces allow the system to return the information to the user by using several modalities and media. In order to design such interfaces for critical systems, we proposed a generic formal model for the design of output multimodal interfaces. The proposed model consists of two successive models: the fission model that describes the semantic decomposition of information produced by the functional core into elementary information, and the allocation model that specifies the allocation of pairs modality/media for each elementary information. In a previous work (Mohand-Oussaid, Ait-Sadoune, and Ait-Ameur 2011), we have proposed an Event-B implementation of the fission model. In this paper, we present an Event-B implementation of the allocation model.
- ItemUn modèle formel générique de fission des modalités dans les systèmes multimodaux en sortie(CERIST, 2009-05) Mohand Oussaïd, LindaLes interfaces homme-machine multi-modales en sortie combinent sémantiquement les médias et modalités en sortie en vue d'accroître les capacités d'interaction de la machine. L'objectif de ce rapport est de présenter un modèle formel permettant la spécification formelle des systèmes interactifs multi-modaux en sortie. Ainsi, les propriétés d'utilisabilité et de robustesse peuvent être exprimées et vérifiées. Ce rapport propose en plus du modèle générique un modèle paramétré permettant la spécification des systèmes interactifs multimodaux en sortie selon l'espace de conception CASE.
- Itemmodélisation formelle d'IHM multi-modales en sortie avec B Evénementiel(CERIST, 23-04-2014) Mohand Oussaïd, Linda; Ait Sadoune, Idir; Ait Ameur, Yamine; Ahmed-Nacer, MohamedLes interfaces homme-machine (IHM) multi-modales offrent à l’utilisateur la possibilité de combiner les modalités d’interaction afin d’augmenter la robustesse et l’utilisabilité de l’interface utilisateur d’un système. Plus particulièrement, en sortie, les IHM multi-modales permettent au système de restituer à l’utilisateur, l’information produite par le noyau fonctionnel en combinant sémantiquement plusieurs modalités. Dans l’optique de concevoir de telles interfaces pour des systèmes critiques, nous avons proposé un modèle formel de conception des interfaces multi-modales en sortie. Le modèle proposé se décompose en deux modèles : le modèle de fission sémantique qui décrit la décomposition de l’information à restituer en informations élémentaires, et le modèle d’allocation qui spécifie l’allocation des modalités et médias aux informations élémentaires. Nous avons également développé une formalisation B Événementiel détaillée des deux modèles : fission sémantique et allocation. Cet article est dédié à la présentation d’une démarche formelle et générique relative au modèle proposé, il décrit la démarche générale de développement B Événementiel ainsi que le modèle générique B Événementiel correspondant au modèle de conception générique.
- ItemOntological Interaction Modeling and Semantic Rule-Based Reasoning for User Interface Adaptation(CERIST, 2016) Lebib, Fatma-Zohra; Mellah, Hakima; Mohand Oussaïd, LindaDisabled users conducting their interactive tasks on their devices address challenges such as user interface adaptation. The paper provides a valuable knowledge for supporting adaptive user interfaces. In this work an interactive application development, in handicrafts’ domain is considered, with the aim to build ontology which models the available interaction modalities and resources to be used by craftswomen interacting with the system. The paper is more focused on the Semantic Web Rule Language (SWRL) rules allowing to derive the appropriate modalities for specific woman considering different factors related to its sensory perception and motor skills to one finality that is enriching interaction ontology.
- ItemVérification formelle des propriétés de sécurité des logiciels(Institut National de Formation en Informatique (INI), 2006) Mohand Oussaïd, Linda; Ahmed-Nacer, MohamedCette thèse présente une démarche de vérification formelle des propriétés de sécurité des logiciels. En effet, après étude des approches possibles : preuve formelle et model checking, nous avons identifié le model checking comme étant l'approche la plus adéquate pour notre problématique. Ainsi, la démarche proposée est fondée sur une combinaison de la technique de model checking et des mécanismes : d'annotation et d'abstraction basés sur l'interprétation abstraite. Pour procéder au model checking, nous avons commencé par exprimer les propriétés de sécurité (confidentialité, intégrité, disponibilité) dans une logique temporelle appropriée. Ensuite, nous avons spécifié les systèmes auxquels pouvait s'appliquer notre démarche à savoir : les systèmes dont l'évolution peut être assimilée à un programme impératif réduit aux structures de contrôle de base. Moyennant deux étapes : la première qui enrichit le code source par des informations relatives à la propriété à vérifier et la deuxième qui débarrasse le code source enrichi des informations superflues à la vérification de la propriété de sécurité, nous avons transformé le code source d'un programme impératif en un programme abstrait qui exhibe les instructions concernées par les propriétés à vérifier tout en faisant abstraction du reste. L'annotation aussi bien que l'abstraction ont été développées par interprétation abstraite autour d'une correspondance de Galois qui assure que le programme abstrait correspond au programme initial. Cette démarche a été illustrée par un exemple qui consiste en un gestionnaire de transactions bancaires simplifié.