|
Depuis le 15 novembre 2000, j'effectue un post-doc à l'Université de
l'Aquila (Italie) dans l'équipe dirigée par Poala Inverardi dont les
recherches portent sur l'application des méthodes formelles à la
conception de systèmes.
Ces dernières années, ses travaux se sont concentrés sur les architectures logicielles et
l'utilisation d'un langage de spécification, connu sous le nom de
GAMMA [Banatre+:Coordina'96:GammaTenYearsAfter] ou de
«Chemical Abstract Machine» [Berry+:92:TCS:ChemicalAbstractMachine], pour
décrire les aspects dynamiques des architectures logicielles.
Mes travaux de recherche s'inscrivent dans cette voie et se
concentrent sur la vérification de systèmes infinis, la prise en
compte des aspects statiques et dynamiques et l'application des
techniques développées pour les architectures logicielles à l'étude
des propriétés de sécurité des systèmes informatiques.
Cohérence entre aspects statiques et dynamiques d'une spécification
Je poursuis les travaux initiés en fin de thèse sur la définition
d'une technique de cohérence entre les aspects statiques et dynamiques
d'un système.
Les aspects statiques sont décrits par des diagrammes avec
multiplicités.
Un tel diagramme définit une ensemble de graphes qui
représente les états ou les configurations valides du système.
Les aspects dynamiques, c\est à dire le comportement du système, sont décrits
sous forme de règles de réécriture GAMMA qui correspondent des
transformations de graphe.
Le modèle de calcul de GAMMA est la réécriture de multi-ensembles
dont la réécriture de graphe est un cas particulier qui correspond à
la réécriture d'ensemble d'arcs.
Les règles de réécriture définissent un système de transitions
entre des états représentés par des graphes.
Cette construction m'a permis d'établir un lien sémantique entre
aspects statiques et dynamiques.
Puis, en adaptant les travaux de Mentré et al. sur l'étude de
protocoles décrits dans le formalisme GAMMA,
j'ai proposé une première technique de vérification de cohérence entre
aspects statiques et dynamiques.
Mon objectif est maintenant d'améliorer la précision des abstractions
effectuées par l'algorithme et d'appliquer les différentes techniques
de que j'ai développées à la vérification de cohérence entre aspects
statiques et dynamiques de politiques de sécurité d'une part et de
spécifications UML d'autre part.
Vers une formalisation d'UML
Sur ce dernier point, j'ai entrepris un travail traduction des
diagrammes dynamiques d'UML sous forme de règles de réécriture
GAMMA.
Mes efforts de formalisation des diagrammes avec multiplicités et des
diagrammes dynamiques ont pour but de d'offrir des techniques de
vérifications de systèmes infinis aux utilisateurs de notations
graphiques standards.
Transformations d'architectures logicielles
Par ailleurs, je poursuis mes travaux dans le domaine des
architectures logicielles mulit-vues en intégrant désormais les
aspects dynamiques.
Je co-encadre le travail de Fabio Mancinel qui effectue son DEA avec
Paola Inverardi sur la formalisation des transformations permettant de
passer d'un style architecturale à un autre.
Les styles sont décrits par des diagrammes avec multiplicités
(inspirés de la notation UML) pour la partie structurelle et par des
règles de réécriture en ce qui concerne la politique de communication.
La transformation d'un style en un autre est spécifiée par des
correspondances entre les composants de bases de chaque style :
formellement il s'agit d'arcs entre les noeuds des différents
diagrammes.
Ce problème est étayé par une étude de cas proposée par une compagnie
de télécommunication qui souhaite faire évoluer ses applications web
basée sur le concept des Active Objects vers le modèle
J2EE (Java two Enterprise Edition) reposant sur
les Java Beans, plus standard dans le domaine du web.
Nous travaillons actuellement à la définition d'une notion de
correction et d'une notion de coût d'une transformation
d'architecture. Il s'agit en particulier de s'assurer que les
invariants d'un style et le comportment dynamique de l'architecture se
transposent dans l'autre style.
Étude des infrastructures PKI de gestion de clés cryptographiques
Mon intérêt pour la sécurité et la vérification de systèmes au niveau
architectural m'ammène à co-encadrer le DEA de Sabrina Paolini sur les
infrastructures de gestion des clés de cryptage ou PKI (Public Key
Infrastructures).
Le sujet que nous avons proposé à Sabrina Paolini est l'étude des
infrastructures de coopération qui relient entre elles des autorités
de certification (CA) chargées de gérer les associations entre une clé
publique et l'identité de son propriétaire.
L'étude des PKI est un thème émergent en sécurité. En dehors des
failles relatives aux protocoles eux-mêmes, il existe une autre source
de vulnérabilité des échanges cryptés, peu étudiée mais dont
l'importance se fait jour avec le développement à grande échelle du
commerce électronique : comment être sûr que la clé publique K
qu'une personne X utilise pour communiquer secrètement avec
Y est bien celle de la personne Y ?
Si un tiers Z connaissant la clé KY de Y,
réussit à me faire croire que sa clé KZ est la clé de la
personne Y, il peut s'immiser dans la conversation en tant
qu'intermédaire transparent entre X et Y, et ce alors
même que le protocole utilisé est sans faille.
L'étude des infrastructures PKI apparaît donc comme le complément
nécessaire aux vérification de la sûreté de protocoles
cryptographiques.
L'organisation des CAs (structurées en arbre, en un graphe quelconque,
en un graphe sans cycle,...) conduit à des infrastructures plus ou
moins vulnérables et disposant d'une ou plusieurs façon de coopérer
pour produire un certificat (clé, identité).
Cette problématique a de nombreux points communs avec l'étude des
architectures logicielles mulit-vues.
Aussi, avons-nous pour objectif d'adapter les techniques développées
pour l'analyse d'architectures logicielles afin, d'une part, de
vérifier la cohérence des niveaux de confiance associés à chaque CA et
à chaque relation de coopération, et d'autre part, afin d'attribuer un
niveau de confiance à une association (clé, identité).
Formellement, un certificat (clé,
identité) est décrit par un chemin dans le graphe de coopération qui
indique les CAs impliquées dans l'élaboration de ce certificat.
Ce travail est mené en collaboration avec D. Le Métayer, directeur
technique de la société Trusted Logic spécialisée dans le
domaine de la sécurité informatique (cartes à puce et protocoles).
|
Spécifications graphiques multi-vues : vérification et analyse de
systèmes infinis décrits par des diagrammes avec multiplicités
et des règles de réécriture.
Applications :
- à la vérifications d'invariants de systèmes dynamiques ;
- à la vérification de cohérence des diagrammes UML ;
- à la vérification de cohérence de poltiques de sécurité ;
- à l'analyse d'architectures logicielles multi-vues.
Mes recherches se situent à la rencontre des domaines du génie
logiciel et de la vérification de systèmes infinis.
Mon but est de développer des outis d'aide à la conception
de systèmes complexes.
Je m'appuie sur les notions d'abtraction et de décomposition en vues
afin de réduire la complexité des spécifications de systèmes.
Mes travaux visent à la fois
à répondre au besoin d'abstraction et de décomposition par aspects,
auxquelles tentent de répondre des méthodes telles qu'UML
ainsi qu'à formaliser les notations graphiques multi-vues dans le but
de palier le manque d'outils d'analyses et vérifications.
Les techniques que j'étudie s'appuient sur la notion de structuration
en vues, de graphes annotés, de réécriture et d'abstraction.
De part leur généralité, elles trouvent des applications dans des
domaines de nature différente telles que l'analyse des architectures
logicielles, la vérification de cohérence de politques de sécurité et
de diagrammes UML.
Mon projet de recherche s'organise autour de trois activités qui
posent à la fois des problèmes théoriques et pratiques :
| |
formalisation :
Il s'agit de formaliser les notations graphiques utilisées dans
l'industrie du logiciel et notamment UML : les diagrammes statiques
peuvent être plongés dans le formalisme défini dans ma thèse et le
diagrammes dynamiques être traduits sous forme de règles de
réécriture de graphe.
Cette démarche, associée à une formalisation des relations entre
diagrammes, pose les bases nécessaires pour développer des outils de
vérification de systèmes spécifiés à l'aide de plusieurs vues avec
des notations inspirées d'UML.
analyse et vérifiction de systèmes infinis :
Mon objectif est concevoir des techniques d'analyses et de
vérification qui puissent s'appliquer à des familles infinies de
graphes décrites par des diagrammes avec multiplicités.
Je souhaite d'étendre le formalisme proposé dans ma thèse pour
décrire avec plus de précision les familles de graphes définies par
des diagrammes.
Un des aspects théoriques de ce travail consiste à de jouer sur les
deux paramêtres que sont (1) le formalisme de
description et (2) le langage des propriétés de
graphes, de manière à obtenir un cadre dont l'expressivité soit
suffisante pour répondre aux besoins des concepteurs et qui reste
décidable afin que les outils soient automatiques.
Plusieurs directions sont envisagées : l'extension du formalisme des
diagrammes et l'étude de propriétés de nature quantitative (voir CV détaillé).
Il s'agit de généraliser l'utilisation des multiplicités et
contraintes structurelles sur les graphes pour à la fois préciser les
diagrammes et exprimer des invariants à vérifier.
La partie analyse s'attache à définir une technique de calcul de
propriétés de nature quantitative (par opposition aux propriétés de
nature qualitative dont la réponse est vrai/faux) dans le cas de
familles de systèmes (de taille arbitraire).
prise en compte des aspects statiques et dynamiques :
Enfin, je mène des recherches qui visent à prendre en compte les
aspects dynamiques du système afin de s'assurer que le comportement
du système ne met pas en péril les invariants décrits dans la partie
statique par des diagrammes avec multiplicités.
Diverses techniques sont envisageables pour vérifier la cohérence
entre aspects statiques et dynamiques d'un système. Elles sont basées
sur la notion de système de transitions entre des états représentés
par des graphes. Ces travaux prolongent les recherches effectuées
durant mon stage post-doctoral.
|
Je suis particulièrement intéressé par l'utilisation conjointe de
procédures automatiques pour traiter les cas de bases et de techniques
de preuve par induction et d'interprétation abstraite pour étendre le
champ d'application des vérifications.
Les trois activités de recherche précédentets s'inscrivent dans un
démarche génie logiciel et se déclinent suivant trois aspects :
| |
méthodologie :
l'aspect «méthodologique» de mes recherches vise à déterminer les
mécanismes d'abstraction/raffinement, de décomposition en
vues/d'agrégation utiles à l'étude de logiciels complexes.
Les vues et la description de systèmes au niveau architectural sont
les outils dont on se dote pour réussir à maîtriser la construction ou
la maintenance de systèmes complexes.
Dés lors qu'on autorise les concepteurs à créer de nouvelles vues, il
devient nécessaire de proposer des outils d'analyse qui soient
paramétrables et puissent traiter les nouvelles vues.
L'utilisation des graphes annotés pour représenter les architectures
logicielles permet de décrire de nombreux aspects d'un système et de
définir une large panoplie d'analyses qui s'expriment en terme de
propriétés d'accessiblité sur les graphes. Cette démarche tire parti
des travaux de T. Reps dans le domaine de l'analyse de programmes.
La démarche générale de conception de systèmes et d'analyse basée sur
les architectures logicielles multi-vues est présentée en détail dans
la version postscipt de mon CV.
spécification :
l'aspect «spécification» de mes travaux consiste à proposer des
formalismes graphiques adaptés à la pratique des concepteurs de
systèmes et associés à des outils d'analyse automatiques.
La généralisation de l'utilisation des diagrammes avec multiplicités
offre la possibilité de travailler avec des familles infinies.
Les multiplicités sont un mécanisme d'abstraction au sens où elles
permettent d'étudier des familles de systèmes ou d'architectures
logicielles et ainsi de ne pas fixer a priori la taille du système.
Un diagramme définit un ensemble infini de graphes
qui représentent les différents états ou configurations
possibles d'un système.
Les vérifications sont alors indépendantes du nombre d'entités dans le
système. Elles reposent sur l'emploi de langages de propriétés de
graphes. Ce choix correspond au souci de rendre ce cadre accessible à
tout utilisateur de méthodes graphiques de conception qui ne soit pas
nécessairement un spécialiste des méthodes formelles.
applications :
L'aspect «application» de mes recherches consiste à implémenter les
outils d'analyse et de vérification, à les expérimenter sur des études
de cas afin de les valider, puis à les intégrer dans des
environnements de développement afin de vérifier leur applicabilité
sur des problèmes de taille réelle. Deux exemples d'applications sont
détaillés dans les sections «vérification de la cohérence de
politiques de sécurité» et
«vérification de la cohérence de diagrammes UML» de mon CV.
|
Les différents aspects pratiques et théoriques
de mes travaux, qui sont ici présentés séparement, ne sont en réalité
pas dissociés et s'influencent mutuellement.
|
|
- Stage post-doctoral à L'Université de L'Aquila
-
Encadrement de deux étudiants de DEA de Paola Inverardi :
- transformations de styles architecturaux
- étude des infrastructures PKI de gestion de clés cryptographiques
-
Encadrement d'un mini-projet de Maitrise sur la formalisation d'un protocole d'authentification
dans le cadre du cours « ingéniérie du logiciel II : les méthodes formelles »
- ATER à mi-temps à l'IFSIC/université de Rennes 1 en 1999-2000, chargé des
enseignements suivants :
- Génie logiciel, IUP 1ère année
- Outils pour le traitement de l'information, DEUG 2ème année
- Algorithmique et complexité, Ingénieur DIIC 2ème année
I spent one year as a mid-time teaching assistant at the computer science department (IFSIC) of Rennes university.
- Vacataires à l'INSA de Rennes en 1997 et 1998, chargé de la conception et de l'encadrement de TP
- Compilation : techniques et outils, Ingénieurs INSA 4ème année
I was involved for two years (1997, 1998) in a course on "Compiling technics"
for 4th year students at the INSA engineering school.
- Vacataires en 1996 à l'IFSIC chargé de l'encadrement de TP de Pascal
- Introduction à la programmation impérative, DEUG 2ème année
I participated in 1996 at IFSIC in a course on the Pascal programming
language for 2nd year students.
|
-
Consistency checking of static and dynamic diagrams in multiple view graphical design methods,
submited to VLFM'2001.
Extended version published as a
Saladin technical report
keywords
Multiple views, UML, consistency checking, static and dynamic aspects,
diagrams with multiplicities, state machines, graph rewriting.
Bibtex,
abstract,
ps gzipped file
-
Cohérence de spécifications multi-vues (version étendue),
à paraître dans un numero spécial de la revue Technique et Science
Informatiques consacré aux méthodes formelles, 2001.
mots-cles
Architectures logicielles, modélisation multi-vues, vérification de
cohérence, aspects statiques et dynamiques, diagrammes avec
multiplicités, UML, propriétés de graphes, OCL, réécriture de graphes
keywords
Software architecture, multiple views, consistency checking, static
and dynamic aspects, diagrams with multiplicities, UML, graphs
properties, OCL, graph rewriting.
BibTeX,
resume, abstract,
ps gzipped file.
-
Spécifications graphiques multi-vues : formalisation et vérification de cohérence,
thèse de doctorat de l'universite de Rennes 1, soutenue le 6 octobre 2000.
mots-cles
Vues multiples, modélisation, spécification, cohérence,
diagrammes UML, réécriture de graphes, contraintes logiques,
vérification, architectures logicielles
keywords
Multiples views, system modeling, specification, consistency,
UML diagrams, graph rewriting, logic constraints, verification,
software architecture
BibTeX,
resume, abstract, ps, pdf files.
-
Cohérence de spécifications multi-vues,
dans les actes de l'atelier AFADL'2000 (Approche Formelles pour
l'Aide au Developpement de Logiciels), Grenoble.
mots-cles
Architectures logicielles, modélisation multi-vues, vérification de
cohérence, aspects statiques et dynamiques, diagrammes avec
multiplicités, système de contrôle d'accés.
BibTeX,
ps gzipped file.
-
Consistency checking for mutliple view software architectures
with D. Le Métayer, and P. Fradet,
In proceedings of the 7th ACM ESEC / FSE'99 conference, LNCS 1687, Toulouse.
keywords
software architecture, multiple views, formal semantics, UML
diagrams, families of graphs, static consistency verification.
BibTeX, abstract,
ps gzipped file,
pdf gzipped file.
-
Modeling railway control systems using graph grammars: a case study
with A. A. Holzbacher, and M. Südholt,
in proceedings of the 2nd International Conference on
Coordination Models, Languages and Applications
(COORDINATION' 97), LNCS 1282, Berlin.
Extended version published as an
INRIA technical report, no 3210.
keywords
software architecture, graph grammars, architectural style, multiple
views, static verification, architectural evolution.
BibTeX, abstract,
ps gzipped file.
|
I've presented my point of view on software architectures at the
Saladin's
Workshop
on
Software Architectures and Languages to Coordinate Mobile Distributed Components,
Venezia, 14-16 Febbraio 2001 :
« Analysis of multiple view software architectures:
shifting into the graph world »
(slides of the talk)
|
Prototype écrit CAML et C d'un vérificateur de cohérence (en cours)
Je travaille actuellement à une implémentation en CAML des algorithmes
de vérification de cohérence de vues décrits dans ma thèse.
L'algorithme de vérification conçu pour la logique CSG exploite une
bibliothèque C de calcul sur les BDD (Binary Decision
Diagrams). L'utilisation des BDD permet d'une part minimiser la
tâche d'implémentation puisque les connecteurs logiques sont déjà
définis et d'autre part de bénéficier de calculs de point fixe
optimisés pour ces structures. Ainsi, je me concentre sur la partie la
plus interéssante de l'algorithme : la stratégie d'application des
règles d'inférence.
Je travaille en collaboration avec D. Mentré de
l'INRIA-Rocquencourt en prévision d'établir une passerelle
entre nos deux prototypes, tous deux écrits en CAML.
Nous tentons l'expérience intéressante de définir une interface afin
de permettre une coopération sans heurt de nos deux systèmes.
D. Mentré a développé un prototype qui permet de déterminer des
conditions suffisantes pour garantir que des règles de réécriture
préservent des propriétés numériques et logiques ; les conditions
retournées peuvent être traduite dans mon formalisme sous forme de
nouvelles contraintes de multiplicités qui caractérisent les états
initiaux du système.
Au cours de mon stage post-doctoral, j'ai défini un notion de
cohérence entre aspects statiques (les propriétés invariantes) et les
aspects dynamiques (le comportement du système) exprimés sous forme de
règles de réécriture de
graphes.
Cette définition pose les bases qui permette de combiner nos deux
types de vérification.
Le rôle de ce lien entre nos deux outils est détaillé dans
l'article soumis à VLFM'2001.
|
Spécifications graphiques multi-vues :
formalisation et vérification de cohérence
(postscript)
J'ai effectué mes travaux de recherche à l'IRISA/INRIA-Rennes
au sein de l'équipe LANDE (Logiciel : ANalyse et
DÉveloppement) sous la direction de Daniel Le Métayer et
Jean-Pierre Banâtre.
Dans le cadre de mon doctorat, j'ai étudié les architectures
logicielles dont le rôle est de décrire l'organisation globale d'un
système à un niveau d'abstraction suffisamment élevé pour offrir aux
concepteurs une vision synthétique du système.
Je me suis intéressé à la notion de vues, déjà utilisée dans
d'autres disciplines (SGBD, spécifications formelles,
méthodes graphiques de conception, ...) pour mettre en lumière un
aspect du système par extraction d'une vue, ou bien pour structurer
les spécifications d'un système.
J'ai adapté cette notion au cas des architectures logicielles afin de
décrire séparément les différents aspects d'un système tels que les
structures de données, le flot de contrôle, le flot de données, les
interactions entre processus, l'organisation du code en modules,
l'architecture physique, etc.
Les décompositions par aspects simplifient la description mais peuvent
conduire à des spécifications incohérentes. Ceci se produit lorsque
des vues différentes mais qui ne sont pas totalement indépendantes
expriment des exigences contradictoires.
Des vérifications de cohérence sont alors nécessaires afin de détecter
ces erreurs de conception dès les premières phases de développement.
Mes recherches ont conduit à une formalisation de la notion de vue
basée sur les graphes annotés, ainsi qu'à la définition de trois
notions de cohérence de vues (syntaxique, structurelle et sémantique).
Le formalisme graphique proposé dans ma thèse permet de spécifier des
familles d'architectures logicielles multi-vues qui sont
décrites par des diagrammes avec multiplicités inspirés de la notation
UML (un tel diagramme définit un ensemble infini de graphes qui
représentent les différentes configurations possibles de
l'architecture logicielle). Les deux premières notions de cohérence
s'accompagnent de techniques de vérification automatiques qui prennet
en compte la généricité des diagrammes et permettent de vérifier la
cohérence des vues qui définissent la famille d'architectures
logicielles.
Dans le cas des formalismes graphiques multi-vues, la sémantique des
vues est très rarement définie de manière complète et les descriptions
graphiques sont le plus souvent informelles.
Il n'est donc pas envisageable de prouver comme dans le cas des
langages de spécification multi-vues que la description du système ne
comporte aucune contradiction -- ce problème est indécidable en
général -- il s'agit plutôt de définir des critères de cohérence qui
caractérisent les erreurs de conception classiques et de détecter
automatiquement les incohérences entre vues.
Dans ma proposition, les critères de cohérence sont définies par les
concepteurs des vues sous la forme de propriétés logiques sur les
graphes exprimées en terme d'arcs et de chemins.
Cette logique simple permet de spécifier de nombreuses contraintes de
cohérence issues des méthodes graphiques de conception multi-vues
telles qu'UML. Elle s'avère être un sous ensemble du langage OCL
utilisé pour préciser les spécifications UML et exprimée des
contraites de cohérence structurelles entre les différents diagrammes.
Par ailleurs, notre logique s'accompagne d'une techniques de
vérification automatique qui permet de s'assurer qu'une famille d'ALs
décrites par plusieurs vues satisfait des critères de cohérence
imposées par les concepteurs.
S'il est vrai que cette notion de cohérence structurelle n'est pas
suffisante pour montrer qu'un système est réalisable ; en revanche,
elle permet de raisonner sur des objets plus ou moins formels et des
sémantiques partielles, ce qui correspond à la pratique de
utilisateurs de méthodes graphiques de conception. Les techniques de
vérification automatique proposées s'avèrent donc utiles pour détecter
très tôt dans le développement des erreurs de conception et ainsi
contribuer à améliorer la qualité des systèmes.
|
|
