Application de théories d’interfaces sur des documents de spécification

Approches basées sur le formalisme cible

   Une première orientation consiste à s’appuyer sur le formalisme cible, par exemple la logique temporelle. Le but recherché, en suivant cet axe, est d’ajouter une interface pour faciliter l’expression de propriétés à vérifier à l’aide d’une représentation se rapprochant d’un langage naturel. Les patterns de spécification [18, 19] ont été conçus dans cette optique. Dotés de correspondances avec différents formalismes, ils définissent un ensemble d’abstractions paramétrables, plus facile à appréhender car basé sur le langage naturel. Les schémas proposés autorisent ainsi la spécification de propriétés critiques, telles que la restriction d’occurrences de certains événements ou l’interdiction d’une propriété dans des situations données. De ce fait, ils apportent un support pour un ensemble de techniques permettant de prouver des propriétés sur des modélisations de systèmes. Les patterns de spécification peuvent être associés à différentes représentations, par exemple les systèmes de transitions à états finis, les systèmes temporisés ou les systèmes hybrides. Des correspondances sont notamment apportées pour les logiques temporelles LTL 4[20], CTL 5 [2] et les expressions régulières quantifiées QRE 6[21]. De fait, un système de patterns est un ensemble de schémas. Ceux-ci peuvent être regroupés en fonction du formalisme de spécification, par exemple LTL ou CTL. Il est également possible d’avoir une hiérarchie selon le type de comportement décrit. Dans cette classification, les modèles d’occurrence (Occurrence Patterns) caractérisent un événement pendant l’exécution du système, tandis que les modèles d’ordonnancement (Order Patterns) concernent l’ordre relatif dans lequel plusieurs événements se produisent. Précisément, un pattern est une description structurée d’un comportement de système. Il se caractérise par un nom, un énoncé précis de son but (le type de comportement décrit) et une portée (scope). Il est également associé à des transcriptions dans quelques formalismes de spécification et à des exemples d’utilisation. Par exemple, le pattern Response autorise la description d’une relation de cause à effet entre une paire d’événements, avec une certaine portée. La portée permet de situer le comportement décrit globalement, avant ou après un autre évènement ou en fonction de l’occurrence de deux autres événements. Une approche analogue est proposée pour la spécification de systèmes en temps réel [22]. Associée à cette méthode, une grammaire anglaise structurée a été développée pour faciliter l’usage des patterns de spécification. Elle prend en charge des modèles avec plusieurs champs d’application, qualitatif (par exemple l’absence, la globalité ou l’enchaînement d’événements) et quantitatif (incluant des informations sur le temps). Les modèles de spécification proposés peuvent être reliés à plusieurs logiques temporelles en temps réel, telles que la logique temporelle métrique MTL 7 [23] ou la logique d’arbres de calcul temporisé TCTL 8 [24]. L’usage d’un langage naturel contrôlé, tel que le langage ACE 9 [25], peut également être envisagé. La structure des phrases y est contrainte avec des règles de construction et d’interprétation, tout en restant très proche de l’anglais courant. Associé à un moteur d’analyse, l’APE10, il permet de générer des représentations sémantiques sous la forme de structures de représentation du discours (DRS 11) [26] et d’expressions logiques du premier ordre. Par extension, les DRS peuvent ensuite être traduites dans diverses représentations telles que OWL 12 [27], SWRL 13 [28] ou RuleML [29]. Le contrôle du langage par des processus automatiques est renforcé, au prix d’une perte d’expressivité et d’un temps d’apprentissage. Si les méthodologies construites autour de ces langages ne permettent pas d’analyser directement des énoncés exprimés en langue naturelle, elles offrent néanmoins la possibilité de construire efficacement des éléments d’interfaces entre les documents de spécification et leurs modélisations.

