Recherche

Mes domaines de recherche se rapportent aux méthodes formelles et à leurs extensions et applications afin de faciliter la conception, le développement et la validation de systèmes qu'ils soient logiciels, matériels, ou biologiques. Certains de mes travaux, plus théoriques, s'intéressent aux fondements des méthodes formelles tandis que d'autres, plus appliqués, s'intéressent à élaborer de nouveaux formalismes de spécifications en fonction des applications souhaitées et à élargir l'impact des spécifications en généralisant leur utilisation à toutes les étapes du développement d'un système informatique (réalisation, vérification, validation, preuve, test, etc.).

Fondements des méthodes formelles :

Démonstration automatique - axiomatisation de la réécriture abstraite et généralisation de résultats de normalisation (élimination des coupures, logicalité, lemme de Newman, complétude du dépliage d'axiomes pour séléctionner des jeux de test)
Théorie des modèles abstraits - généralisation de résultats de la théorie des modèles dans la théorie des institutions (Interpolation de Craig et son équivalent quand la négation est vérifiée - la consistance de Robinson, chaîne élémentaire de Tarski, théorème de Beth)

Méthodes formelles dédiées :
L'emploi des méthodes formelles induit comme directions de recherche :

Élaboration de nouveaux formalismes. Spécifications algébriques dynamiques et temps-réel, intégration et interaction de services, dénotation formelle et abstraite des systèmes complexes (travail effectué dans le cadre du projet européen du FP6 (Information Society Technologies / Future and Emerging Technologies) GENNETEC (<< GENetic NETworks: Emergence and Complexity>>).
Élargir l'impact des spécifications. test fonctionnel des systèmes (définition d'algorithmes de sélection de jeux de test par dépliage d'axiomes pour des spécifications algébriques et co-algébriques).

Research

My research activy relates to formal methods and to their extension and application in order to make easier both system design and validation. Some of my works, more theoretical, are interested in the foundations of formal methods, while some others, more applied, are interested in defining new specification formalisms contingent on expected applications, and in making wider specification impact by generalizing the use of specification formalisms at every step of the system design (realization/implementation, certification, validation, proof, test, etc.).

Foundations of formal methods :

Automated reasoning - axiomatization of abstract rewriting and generalization of some normalization results (cut elimination, logicality, Newman's lemma, completeness of axiom unfolding used to select test cases)
Abstract model theory - generalization of some results of model theory in the institution theory (Craig interpolation and its equivalent when negation holds - Robinson consistency, Tarski's elementary chains, Beth's theorem)

Dedicated formal methods :
The use of formal methods leads to the following research activities :

Defining new formalisms. Dynamic and real-time algebraic specifications, feature integration and interaction, formal and abstract denotation of complex systems (work made in the framework of the European project of FP6 (Information Society Technologies / Future and Emerging Technologies) GENNETEC (<< GENetic NETworks: Emergence and Complexity>>).
Making wider specification impact. Functional testing of systems (development of algorithms to select test case by axiom unfolding for algebraic and co-algebraic specifications)

PhD students (former and current)

Stéfan Béroff - (An algebraic approach for CoDesign)
Christophe Gaston co-supervised with Pascale Le Gall - Researcher at CEA (French Atomic Energy Commission) - (Abstract denotation of feature integration and interaction over institutions)
Diane Bahrami co-supervised with Catherine Dubois - Researcher at CEA (French Atomic Energy Commission) - (Abstract rewriting theory)
Fabrice Barbier - (Abstract model theory)
Clément Boin co-supervised with Pascale Le Gall and Agnès Arnould - (Proof and test)
Delphine Longuet - Post-doc at CWI Netherlands - (Extension of axiom unfolding to select test cases for algebraic and co-algebraic specifications)
M'Barka Mabrouki co-supervised with Pascale Le Gall - ongoing - (Abstract denotation of complex systems : application to software architecture and regulatory gennetic networks)
Bilal Kanso co-supervised with Frédéric Boulanger, and Assia Touil - ongoing - (Heterogeneous modelling and integration testing)

Other information

Member of the editorial board of the International Journal on Advances in Software (IARIA Journals)
Member of the program committee of the International Conference on Software Engineering Advances (ICSEA)