Master 2015 2016
Stages de la spécialité SAR
Vérification de programmes concurrents par solveurs SMT


Site : Vérification de programmes concurrents par solveurs SMT
Lieu : LIP6
Encadrant : Pr. J.-F. Pradat-Peyre
Dates :du 01/03/2016 au 31/08/2016
Rémunération :environ 550 Euros par mois sur 6 mois
Mots-clés : Master SAR, autre qu’ATIAM

Cliquer ici pour vous authentifier


Description

Contexte L’utilisation d’architectures multi-cœurs répond au double défi d’augmenter la puissance de calcul tout en réduisant la consommation énergétique par l’utilisation d’horloges 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 de sûreté ou de vivacité exprimées en logique temporelle. Si des travaux récents ont permis d’améliorer la fiabilité des logiciels systèmes embarqués en combinant l’utilisation de langages adaptés et des outils d’analyses automatiques - comme les solveurs SMT (par exemple CVC4 de New York University ou Z3 de Microsoft) ou des démonstrateurs de théorèmes (par exemple Why3 du LRI ou Alt-Ergo de OcamlPro) - la prise en compte efficace des aspects concurrents et multi tâches reste à faire. Une étude a été menée l’an passé pour tenter 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. Malheureusement différentes difficultés techniques dans la prise en main des outils utilisés de manipulation automatiques de programmes ont rendu peu conclusifs les résultats obtenus bien que plusieurs avancées prometteuses aient pu être réalisées. Nous souhaitons poursuivre cette étude porteuse d’avancées. Travail à faire Le stage aura pour objectif de définir et d’implémenter les patterns SMT correspondant aux patterns de la programmation concurrente : définition, démarrage ou arrêt d’une tâche, prise ou relâchement d’un verrou, accès à un moniteur, instructions de contrôles, etc. Ces patterns permettront de définir un procédé de traduction semi automatique de programmes concurrents (Ada, Java ou C/ POSIX) et de propriétés d’accessibilité vers un problème SMT. En appliquant ce procédé à des exemples bien choisis de la littérature du domaine ou provenant de projets industriels le stage permettra de démontrer la pertinence d’utiliser des outils SMT dans la vérification de programmes concurrents. 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 faire l’objet d’une poursuite en thèse.

Bibliographie

[1] O. Inverso, E. Tomasco, B. Fischer, S. La Torre, and G. Parlato. Lazy-CSeq : A Lazy Sequentialization Tool for C - (Competition Contribution). TACAS, LNCS 8413, pp. 398–401, 2014. [2] L. Cordeiro and B. Fischer. Verifying Multi-threaded Software using SMT-based Context-bounded Model Checking. In R. N. Taylor, H. Gall, and N. Medvidovic, editors, ICSE, pages 331340. ACM, 2011. [3] P. Trojanek and K. : Eder Verification and testing of mobile robot navigation algorithms : A case study in SPARK - Intelligent Robots and Systems (IROS 2014), 2014 IEEE/RSJ International [4] C.Dross, P. Efstathopoulos, D. Lesen, D. Mentre, Y. Moy : Rail, Space, Security : Three Case Studies for SPARK 2014 - ERTS2 2014