Depuis 2001 j'ai développé au sein de l'équipe Oasis des travaux de recherche sur la sémantique des applications à base d'objets distribués, appliquant dans le contexte d'un vrai langage, et d'applications de taille réelle, mes recherches précédentes dans le domaine des algèbres de processus. Les différents aspects de ce travail touchent naturellement à la sémantique comportementale, et à la définition de procédures de génération de modèles prenant en compte les différentes facettes de la programmation d'applications distribuées, mais aussi, en amont, à l'analyse statique de code et aux techniques d'abstraction de modèles, et en aval aux outils de vérification de propriétés comportementales. Je montre dans ce mémoire la complexité de ces recherches et la grande variété des techniques requises. Nous avons mis en place une méthode cohérente basée sur un modèle sémantique très flexible, le modèle pNets (parameterized Networks of automata), qui nous offre un bon compromis entre décidabilité, complexité, et utilisabilité. Cette approche nous a permis de définir une sémantique comportementale pour différents aspects des applications à base d'objets ou de composants distribués, mais aussi une notion d'abstraction vers des modèles abstraits finis, permettant d'utiliser des outils de vérification de type " model-checking ". L'ensemble de ces aspects a donné lieu à la réalisation de prototypes, dans la plateforme VerCors, et à des cas d'étude de grande taille.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00625248 |
| Date | 29 September 2011 |
| Creators | Madelaine, Eric |
| Publisher | Université de Nice Sophia-Antipolis |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | French |
| Type | habilitation ࠤiriger des recherches |
Page generated in 0.002 seconds