Analyse formelle d’exigences en langue naturelle pour la conception de systèmes cyber-physiques (Formal analysis of natural language requirements for the design of cyber-physical systems ) (2018)

Abstract: Cet article explore la construction de représentations formelles d’énoncés en langue naturelle. Le passage d’un langage naturel à une représentation logique est réalisé avec un formalisme grammatical, reliant l’analyse syntaxique de l’énoncé à une représentation sémantique. Nous ciblons l’aspect comportemental des cahiers des charges pour les systèmes cyber-physiques, c’est-à-dire tout type de systèmes dans lesquels des composants logiciels interagissent étroitement avec un environnement physique. Dans ce cadre, l’enjeu serait d’apporter une aide au concepteur. Il s’agit de permettre de simuler et vérifier, par des méthodes automatiques ou assistées, des cahiers des charges “systèmes” exprimés en langue naturelle. Cet article présente des solutions existantes qui pourraient être combinées en vue de la résolution de la problématique exposée.

## introduction l'objectif de cet article est de proposer les éléments d'une méthodologie permettant de transformer certains fragments de cahiers des charges, exprimés en langue naturelle, en spécifications formelles, vérifiables et exécutables. notre cadre applicatif porte sur les systèmes cyber-physiques, où des éléments informatiques sont conçus en interaction avec des entités physiques. nous pouvons donner de nombreux exemples de systèmes cyber-physiques : un avion, une centrale électrique, un réseau ferroviaire, etc. ## analyse d'exigence l'approche que nous proposons vise à construire une représentation logique d'un énoncé en "capturant" finement sa sémantique. suivant les travaux de montague @xcite , nous considérons le sens d'une phrase comme lié à sa construction syntaxique. nous partons d'une décomposition de l'énoncé à l'aide d'un formalisme grammatical, pour ainsi définir le comportement syntaxique de l'énoncé cible. l'idée est ensuite de relier cette décomposition à une représentation formelle. comme indiqué en introduction, nous proposons d'utiliser les grammaires catégorielles, un formalisme de haut-niveau pour l'analyse de textes. les grammaires catégorielles ont pris forme dans les années 50 et 60, à partir des travaux de adjukiewicz @xcite , @xcite et @xcite . elles reposent sur la notion de catégories primitives et de catégories dérivées (on parle aussi de types). elles offrent la possibilité de décomposer une phrase en catégories, les catégories composées mettant en évidence les liens syntaxiques du langage ciblé. les grammaires catégorielles intègrent également des règles de dérivation qui permettent de combiner les éléments d'une phrase. du point de vue de la théorie grammaticale, il est important de considérer l'expressivité des formalismes étudiés. pour les grammaires catégorielles classiques, elle est équivalente aux grammaires non-contextuelles @xcite . plusieurs extensions ont donc été proposées pour dépasser cette contrainte, dont la grammaire catégorielle combinatoire (ccg), introduite par mark steedman en 1989 @xcite . ce formalisme utilise un ensemble d'opérateurs pour saisir d'autres aspects linguistiques. dans cette grammaire, la sémantique des mots est guidée tout au long de l'arbre de dérivation en combinant les sémantiques des autres mots jusqu'à produire la sémantique complète de la phrase, à la montague @xcite . elle est particulièrement intéressante dans notre cas c atala 2018 pour ses liens avec le lambda-calcul, qui pourrait être une représentation formelle intermédiaire avant d'aboutir à d'autres représentations logiques. concrètement, les grammaires ccg permettent de relier la syntaxe des énoncés étudiés à leur représentation sémantique sous-jacente. elles se définissent avec un ensemble de catégories basiques, un ensemble de catégories dérivées, des règles de calcul syntaxiques et un lexique de mots. les catégories primitives correspondent aux catégories syntaxiques habituellement utilisées dans les grammaires traditionnelles. cet ensemble de catégories primitives n'est pas universel mais fait partie de la définition de la grammaire. il est possible de se restreindre à deux catégories : s pour la phrase ("sentence" en anglais), n pour les noms communs et les noms propres. il est également possible d'étendre cet ensemble en ajoutant des catégories, par exemple pour les adjectifs ou les pronoms. de même, la grammaire peut-être raffiner avec des sous-catégories, comme sur la figure 2. les catégories dérivées sont construites à partir des catégories primitives. elles peuvent se définir récursivement avec les règles syntaxiques : soit x et y deux catégories, alors x/y et x\y sont également des catégories 1 . les règles syntaxiques permettent de produire l'analyse sémantique en combinant les entrées lexicales. les grammaires catégorielles classiques proposent deux règles de calcul, également présentes avec les ccg : l'application en avant ( > ) et l'application en arrière ( < ). chacune de ces règles permet de former une nouvelle catégorie en combinant une catégorie de type x/y ou x\y avec une catégorie de type y . formellement, elles peuvent se définir comme suit : les ccg enrichissent les grammaires catégorielles classiques avec de nouvelles règles de calcul. nous définissons ici les règles de composition harmoniques, en avant ( @xmath0: d'autres règles sont également proposées : des règles de compositions croisées, des règles de composition mixtes et des règles de changement de types. l'ensemble de ces règles offre différentes façons de combiner les catégories, et introduisent un certain degré d'associativité. elle permettent ainsi de traiter des aspects linguistiques plus riches. finalement, le lexique permet de définir la grammaire qui correspond à un langage donné. il est constitué d'un ensemble d'entrées lexicales associant un mot et un ensemble de types, auxquelles il est possible d'adjoindre une représentation sémantique. cette dernière peut être donnée sous la forme d'expressions en lambda-calcul 2 . par exemple, le mot "gate" pourra être associé à la catégorie n, tandis que la modalité "may" serait associée à la catégorie (s\n p )/(s\n p ). ces deux entrées les spécifications modales @xcite représentent le compromis recherché. en effet, correspondant aux systèmes de transitions modaux déterministes @xcite , ce formalisme intègre les opérations de conjonction, de composition et de quotient avec une complexité algorithmique polynomiale. il est donc adapté pour la représentation d'interfaces des différents composants d'un système. certes, les spécifications modales sont strictement moins expressives que le µ-calcul modal . cette limitation est néanmoins acceptable pour formaliser les propriétés de sureté des cahiers des charges de systèmes cyber-physiques. ce formalisme permet de représenter des automates dont les transitions sont typées avec les modalités must et may, permettant de définir un ensemble de modèles. de manière informelle, une transition de type must ( obligatoire) doit être présente dans chaque composant qui implémente la spécification modale, alors qu'une transition de type may ( facultative) peut ne pas l'être. les spécifications modales sont des systèmes de transitions modaux déterministes @xcite . les systèmes de transitions modaux ont été introduits par larsen et thomsen dans les années 80 @xcite pour étudier le raffinement d'actions, opération qui consiste à remplacer des transitions pour relier les descriptions d'un système à différents niveaux d'abstraction. nous reprenons la définition formelle de j.-b. raclet @xcite . une spécification modale est un tuple @xmath1, q 0 , σ, ∆ m , ∆ m ). q est un ensemble fini d'états. q 0 est l'unique état initial. σ est un ensemble fini d'actions. ∆ m ⊆ q × σ × q est l'ensemble déterministe des transitions facultatives ; ∆ m ⊆ q × σ × q est l'ensemble déterministe des transitions obligatoires. enfin, la condition de consistance suivante doit être respectée : ∆ m ⊆ ∆ m et q 0 ∈ q. cette condition signifie que chaque transition obligatoire (appartenant à l'ensemble ∆ m ) est également une transition facultative (appartenant à l'ensemble ∆ m ). le modèle d'une spécification modale est défini à partir de la relation de satisfaction, notée |=. la figure 3 montre une spécification modale (à gauche) et deux modèles possibles de cette spécification (à droite), où a et b sont deux actions (ou évènements). les spécifications modales sont dotées de propriétés algébriques particulièrement intéressantes. ces propriétés sont détaillées dans @xcite . on y trouvera en particulier les définitions formelles (et preuves associées) pour la composition (s 1 ⊗ s 2 ), la conjonction (s 1 ∧ s 2 ) et le quotient (s 1 /s 2 ) de spécifications modales (avec s 1 et s 2 deux spécifications modales). nous précisons ici quelques points importants : la notion de raffinement, et les caractéristiques algébriques des opérations évoquées. une spécification modale s 1 est le raffinement d'une spécic atala 2018 figure 3 -une spécification modale et deux modèles possibles fication s 2 si, et seulement si, les modèles de s 1 sont aussi des modèles de s 2 . formellement, le raffinement, noté , se définit comme suit : s 1 s 2 si, et seulement si, pour tout modèle m , nous avons m |= s 1 ⇒ m |= s 2 . nous pouvons dès lors donner les caractéristiques algébriques des opérations de composition, conjonction et quotient, en nous appuyant sur le raffinement : les spécifications modales apparaissent comme un formalisme pertinent pour la représentation des exigences d'un système réactif. elles peuvent prendre la forme d'automates qu'il est possible d'exécuter pour valider un cahier des charges. de plus, elles sont implémentables avec une complexité raisonnable, et permettent de représenter les modalités déontiques et temporelles présentes dans la définition d'un système. ## travaux préliminaires nous proposons de montrer une mise en oeuvre possible des concepts exposés dans les sections précédentes sur un cas d'étude. l'objectif visé est la construction de la spécification modale d'un système dont le comportement est décrit en langue naturelle. pour atteindre ce but, nous présentons une méthode de traitement sur un ensemble d'exigences. celle-ci doit permettre de relier les dérivations syntaxiques de ces exigences à des représentations sémantiques pertinentes. l'exemple présenté ici repose sur des expérimentations préliminaires @xcite portant sur un système représentant un garage de voitures @xcite . la figure 4 propose une vue d'ensemble du document de spécifications, composé de plusieurs sections (gate, payment, supervisor). pour ces travaux préliminaires, les données utilisées proviennent d'un cas d'étude théorique. de plus, les exigences exprimées en plusieurs phrases, avec des formulations imposant la prise en compte du contexte, ont été mises de côté. chaque exigence est donc définie en une phrase et sans pronom, c atala 2018 chaque entité devant être explicitement désignée dans l'exigence 4 . les représentations sémantiques sont obtenues à partir de dérivations ccg, comme définies section 2. concrètement, chaque élément lexical est associé à une catégorie lexicale et une représentation sémantique exprimée en lambda-calcul. il est également possible de donner plusieurs représentations pour un même élément lexical (dans le cas où l'élément lexical serait associé à plusieurs catégories syntaxiques). le traitement implique ensuite de déterminer les fonctions et les arguments, et d'appliquer récursivement les fonctions sur les arguments jusqu'à obtenir la représentation sémantique complète de l'exigence ciblée. le passage des formules en lambda-calcul vers les spécifications modales comporte plusieurs difficultés, dont la mise en relation des termes de l'énoncé (source) aux états et actions de la spécification (cible). au niveau de l'implémentation, un module spécifique pourrait permettre de gérer cette transformation. ce module doit également intégrer la résolution des références aux concepts, par exemple en s'appuyant sur une ontologie du domaine d'étude. un automate peut être spécifié sous la forme d'une expression régulière, dont la définition peut prendre en compte les opérateurs algébriques tels que la concaténation, le choix, la répétition ou le mot vide. des règles de transformation associant une expression régulière à chaque terme en langue naturelle peuvent être proposées en s'appuyant sur cette définition. l'application de ces règles permet de décrire les propriétés d'états en expression régulière. sur le même principe, nous pouvons associer des transitions aux termes en langue naturelle définissant des modalités. la combinaison de ces relations permet de construire la représentation des états et transitions sous la forme d'une spécification modale, à partir de l'arbre de dérivation ccg. directement les exigences exprimées en langue naturelle. dans le tableau 1, nous reprenons quelques exigences portant sur la section "gate". id. exigence 1 entry gate must open once a ticket has been issued. 2 when a ticket has been issued, entry gate must open. 3 when a ticket has been issued, entry gate opening is obligatory. 4 afer an exit ticket is inserted, exit gate must open. l'outil boxer, développé par johan bos @xcite , a été utilisé pour traiter les exigences et construire des représentations sémantiques. boxer/c&c est un analyseur sémantique de textes en anglais. il s'appuie sur la grammaire catégorielle combinatoire et la théorie de représentation du discours @xcite , et permet de construire des représentations sémantiques sous différentes formes. la figure 5 donne une représentation de l'exigence 4 du tableau 1. figure 5 -représentation graphique de l'analyse sémantique pour l'exigence 4 le lien entre boxer et mica n'a pas encore été réalisé. sur le principe, il s'agit de générer du code o'caml à partir des représentations formelles obtenues. la figure 6 donne une vue du résultat que nous pourrions obtenir sous la forme d'une spécification modale en prenant en compte les exigences de la section "gate". cette représentation intègre l'analyse de l'exigence 4 (figure 5 ). on retrouve cette propriété au niveau des états 0 et 1. même s'il est incomplet, le résultat obtenu montre la pertinence de l'approche. il serait souhaitable de développer un outil complet permettant l'implémentation d'interfaces modales pour des composants spécifiés en langue naturelle. sa réalisation pourrait s'appuyer sur les outils présentés, boxer pour la dérivation ccg, et mica pour les interfaces modales, ou d'autres outils aux caractéristiques similaires. pour valider cette démarche, il conviendrait également d'évaluer l'approche sur l'ensemble des exigences du cas d'étude, ainsi que sur des données issues d'un cas réel. a contrario, l'approche que nous proposons vise à construire automatiquement les représentations formelles à partir d'énoncés exprimés en langue naturelle. même si l'écriture des énoncés devra être d'abord restreinte à un langage contrôlé, notre objectif est de permettre de dépasser cette contrainte et rejoindre dans une certaine mesure la flexibilité du langage naturel. pour atteindre notre objectif, plusieurs étapes sont nécessaires. la première étape consiste en la dérivation d'une analyse syntaxique de l'énoncé, pour aboutir à un arbre syntaxique. la deuxième étape vise à relier l'analyse syntaxique à une représentation formelle intermédiaire, par exemple le lambda-calcul. nous pensons possible de passer de cette représentation à une autre forme. nous avons notamment montré l'intérêt des spécifications modales pour la vérification d'un cahier des charges. concernant le passage de la langue naturelle vers une représentation formelle, nous avons évoqué une première piste, à savoir l'utilisation des ccg, couplée aux drt si nous voulons traiter les pronoms. d'autres options sont également envisageables et pourraient être étudiées. nous pensons notamment aux travaux autour du "grammatical framework" foot_2 , également fondé sur les grammaires catégorielles et la théorie des types. nous songeons aussi aux grammaires catégorielles abstraites (de groote, 2001), formalisme qui généralise les grammaires catégorielles en traitant directement les catégories et le lambda-calcul. nous avons évoqué la théorie de représentation du discours (drt), proposé par hans @xcite . ce modèle permet de construire une représentation d'un texte en examinant le contenu sémantique dépendant du contexte. il permet ainsi de traiter certaines difficultés linguistiques, en particulier les mots grammaticaux se substituant à un élément donné (pronoms). a la base de la drt, il y a l'idée que l'interprétation d'un discours s'appuie sur une représentation sémantique, chaque phrase enrichissant cette représentation. cette représentation est appelée "structure de représentation du discours" (drs). la drt intègre également une procédure de construction, pour mettre à jour la représentation à chaque nouvelle phrase, et un ensemble de modèle sémantique, pour évaluer les drs. ce formalisme pourrait être exploité conjointement aux ccg pour augmenter la couverture des phénomènes linguistiques. la validation de la méthodologie proposée passe par une mise en oeuvre concrète. une première étape serait de développer un prototype visant l'implémentation de spécifications modales à partir d'exigences exprimées dans un langage contraint, le plus proche possible de la langue naturelle. dans un second temps, il s'agirait de lever les contraintes sur le texte pour se rapprocher au maximum de la flexibilité de la langue naturelle. de nombreuses questions se posent alors, en particulier pour le traitement des énoncés ambigus. l'interaction entre le programme et l'utilisateur est une première réponse. nous pourrions imaginer que le système propose plusieurs variantes pour l'énoncé. cependant, cela demanderait un pré-requis important pour l'usage de l'outil, à savoir la maîtrise du langage formel utilisé. cette solution ne serait pas satisfaisante sous cette forme. il serait donc intéressant de travailler sur le cheminement inverse, c'est-à-dire le passage d'une représentation formelle vers un énoncé en langue naturelle intelligible. nous pourrions d'ailleurs pousser la réflexion sur le développement de l'interaction. la théorie de la représentation du discours pourrait être une source d'inspiration. l'idée serait la suivante : l'analyse de l'énoncé permet de construire une première représentation avec un certain niveau d'ambiguïté ; les interactions du système avec l'utilisateur conduisent à la mise à jour de cette représentation, qui est validée lorsqu'il n'y a plus d'ambiguïté. l'utilisation d'une ontologie pour représenter les concepts du domaine est une autre piste, alternative ou complémentaire. celle-ci nous semble particulièrement adaptée pour le traitement des ambiguïtés dans les groupes nominaux. en effet, un groupe nominal, éventuellement complexe, doit correspondre à un concept de l'ontologie, et ainsi être vu comme atomique. les synonymes pourraient être traités de manière similaire, un même concept pouvant correspondre à plusieurs groupes nominaux. ces deux axes pourraient être complémentaires. la construction d'une ontologie est cependant une tâche délicate qui demande un investissement important. travailler sur une ontologie incomplète pourrait être une nécessité. il serait instructif d'examiner les possibilités d'apprentissage des concepts par le système, et de la mise à jour interactive de l'ontologie de référence. par exemple, le cahier des charges pourrait contenir des définitions qui pourraient être prises en compte pour mettre à jour l'ontologie. de même, les différents échanges du système avec l'utilisateur pourraient être pris en compte, avec un certain degré de confiance sur les concepts enregistrés. par ricochet, de nouvelles problématiques apparaissent : comment quantifier ce degré de confiance ? et même au delà, l'un des objectifs étant de vérifier la cohérence des exigences, une réflexion devra être menée sur la mise en évidence des incohérences. autrement dit, quel résultat proposer lorsque le cahier des charges est inconsistant ? il pourrait alors être utile d'offrir au concepteur la possibilité de simuler un cahier des charges, traduit dans un formalisme tel que les spécifications modales, et de modifier les spécifications de manière interactive, en cours de simulation. un autre axe de travail consisterait à étendre les interfaces modales à des formalismes plus expressifs, et à tenter de prendre en compte les propriétés numériques des systèmes cyber-physiques. les propriétés numériques permettent de définir des enveloppes de trajectoires pour les systèmes cyberphysiques, prenant généralement la forme d'équations ou d'inclusions différentielles qui caractérisent la dynamique en temps continu du système. c atala 2018