Activités de Recherche / Research Interest
Ma recherche s'articule autour du développement de modèles pour la spécification et validation de systèmes autonomes et concurrents. Elle inclut l'analyse et la preuve des propriétés de ces modèles, leur application à la sémantique de diverses types de langages de spécification, ainsi que le développement de techniques permettant de rendre ces analyses et vérifications efficaces. La motivation principale de ces modèles est de permettre l'analyse des aspects liés à la concurrence, à la causalité, aux conflits, à l'adaptation, à la localisation, à la mobilité, et la vérification formelle des spécifications par des techniques fondées sur les réseaux de Petri, les automates ou les algèbres de processus.
Le point de départ de mes travaux a été l'algèbre des Petri-boxes (ou Petri Box Calculus, PBC), qui est un formalisme de bas niveau combinant dans un cadre unifié deux modèles fondamentaux de la concurrence : les algèbres de processus et les réseaux de Petri. PBC possède une syntaxe composée d'expressions (que l'on peut voir comme une généralisation des expressions régulières) et une sémantique composée de réseaux de Petri munis d'interfaces, appelés boxes (que l'on peut voir comme une généralisation adéquate des automates finis). Il dispose d'une panoplie d'opérations de contrôle de flot et de communication, et fournit une base flexible pour la définition des sémantiques compositionnelles des langages de spécification ou de programmation concurrents.
Mes recherches ont abouti à la définition de plusieurs versions de haut niveau de l'algèbre des Petri-boxes, dont l'algèbre des réseaux algébriques (retenus pour leur généralité, en particulier dans le traitement abstrait des données), l'algèbre des M-nets (basée sur l'utilisation des réseaux dits colorés, plus simples que les précédents car utilisant uniquement des types énumérés) et diverses extensions de cette dernière incluant le traitement du temps, de la préemption, de la mobilité et de la sécurité. Ces travaux ont été suivis, et souvent aussi motivés, par des applications à la sémantique des langages de spécification ou de programmation concurrents, mais aussi temporisés, orientés-objets, mobiles ou dédiés à la spécification de protocoles.
Mes travaux correspondent aux trois axes thématiques suivants :
- l'étude théorique et le développement de ces algèbres de réseaux de Petri de haut niveau et des preuves de propriétés sur leurs opérations,
- ll'application de ces modèles à la sémantique formelle des langages de spécification ou de programmation concurrents, mobiles ou temps-réel,
- la modélisation structurée et la vérification de systèmes complexes ; ces systèmes incluent les réseaux d'interaction biologiques, les systèmes multi-agents mobiles et les architectures à base de composants pour des applications de réalité virtuelle.
Une grande partie de ces recherches ont été menées dans le cadre de collaborations internationales : projets européens ou bilatéraux et échanges entre universités.