Transformation sémantique de la représentation pivot

   L’étape suivante consiste à traiter ces représentations pour les classer et les transformer. Le problème se pose donc en termes différents : ce n’est plus un énoncé du langage naturel qui est traité, mais une représentation formelle de cet énoncé qu’il s’agit d’interpréter. Nous proposons une méthodologie que nous nommons transduction sémantique. Le principe général est d’appliquer une série de transformations à partir du graphe AMR tout en respectant certaines conditions. Ces conditions prennent la forme de formules logiques traduisant les critères d’application des transformations. Ces dernières consistent en l’application d’opérations qui enrichissent l’interprétation du graphe. Elles permettent de construire des regroupements de nœuds. Associés à de nouveaux concepts, ces ensembles forment, en un certain sens, des abstractions sur différentes parties du graphe. Les formules logiques et les opérations sont associées dans des schémas que nous appelons schéma de transduction compositionnel (STC). Ces schémas définissent des règles s’appliquant à une interprétation logique de base pour aboutir à une interprétation enrichie, où apparaissent des concepts abstraits. L’un de ces concepts correspond au résultat attendu. Sa présence permet d’obtenir la formalisation attendue, tandis que son absence entraîne le rejet de l’énoncé (qui ne correspond pas à la cible). L’analyse du graphe sémantique de l’énoncé E1 part d’une interprétation brute initiale, constituée d’ensembles formés autour de chaque sommet du graphe. Cette interprétation est enrichie par application successive de règles dites de transduction. Elles permettent d’aboutir à une représentation de plus haut niveau correspondant à la formalisation attendue en sortie

Discourse Representation Theory (DRT)

   La théorie de la représentation du discours de Kamp (DRT , [42, 26]) fournit un premier cadre d’exploration du sens selon une approche sémantique formelle. Elle inclut un niveau de représentations mentales abstraites, appelé structure de représentation du discours (DRS ). Cet élément est central pour la DRT. Elle permet de refléter la dépendance du sens par rapport au contexte, et confère à la DRT une capacité intrinsèque à traiter le sens au-delà des limites de la phrase. Une DRS est un objet mathématique qui comporte deux éléments essentiels : un ensemble de référents discursifs représentant des entités, et un ensemble de conditions représentant des concepts liés aux référents. Les conditions peuvent être atomiques ou complexes. La DRS consiste en un prédicat dans le premier cas, avec un nombre approprié de référents discursifs. Les DRS peuvent être combinées par fusion pour produire des conditions complexes.Ce principe se reflète dans la construction et l’enrichissement des DRS. Nous reprenons l’exemple classique des phrases “donkey”, initialement proposées par le philosophe Peter Geach en 1962 [69]. Ces phrases ont constitué un cadre d’étude important pour différentes théories, dont la DRT. L’énoncé “Every farmer who owns a donkey beats it” peut être représenté par la DRS [x, y : f armer(x), donkey(y), owns(x, y)] ⇒ [beat(x, y)]. Cette structure intègre deux DRS : [x, y : f armer(x), donkey(y), owns(x, y)] et [beat(x, y)], qui contiennent deux référentiels discursifs (x et y), et quatre conditions (farmer, donkey, own et beat). La DRT est une théorie de la sémantique dynamique. Elle est fondée sur l’idée que la signification réalise, au fil du discours, des modifications successives du contexte discursif. Le lien entre l’interprétation et le contexte y est dual : l’interprétation dépend du contexte tout en créant celui-ci. Cette dualité se traduit par l’imbrication des DRS. Le langage de représentation de la DRT consiste en une définition récursive de l’ensemble des DRS bien formées. Un modèle sémantique théorique est associé aux éléments de cet ensemble. Ce modèle intègre une procédure de construction qui précise comment étendre une DRS donnée à chaque analyse d’une nouvelle phrase. Proposée au début des années 80, la théorie de la représentation du discours a été développée dans le but de soutenir l’inférence logique dans les systèmes de traitement basés sur le raisonnement logique. Elle constitue ainsi un cadre de représentation assez ancien, mis en œuvre dans différents projets [70, 71]. Les systèmes exploitant les DRS nécessitent, en complément, une représentation appropriée des composantes sémantiques.

