L’équipe de recherche CONVECS [L1] (INRIA, Univ. Grenoble Alpes, Grenoble INP, CNRS) étudie la modélisation et la vérification formelle de systèmes distribués, en proposant des langages de nouvelle génération pour décrire formellement le comportement et les propriétés de correction de ces systèmes. Ces langages et les outils d’analyse associés sont implémentés dans la boîte à outils CADP [L2] [L3], qui fournit une palette complète de fonctionnalités assistant le processus de conception : compilation et prototypage rapide, simulation interactive et guidée, vérification par équivalences et logiques temporelles, génération de tests de conformité avec garanties de couverture, évaluation de performances, etc.
Les outils CADP sont utilisés pour de nombreuses applications et leur développement a été salué par plusieurs prix scientifiques, dont le prix de l’innovation de l’Académie des sciences et le premier Test-of-Time Tool Award d’ETAPS.
Mission confiée
Le projet proposé consiste à améliorer CADP du point de vue des utilisateurs. Il comporte trois parties indépendantes.
Actuellement, le logiciel CADP est distribué en utilisant le protocole FTP (File Transfer Protocol), qui est ancien et de plus en plus souvent filtré par les navigateurs et les gestionnaires de réseau. L’objectif est de proposer une solution de remplacement, basée sur le protocole (Hypertext). Cette solution sera implantée dans l’outil INSTALLATOR qui permet de télécharger et d’installer automatiquement CADP sur une machine ou une grille de calcul. Il s’agira de modifier ponctuellement le code de cet outil, écrit dans le langage de scripts Tcl / Tk, afin de remplacer FTP par le nouveau protocole.
Les outils de base de CADP fonctionnent en ligne de commande, mais plusieurs interfaces graphiques ont été développées pour permettre de les utiliser de manière plus conviviale : EUCALYPTUS, CONTRIBUTOR et OCIS. Afin d’être portables sur divers systèmes d’exploitation (Linux, macOS, Solaris, Windows), ces interfaces ont été développées dans le langage de scripts Tcl / Tk et régulièrement maintenues au fil du temps. L’objectif est d’adapter ces interfaces pour permettre leur fonctionnement sur les écrans récents à haute résolution. En effet, les fenêtres de ces interfaces ont souvent une taille fixe, qui ne permet pas d’utiliser tous les pixels disponibles et qui conduit à des tailles de polices trop petites pour les yeux de certains utilisateurs. Le travail proposé consiste à faire évoluer ces interfaces par des modifications bien ciblées, afin d’autoriser les fenêtres de taille variable et d’apporter la possibilité de zoom sur le contenu de ces fenêtres.
Visual Studio Code (VS Code en abrégé) est un éditeur de code source très populaire. Développé par Microsoft et disponible en code libre ouvert sous Windows, macOS et Linux, VS Code reconnaît la plupart des langages de programmation existants. L’objectif est d’intégrer dans VS Code les différents langages de CADP (LNT, MCL, SVL, etc.). Dans un premier temps, le travail consistera à étudier VS Code et à comprendre ses interfaces qui permettent de connecter de nouveaux langages. Ensuite, il faudra réaliser des prototypes permettant de connecter un ou deux langages simples de CADP et s’assurer que le résultat correspond aux attentes des utilisateurs. Enfin, il faudra automatiser la production de connecteurs pour VS Code en étendant les outils SECT de l’équipe CONVECS qui permettent déjà de connecter automatiquement les différents langages de CADP à d’autres éditeurs : Emacs, Gnome GTK, Jedit, Nano, Notepad++, Sublime Text et Vim.
Principales activités
Pour tous renseignements complémentaires sur la mission confiée, il est possible de contacter.
Compétences
Compétences techniques et niveau requis : formation en informatique BAC + 4 minimum.
Langues : français ou anglais.
Compétences additionnelles appréciées : en lien avec le travail proposé.