Représentation et vérification d’un environnement intelligent à partir de spécifications utilisateur en langage naturel

International audienceAujourd'hui des capteurs et actionneurs associés à des périphériques de contrôle peuvent être installés n'importe où, notamment dans nos maisons, créant des environnements intelligents. Notre objectif est de permettre à un utilisateur de configurer son propre environne-ment intelligent en décrivant ses besoins, i.e. les règles de comportement de l'environnement, en langage naturel (LN). Nous explorons les possibilités offertes par une ontologie formelle pour faire le lien entre spécifications en LN et spécifications formelles. L'analyse des spécifications LN permet l'instanciation automatique de l'ontologie afin qu'elle représente le comportement décrit par l'utilisateur. Les règles de comportement représentées sont alors traduites en spécifi-cations Maude, afin de compléter les vérifications possibles sous OWL. Nous montrons que tout au long de ce processus de formalisation, il est possible de vérifier la complétude, la cohérence et la conformité des exigences spécifiées et de maintenir une traçabilité entre spécification LN et spécifications formelles autorisant un retour précis à l'utilisateur. ABSTRACT. Nowadays sensors and actuators associated with control devices can be installed anywhere, as in our homes creating smart environments. Our goal is to allow a user to configure her own smart environment by describing her needs, i.e. the environment behavioral rules, in natural language (NL). We explore the possibilities offered by an ontology, to transform NL specifications into formal specifications. Analysis of user requirements allows us an automatic instantiation of the ontology so that it represents the behavior described by the user. The represented behavioral rules are then translated into Maude specifications to complement ve-rifications realized in OWL. We show that throughout this formalization process, it is possible to check the completeness, the consistency and the conformity of the specified requirements and maintain traceability between NL requirements and formal specifications to allow a precise feedback to the user. MOTS-CLÉS : environnement intelligent, ontologie, spécifications, vérification formelle