Il existe quelques outils logiciels expérimentaux permettant de calculer des modèles mathématiques représentant le comportement d'applications Java, et d'en prouver des propriétés logiques. Parmi ces logiciels, nous nous intéressons à Bandera, conçu à Kansas University, qui extrait des modèles finis de programmes Java, et à nuSMV, développé à l'ITC-IRST à Trente (Italie), qui permet la verification de propriétés sur ces modèles (Model Checking).
Le stage consistera à tester l'usage de ces logiciels pour analyser des propriétés de sécurité ou de comportement distribués, pour des applications Java. Le but à moyen terme étant de développer une plateforme d'analyse et de vérification pour ces applications.
Nous avons développé ProActive, une bibliothèque 100% Java, qui fournit : des objets distants, des appels asynchrones, de la migration d'objets actifs (mobilité), le tout offrant des mécanismes de synchronisation de haut niveau qui simplifient la programmation répartie.
D'autre part nous avons étudié la vérification formelle par Model Checking de propriété de sécurité "à la Java2", ainsi que de propriétés de comportement de systèmes à objets répartis ProActive. Ces travaux ont été menés avec nos propres outils de vérification.
Le stage consistera à expérimenter l'application aux mêmes exemples des outils Bandera et nuSMV. Il sera nécessaire d'adapter les analyses fournies par Bandera à nos besoins propres en adaptant ou en développant de nouveaux modules d'analyse (Bandera et nuSMV sont fournis en Open-Source).
Ces travaux pourront éventuellement se poursuivre en Thèse de Doctorat.