Spécification informelle du système

   Le cas d’étude définit un système relativement classique de contrôle d’accès pour un garage de voitures [4]. Le système est composé de plusieurs entités. Les barrières de sécurité permettent de contrôler les entrées et sorties du parking. La capacité maximale est fixée. Un ticket est fourni en entrée. Ce ticket autorise la sortie après paiement. La section Gate intègre les exigences qui caractérisent le comportement des barrières d’accès au parking. Ces exigences peuvent être instanciées pour chaque barrière (en entrée ou sortie). La section Payment précise le comportement de la machine de paiement. Finalement, la section Supervisor rassemble les exigences se rapportant à l’ensemble du système. Ce système a été étudié en détail, du point de vue ingénierie des exigences, dans le livre Contract for System Design [4].  Elles sont exprimées avec un langage naturel, à savoir l’anglais. Il n’y a aucune contrainte particulière sur la forme de l’énoncé. L’objectif fixé est l’interprétation automatique de ces énoncés, c’est à dire la construction d’une certaine structure formelle. Le but est de démontrer formellement la consistance, ou l’inconsistance, de cet ensemble. En cas d’inconsistance, il s’agit de mettre en évidence les exigences contradictoires. Ces exigences contiennent plusieurs caractéristiques linguistiques qui doivent être prises en compte. Elles peuvent décrire des enchaînements d’événements, avec des modalités temporelles (after, before).  Les spécifications contiennent aussi des modalités d’obligation et d’interdiction (may, must, cannot). L’extraction des informations nécessaires pour le passage vers une spécification formelle implique une bonne évaluation de ces différents aspects.

Table des matières

1 Introduction 
2 Assistance à la conception de systèmes 
2.1 Contexte 
2.2 Formalisation des exigences 
2.2.1 Approches basées sur le formalisme cible
2.2.2 Approches basées sur une décomposition des énoncés
2.2.3 Approches basées sur une structure pivot
2.3 Traitement complet
2.3.1 Prétraitements des documents
2.3.2 Analyse syntaxico-sémantique des énoncés
2.3.3 Transformation sémantique de la représentation pivot
2.3.4 Modélisation
3 Représentations sémantiques pour capturer le sens des énoncés 
3.1 État de l’art 
3.1.1 Discourse Representation Theory (DRT)
3.1.2 Abstract Meaning Representation (AMR)
3.1.3 Prague Dependency Treebank (PDT-TL)
3.1.4 Universal Conceptual Cognitive Annotation (UCCA)
3.2 Représentation de sens abstrait 
3.2.1 Structure des graphes AMR
3.2.2 Analyse syntaxico-sémantique
3.3 Discussion
4 Principes d’analyse par transduction sémantique 
4.1 Modèle sémantique
4.1.1 Graphe sémantique élémentaire
4.1.2 Filets sémantiques
4.2 Opération de transduction 
4.2.1 Requête logique
4.2.2 Opérateur de transduction
4.2.3 Schéma de transduction compositionnel (STC)
4.3 Algorithme d’analyse sémantique
4.4 Expérimentation
4.4.1 Implémentation
4.4.2 Paramétrage
4.4.3 Évaluation
5 Vers une théorie d’interface prenant en compte les propriétés d’états
5.1 Modélisation de systèmes
5.1.1 Syntaxe
5.1.2 Sémantique
5.1.3 Produit de modèles
5.2 Algèbre de composition
5.2.1 Consistance et relation de satisfaction
5.2.2 Relation de raffinement
5.2.3 Conjonction
5.2.4 Composition parallèle
5.2.5 Quotient
5.3 Spécifications 
5.3.1 Spécifications modales
5.3.2 Structure de spécification pour les modèles de Kripke
5.3.3 Complément
6 Ensembles d’acceptation 
6.1 Définition 
6.2 Algèbre des ensembles d’acceptation 
6.2.1 Algèbre des AS homogènes
6.2.2 Algèbre des AS hétérogènes
6.3 Représentation implicite
7 Automates moniteurs 
7.1 Définition
7.2 Configuration, observation et langage support
7.3 Relation de satisfaction
7.4 Quelques opérations de transformation 
7.4.1 Réduction
7.4.2 Complétion
7.4.3 Déterminisation
7.5 Relation de raffinement
7.6 Algèbre de composition 
7.7 Discussion
8 Automates déterministes à ensembles d’acceptation propositionnels
8.1 Syntaxe
8.2 Relation de satisfaction 
8.3 Relation de raffinement 
8.4 Algèbre de composition 
8.4.1 Conjonction
8.4.2 Produit
8.4.3 Quotient
9 Systèmes étudiés de bout en bout 
9.1 Système de contrôle d’accès d’un garage de voitures 
9.2 Procédure de manipulation d’un jeu de poupées russes 
10 Conclusion

Télécharger le rapport complet