Thèse Contrats Quantitatifs et Sémantique Compositionnelle pour la Conception de Systèmes H/F - Doctorat.Gouv.Fr

Établissement : Université Paris-Saclay GS Sciences de l'ingénierie et des systèmes École doctorale : Interfaces : matériaux, systèmes, usages Laboratoire de recherche : Mathématiques et Informatique pour la Complexité et les Systèmes - EA 4037 Direction de la thèse : Marc AIGUIER ORCID 0000000301540909 Début de la thèse : 2026-10-01 Date limite de candidature : 2026-05-22T23:59:59 Les systèmes logiciels modernes et les systèmes cyber-physiques sont trop complexes pour être décrits par un seul modèle. On utilise donc plusieurs modèles complémentaires (structure, comportement, données, déploiement). Le génie dirigé par les modèles (MDE) organise cela en familles de modèles interconnectés, chacun représentant un aspect précis du système. Ces modèles peuvent être formalisés mathématiquement, par exemple via des graphes typés et des transformations de graphes, ce qui permet de raisonner sur leur structure et leur évolution.

Cependant, ces approches sont surtout structurelles et ne fournissent pas directement un cadre logique interne pour raisonner sur les propriétés (comme la correction ou les invariants). Pour cela, on utilise souvent des logiques externes ou des contraintes additionnelles. Cela motive le développement de cadres plus riches, notamment catégoriques (comme les fibrations ou les topos), qui intègrent structure et logique dans une même théorie.

Par ailleurs, la notion de design by contract permet de spécifier les systèmes via des contrats entre composants : des hypothèses sur l'environnement et des garanties si ces hypothèses sont respectées. Par exemple, un système de freinage garantit une distance d'arrêt sûre si la vitesse reste sous un seuil. Mais les approches classiques sont booléennes : un contrat est soit respecté soit violé, sans notion de degré ou de robustesse.

Enfin, bien que le MDE et le design by contract aient des objectifs similaires (raisonner sur des systèmes complexes de manière compositionnelle), ils sont généralement étudiés séparément : le premier se concentre sur la structure des modèles, le second sur le comportement. Cela limite la capacité à raisonner globalement sur les systèmes. D'où l'intérêt de cadres unifiés, notamment catégoriques, permettant de relier structure et sémantique de façon intégrée. Le projet s'inscrit dans une problématique fondamentale de l'informatique théorique appliquée aux systèmes complexes, à savoir la réconciliation entre sémantique contractuelle et structures catégoriques de modélisation. L'extension des contrats vers des cadres gradués et leur intégration dans des structures fibrées ou topos-théoriques constitue une approche prometteuse pour unifier compositionnalité, abstraction multi-niveaux et raisonnement logique interne. Le projet étudiera des extensions de la théorie des contrats ainsi qu'une approche structurée de la modélisation multi-niveaux.

Les extensions de la théorie des contrats pourront inclure des notions de satisfaction graduée ou floue, de robustesse et de raffinement, ainsi que des propriétés compositionnelles de ces contrats, en particulier leur comportement lors de la composition et de la décomposition de systèmes. Les abstractions catégoriques utilisées pour la modélisation multi-niveaux pourront inclure des fibrations et des topos relatifs, afin de permettre un traitement uniforme des modèles, des transformations et des relations sémantiques.

L'interaction entre ces deux axes pourra conduire à étudier la manière dont des structures catégoriques peuvent soutenir l'extension des cadres logiques pour le raisonnement sur les propriétés des systèmes. Les approches proposées seront validées à l'aide d'études de cas portant sur des systèmes logiciels complexes ou des systèmes cyber-physiques. L'évaluation portera sur l'expressivité du cadre, sa capacité à représenter des descriptions de systèmes évolutives, ainsi que son aptitude à permettre un raisonnement systématique sur les effets des changements.

Le candidat doit être titulaire d'un master ou d'un diplôme d'ingénieur, avec une spécialisation en informatique ou en mathématiques. Le candidat doit manifester un intérêt pour la logique mathématique, les méthodes formelles et la théorie des catégories. Des connaissances préalables en théorie des topos et en conception de logiciels ou de systèmes sont appréciées mais non obligatoires.