Doctorat
Equipe : Vérification d'Algorithmes, Langages et Systèmes
Constructing Semantically Sound Object-Logics for UML/OCL Based Domain-Specific Languages
Début le 01/02/2013
Direction : WOLFF, Burkhart
[Delphine LONGUET]
Ecole doctorale : ED STIC 580
Etablissement d'inscription : Université Paris-Saclay
Lieu de déroulement : LRI
Soutenue le 06/04/2016 devant le jury composé de :
Directeur de thèse :
M. Burkhart WOLFF
Examinateurs :
M. Achim D. BRUCKER
M. Stéphane MAAG
M. Safouan TAHA
Rapporteurs :
Mme Catherine DUBOIS
M. Bernhard RUMPE
Activités de recherche :
- Formalisation de langages (de spécification et de programmation) dans les assistants de preuve
- Test formel basé sur les modèles
Résumé :
Les langages de spécifications basés et orientés objets (comme
UML/OCL, JML, Spec#, ou Eiffel) permettent la
création et destruction, la conversion et tests de types dynamiques
d'objets statiquement typés. Par dessus, les invariants de classes et
les opérations de contrat peuvent y être exprimés; ces derniers
représentent les éléments clés des spécifications orientées
objets. Une sémantique formelle des structures de données orientées
objets est complexe~: des descriptions imprécises mènent souvent à
différentes interprétations dans les outils qui en résultent.
Dans cette thèse, nous démontrons comment dériver un environnement de
preuves moderne comme un emph{méta-outil} pour la définition et
l'analyse de sémantique formelle de langages de spécifications
orientés objets. Étant donné une représentation d'un langage
particulier plongé en Isabelle/HOL, nous construisons pour ce langage
un environnement étendu d'Isabelle, à travers une emph{méthode} de
génération de code particulière, qui implique notamment plusieurs
variantes de génération de code. Le résultat supporte l'édition
asynchrone, la vérification de types, et les activités de déduction
formelle, tous ``hérités'' d'Isabelle.
En application de cette méthode, nous obtenons un emph{outil de
modélisation orienté objet} pour du UML/OCL textuel. Nous
intégrons également des idiomes non nécessairement présent dans
UML/OCL --- en d'autres termes, nous développons un support pour des
dialectes d'UML/OCL à domaine spécifique.
En tant que construction méta, nous définissons un méta-modèle d'une
partie d'UML/OCL en HOL, un méta-modèle d'une partie de l'API
d'Isabelle en HOL, et une fonction de traduction entre eux en
HOL. Le méta-outil va alors exploiter deux procédés de générations de
code pour produire soit du emph{code raisonnablement efficace}, soit
du emph{code raisonnablement lisible}. Cela fournit donc deux modes
d'animations pour inspecter plus en détail la sémantique d'un langage
venant d'être plongé~: en chargeant à vitesse réelle sa sémantique, ou
simplement en retardant à un autre niveau ``méta'' l'expérimentation
précédente pour un futur instant de typage en Isabelle, que ce soit
pour des raisons de performances, de tests ou de prototypages.
Remarquons que la génération de ``code raisonnablement efficace'', et
de ``code raisonnablement lisible'' incluent la génération de
emph{code tactiques} qui prouvent une collection de théorèmes formant
une théorie de types de données orientés objets d'un modèle
dénotationnel~: étant donné un modèle de classe UML/OCL, les preuves
des propriétés pertinentes aux conversions, tests de types,
constructeurs et sélecteurs sont traitées automatiquement. Cette
fonctionnalité est similaire aux emph{paquets de théories de types de
données} présents au sein d'autres prouveurs de la famille HOL, à
l'exception que certaines motivations ont conduit ce travail présent à
programmer des tactiques haut-niveaux en HOL lui-même.
Ce travail prend en compte les plus récentes avancées du standard
d'UML/OCL 2.5. Par conséquent, tous les types UML/OCL ainsi que
les types logiques distinguent deux éléments d'exception différents~:
inlineocl{invalid} (exception) et inlineocl{null} (élément
non-existant). Cela entraîne des conséquences sur les propriétés aussi
bien logiques qu'algébriques des structures orientées objets résultant
des modèles de classes.
Étant donné que notre construction est réduite à une séquence
d'extension conservative de théorie, notre approche peut garantir la
correction logique du langage entier considéré, et fournit une
méthodologie pour étendre formellement des langages à domaine
spécifique.
