Titre : Validation d'applications pour les robots Lego(TM) Mindstorms

Responsable(s) : Yves Ledru, Lydie du Bousquet Email : Yves.Ledru@imag.fr

Laboratoire : Logiciels, Systèmes et Réseaux (LSR)

Mots Clefs : Specifications, validation, test

Condition de réalisation :

Description du Contexte :

Les Légos Mindstorms sont une évolution du célèbre jeu de construction. Ces robots sont commandés par un petit ordinateur (le RCX) qui peut commander jusque trois moteurs et gérer trois capteurs. Combinés avec diverses pièces, il est possible de réaliser toutes sortes de robots.

L'unité de commande RCX peut se programmer dans divers langages, notamment en Java( voir le site Java pour les mindstorms). Dans le cadre de l'enseignement de l'informatique, ces robots peuvent être utilisés pour illustrer diverses activités : programmation parallèle et réactive, test d'applications, simulation, validation et vérification.

JML (Java Modelling language) est un langage de spécification qui permet d'ajouter diverses assertions en entrée et sortie de méthodes java. D'une part, ces assertions décrivent le "contrat" que réalise la méthode, sans entrer dans les détails de sa réalisation. D'autre part, elles permettent de tester si une exécution de la méthode se déroule comme prévu.

Le but de ce travail est d'expérimenter l'utilisation de JML en combinaison avec les Légos Mindstorms. Il s'agira de spécifier en JML et de réaliser en Java une application simple, mais qui illustre bien l'utilisation d'assertions en entrée et en sortie de chaque méthode.

Ce sujet est proposé à la fois en Magistère et en TER. Il s'agira d'adapter la portée du travail au temps disponible.