Master 2014 2015
Stages de la spécialité SAR
Aide à la conception de programmes fiables pour architecture multi cœurs


Lieu :LIP6
Encadrant : Jean-François Pradat-Peyre
Dates :01/03/2015 au 31/08/2015
Rémunération :475€/mois (gratification classique)
Mots-clés : Master SAR, autre qu’ATIAM


Description

Contexte L’utilisation d’architectures multi-cœurs répond au double défi d’augmenter la puissance de calcul tout en maintenant voir en réduisant la consommation énergétique par l’utilisation d’horloge moins rapides. Ces architectures sont donc de plus en plus employées dans des contextes embarqués ou enfouis. Cependant ces architectures ne peuvent être réellement exploitées que dans le cadre d’exécution d’applications multi tâches, applications qui tirent pleinement parti du parallélisme offert par ces architectures de par leur conception pour laquelle les différentes activités sont réalisées par différentes tâches qui coopèrent. Une des difficultés que l’on rencontre alors est de concevoir des applications efficaces mais fiables, c’est à dire ne posant pas de problèmes d’inter blocage ou de race conditions et plus généralement respectant certaines bonnes propriétés exprimées en logique temporelle. Si des travaux récents ont permis d’améliorer grandement la fiabilité de logiciels systèmes embarqués (par exemple dans un contexte précis (environnement SPARK 2014, www.spark-2014.org) en utilisant des solveurs SMT ou des démonstrateurs de théorèmes comme CVC4, la prise en compte des aspects concurrents et multi tâches reste à faire.

Travail à faire Le stage aura pour objectif de compléter la chaine de production SPARK de programmes embarqués fiables par la prise en compte des aspects multi tâches, à la fois au niveau de la définition des constructions possibles en terme de langage et de propriétés à vérifier mais aussi en la réalisation de briques efficaces de vérification basées sur un solveur SMT. Dans un premier temps il conviendra d’analyser avec précision le langage SPARK version 2014 et 2015 afin de définir les constructions liées à la concurrence présentes dans le langage Ada, non inclues dans les versions SPARK mais pouvant être assez facilement vérifiables par des techniques statiques ou de model-checking et donc pouvant être introduites sans danger dans le langage SPARK 2014. Il faudra alors développer (par assemblage ou spécialisations d’outils existants par exemple développés au LIP6) les outils permettant de vérifier quelques propriétés utiles liées à la concurrence pour des programmes écrits en SPARK 2014. Le travail sera mené en partenariat avec des industriels du domaine et les expérimentations se feront sur des parties de codes réellement exploitées ou exploitables dans des environnements sensibles. Perspectives Ce travail pourra être étendu dans le cadre d’une thèse à des environnements de développements plus larges en particulier vers les machines virtuelles type LLVM.

Bibliographie

http://www.spark-2014.org/uploads/e..., ERTS2 2014

Verification and testing of mobile robot navigation algorithms : A case study in SPARK, Piotr Trojanek and Kerstin Eder