These: Driss Sadoun, Des specifications en langage naturel aux specifications formelles

[Thierry Hamon]

Date: Fri, 06 Jun 2014 16:45:17 +0200
From: sadoun <sadoun at limsi.fr>
Message-ID: <5391D3FD.2070307 at limsi.fr>

Bonjour,

J'ai le plaisir de vous inviter à ma soutenance de thèse intitulée /"Des
spécifications en langage naturel aux spécifications formelles via une
ontologie comme modèle pivot" /ainsi qu'au pot qui suivra.


*Date et heure* : Mercredi 17 juin 2014, à 14h

*Lieu* :   LIMSI-CNRS,
           Bâtiments /S/
           Rue John von Neumann
           Université Paris-Sud
           91403 ORSAY (France)
           en salle de conférence.

*Le jury est constitué de :*

*Co-directeurs* :

Mme Brigitte Grau Professeur (LIMSI-CNRS - ENSIIE)
Mme Catherine Dubois Professeur (CEDRIC-CNAM - ENSIIE)
M. Yacine Ghamri-Doudane Professeur (Université de La Rochelle)

*Rapporteurs* :
M. François Lévy Professeur (LIPN - Université Paris 13)
M. Yamine Ait-Ameur Professeur (IRIT-ENSEEIHT)

*Examinateurs* :
Mme Chantal Reynaud Professeur (LRI - Université Paris-Sud)
M. Yannick Toussaint CR HDR (LORIA-INRIA)

*Résumé *:


Le développement d'un système a pour objectif de répondre à des
exigences. Aussi, le succès de sa réalisation repose en grande partie
sur la phase de spécification des exigences qui a pour vocation de
décrire de manière précise et non ambiguë toutes les caractéristiques du
système à développer. Les spécifications d'exigences sont le résultat
d'une analyse des besoins faisant intervenir différentes parties. Elles
sont généralement rédigées en langage naturel (LN) pour une plus large
compréhension, ce qui peut mener à diverses interprétations, car les
textes en LN peuvent contenir des ambiguïtés sémantiques ou des
informations implicites. Il n'est donc pas aisé de spécifier un ensemble
complet et cohérent d'exigences. D'où la nécessité d'une vérification
formelle des spécifications résultats. Les spécifications LN ne sont pas
considérées comme formelles et ne permettent pas l'application directe
de méthodes vérification formelles. Ce constat mène à la nécessité de
transformer les spécifications LN en spécifications formelles. C'est
dans ce contexte que s'inscrit cette thèse. La difficulté principale
d'une telle transformation réside dans l'ampleur du fossé entre
spécifications LN et spécifications formelles.

L'objectif de mon travail de thèse est de proposer une approche
permettant de vérifier automatiquement des spécifications d'exigences
utilisateur, écrites en langage naturel et décrivant le comportement
d'un système.
Pour cela, nous avons exploré les possibilités offertes par un modèle de
représentation fondé sur un formalisme logique.
Nos contributions portent essentiellement sur trois propositions :

1) une ontologie en /OWL-DL/ fondée sur les logiques de description,
   comme modèle de représentation pivot permettant de faire le lien
   entre spécifications en langage naturel et spécifications formelles;
2) une approche d'instanciation du modèle de représentation pivot,
   fondée sur une analyse dirigée par la sémantique de l'ontologie,
   permettant de passer automatiquement des spécifications en langage
   naturel à leur représentation conceptuelle;
et 3) une approche exploitant le formalisme logique de l'ontologie, pour
   permettre un passage automatique du modèle de représentation pivot
   vers un langage de spécifications formelles nommé /Maude/.

*Abstract:*

The main objective of system development is to address requirements. As
such, success in its realisation is highly dependent on a requirement
specification phase which aims to describe precisely and unambiguously
all the characteristics of the system that should be developed. In order
to arrive at a set of requirements, a user needs analysis is carried out
which involves different parties (stakeholders). The system requirements
are generally written in natural language to garantuee a wider
understanding. However, since NL texts can contain semantic ambiguities,
implicit information, or other inconsistenties, this can lead to diverse
interpretations. Hence, it is not easy to specify a set of complete and
consistent requirements, and therefore, the specified requirements must
be formally checked. Specifications written in NL are not considered to
be formal and do not allow for a direct application of formal methods.
We must therefore transform NL requirements into formal specifications.
The work presented in this thesis was carried out in this framework. The
main difficulty of such transformation is the gap between NL
requirements and formal specifications.

The objective of this work is to propose an approach for an automatic
verification of user requirements which are written in natural language
and describe a system's expected behaviour. Our approach uses the
potential offered by a representation model based on a logical
formalism.

Our contribution has three main aspects:
1) an /OWL-DL/ontology based on description logic, used as a pivot
   representation model that serves as a link between NL requirements to
   formal specifications;
2) an approach for the instantiation of the pivot ontology, which allows
   an automatic transformation of NL requirements to their conceptual
   representations;
and 3) an approach exploiting the logical formalism of the ontology in
   order to automatically translate the ontology into a formal
   specification language called /Maude/.


-------------------------------------------------------------------------
Message diffuse par la liste Langage Naturel <LN at cines.fr>
Informations, abonnement : http://www.atala.org/article.php3?id_article=48
English version       : 
Archives                 : http://listserv.linguistlist.org/archives/ln.html
                                http://liste.cines.fr/info/ln

La liste LN est parrainee par l'ATALA (Association pour le Traitement
Automatique des Langues)
Information et adhesion  : http://www.atala.org/

ATALA décline toute responsabilité concernant le contenu des
messages diffusés sur la liste LN
-------------------------------------------------------------------------