11/01/2001: Jerome Feret (LIENS)
Analyse de Systemes Mobiles par Interpretation Abstraite.
Résumé
Nous utilisons l'Interprétation Abstraite pour trouver et prouver de
manière automatique des propriétés de sûreté pour les systèmes
mobiles. Nous étudions notamment les propriétés de confidentialité, de
non-exhaustion et d'exclusion mutuelle. Nous nous sommes restreint à
l'étude des systèmes ouverts exprimés en pi-calcul (ces systèmes peuvent
interagir avec un contexte inconnu).
Notre analyse comporte une analyse non-uniforme des interactions entre
les processus et une analyse du multi-ensemble des processus présents
en cours d'exécution de notre système.
Notre première tâche a été de reformuler la sémantique de transition
du pi-calcul. Du fait de l'alpha-conversion, la sémantique
de Milner détruit le lien entre les noms de canaux et les instances
récursives de processus qui les ont déclarés. Nous introduisons une
sémantique non-standard qui tient explicitement compte de ce lien.
Nous utilisons ensuite l'Interprétation Abstraite
pour en dériver deux sémantiques abstraites. La première permet
d'obtenir une description non-uniforme des interactions entre les
processus du systèmes. Elle permet de savoir où les noms de canaux
peuvent être communiqués. La description est assez précise pour
distinguer les instances récursives d'un même processus. La deuxième
permet de
compter les occurrences des processus au cours des exécutions du
système. L'utilisation d'un domaine numérique adapté nous permet de
détecter des non-exhaustions de ressources et des exclusion mutuelles
pour un coût polynômial.