Ce travail nous amènera à enrichir la théorie mathématique des structures ordonnées par des thématiques proches des applications en informatique; en direction opposée, nous pensons pouvoir profiter des connaissances théoriques pour aboutir à une meilleure compréhension du domaine applicatif. En particulier, une meilleure compréhension des heuristiques mises en place dans les outils de vérification par modèle nous permettra de comprendre leurs complexités théoriques, de les améliorer et d'obtenir ainsi des outils de vérification plus efficaces.
Un deuxième objectif du projet -- de nature plus appliquée -- est le développement d'outils de vérification par modèle efficaces reposant sur les considérations théoriques développées.
Deux aspects de la théorie des ensembles ordonnés nous paraissent être plus prometteurs en vue des applications au calcul parallèle, distribué et concurrent.
Le premier thème -- qu'on peut encadrer dans le thème plus général de la sémantique de la concurrence -- porte sur la spécification des structures d'ordre infinies par des méthodes finies. Son étude fera appel à la théorie des traces et des automates avec relations d'indépendance et posera en premier plan les structures d'ordre circulaire. La maîtrise de ce sujet nous permettra de mieux comprendre la structure fine de la sémantique du calcul concurrent, traditionnellement définie à l'aide des structures ordonnées.
Un deuxième thème porte sur la combinatoire et l'algèbre des ensembles ordonnés finis. On s'intéressera à la structure combinatoire des traces modélisant les exécutions concurrentes et aux systèmes dynamiques dont l'ordre d'atteignabilité donne lieu à un treillis. Rappelons qu'un problème fondamental pour développer les outils de vérification par modèle est l'explosion du nombre d'états d'un système : la maîtrise de la combinatoire des structures ordonnées nous permettra de développer des algorithmes pour explorer efficacement les états des systèmes concurrents.
Notre travail sera complété par le développement des deux outils de spécification et vérification des systèmes concurrents, AMSC et ELSE. Ces deux outils s'appuient sur des représentations d'exécutions sous forme d'ordres partiels. Le premier permettra l'analyse fine des diagrammes de séquences utilisés pour la spécification des protocoles. Le deuxième permettra d'explorer de manière efficaces l'ensemble des états des systèmes concurrents.