Abstract FR:

Nous nous intéressons dans ce document à la vérification de propriétés comportementales d’applications distribuées par la technique du model-checking. En particulier, nous étudions le problème de génération de modèles à partir de programmes Java répartis et représentés par systèmes de transitions communiquant. A partir de la sémantique formelle de programmes ProActive – une librairie 100 % Java pour la programmation parallèle, distribuée et concurrente – nous construisons, de manière compositionnelle et hiérarchique, des modèles comportementaux finis pour des abstractions finies d’applications. Ces modèles sont décrits mathématiquement et graphiquement. Et la procédure de construction, dont nous prouvons la terminaison, est décrite par des règles sémantiques s’appliquant à une forme intermédiaire des programmes obtenue par analyse statique. Ces règles sont ensuite étendues afin de générer des modèles paramétrés pour des applications possiblement infinies. La construction de modèles paramétrés a été, d’abord, faite sur un noyau de Java et la bibliothèque ProActive, puis étendue à des constructions communication de groupe. Des exemples de modèles, générés directement à partir de ces règles implémentées par un prototype, sont également étudiés.