Validation de code mobile par interprétation abstraite

• Analyse du pi-calcul


• Pi-s.a. III : analyse (non-uniforme) des interactions entre les processus et dénombrement des processus.



 Analysis Session Version 3.23 (Feb 2006)

Une aide en ligne est disponible,
Ainsi que quelques exemples:

• un serveur ftp : ftp_server.pi, ftp_server.html ;
• un serveur ftp erroné: wrong_ftp_server.pi, wrong_ftp_server.html ;
• un anneau de processus : ring_of_processes.pi, ring_of_processes.html ;
• un anneau à jeton: token_ring.pi, token_ring.html ;
• un anneau à jeton erroné: wrong_token_ring.pi, wrong_token_ring.html ;
• une exclusion mutuelle : alterne.pi, alterne.html ;
• une liste doublement chainee : double_linked_list.pi, double_linked_list.html.

Ces exemples sont expliqués ici.

Prochainement (peut-être ?)
• rafinement de l'analyse des interactions (avec invariants affines)
• analyse de dépendance entre les canaux d'un même processus



• Analyse des ambients


• Amb-s.a. : analyse (non-uniforme) des interactions entre les processus et analyse de forme



 Analysis Session Version 1.01 (Feb 2006)


Une aide en ligne est disponible,
Voici un exemple de serveur ftp:

server.amb, server.html ;





• Analyseur générique
• Mob-s.a. : a generic analyzer for mobile systems

 Analysis Session Version 0.01 (Feb 2006)


• frontends/backends disponibles:
  • pi-calcul, fusion-calcul, swapping-calcul
• analyses disponibles:
• 0-cfa et confinement.