Journée “solveurs SMT dans le contexte des systèmes embarqués critiques”. 29 Mars 2016

Journée AFSEC

Quand: Le 29 mars 2016
Lieu: Université Paris Diderot amphi Turing du bâtiment Sophie Germain map

Du fait des restrictions budgétaires, l'action prendra en charge les pauses café et le repas de midi sera à la charge de chacun. L'inscription (gratuite) au plus tard le 20 mars 2016 est nécessaire
en envoyant un email à claire.pagetti@onera.fr ; objet : "Inscription AFSEC 29 mars" (cliquer sur le lien) - préciser : Nom et Affiliation.

Programme :

• 9h30-10h00: accueil
• 10h00-11h15 Présentation de l'approche SMT (fondements mathématiques et logiques) et le standard SMT-lib (Pascal Fontaine, LORIA)
  • Résumé: Avant d'aborder les solveurs Satisfaisabilité Modulo Théories (SMT), nous considérerons brièvement le problème SAT de la satisfaisabilité en logique propositionnelle, et les techniques actuelles pour le résoudre, ces techniques étant elles aussi utilisées au coeur des les solveurs SMT.  Nous verrons ensuite l'architecture SMT, et comment elle s'articule autour d'un solveur SAT.  En particulier, nous verrons par l'exemple comment on peut élever l'expressivité d'un solveur SAT vers des langages plus riches, et comment, à partir de procédures de décision pour différents langages, on peut construire une procédure de décision sur la combinaison des langages.
    Enfin, nous présenterons quelques solveurs SMT disponibles, la communauté SMT et les différentes initiatives, notamment le standard SMT-lib qui définit un langage d'entrée accepté par la majorité des solveurs SMT.
• 11h15-12h30 Implémentation d'un solveur SMT: le cas Alt-Ergo (Theory-comb, AC-comp, Quantificateurs, etc) (Mohamed Iguernlala, OCamlPro/LRI)
  • Résumé: Alt-Ergo est un démonstrateur SMT conçu pour le domaine de la vérification de programmes. Il est intégré dans plusieurs outils, en particulier via la plateforme Why3. Il est utilisé par Frama-C et Caveat pour démontrer la validité d'obligations de preuves (OPs) issues de code C, par SPARK pour prouver les OPs générées à partir de programmes Ada, ainsi que sur des OPs générées par Atelier-B. Il est aussi utilisé par EasyCrypt pour la vérification de protocoles de cryptographie et par Cubicle pour faire du model-checking.
    Le langage d'entrée d'Alt-Ergo est une logique du premier ordre avec types polymorphes et théories prédéfinies. Son coeur combine un SAT-solver inspiré de la méthode des tableaux, un moteur d'instantiation de formules quantifiées, et un ensemble de procédures de décision pour des théories telles que la théorie de l'égalité non-interprétée, l'arithmétique linéaire sur les entiers et les rationnels, les tableaux fonctionnels polymorphes, les types énumérés ainsi que la théorie AC des symboles associatifs et commutatifs. Cet exposé sera l'occasion de revenir sur quelques détails d'implémentation d'Alt-Ergo, et sur les particularités qui font sa force dans le domaine de la vérification de programmes.
• 13h45-14h45 Vérification déductive de programmes (Claude Marché, LRI)
  • Résumé: Le principe de l'approche déductive de la vérification consiste, à partir d'un programme et d'une spécification formelle, à générer des "obligations de preuve": des formules logiques dont la validité implique que le programme respecte sa spécification. Nous illustrons cette approche telle qu'elle est implantée dans l'environnement Why3, ainsi que dans les plateformes Frama-C et SPARK pour la vérification de codes critiques C et Ada. Les solveurs SMT sont utilisés de manière prépondérante pour la preuve automatique des obligations de preuve. Nous examinons les avantages et les inconvénients de ces solveurs dans ce contexte.
• 14h45-15h45 Solveurs SAT application au model-checking (Loïg Jezequel, Université de Nantes)
  • Résumé: La planification est un domaine de l'intelligence artificielle ayant pour objectif de trouver des séquences d'actions (des plans) permettant d'atteindre, depuis l'état initial d'un système, un état objectif. Au début des années 90 une méthode de planification reposant sur l'utilisation de solveurs SAT a été proposée. Il s'agit de re-coder un problème de planification comme un ensemble (généralement infini) de problèmes SAT, puis de chercher à les résoudre l'un après l'autre dans un ordre bien choisi. Dès qu'une solution à l'un de ces problèmes SAT est trouvée, le problème de planification correspondant est résolu. Cette technique de planification s'est révélée surprenamment efficace, notamment en raison des efforts importants ayant été menés pour optimiser l'implantation des solveurs SAT.
    Dans cet exposé, nous présenterons une manière d'encoder les problèmes de planification comme des ensembles de problèmes SAT. Nous montrerons ensuite comment cette approche peut se généraliser pour calculer non plus un seul plan, mais des ensembles exhaustifs de plans, sous forme d'arbres d'exécution. Enfin, nous discuterons la possibilité d'étendre l'approche pour calculer des préfixes finis complets de dépliages de réseaux de Petri, comparables aux arbres d'exécution, mais plus compacts car prenant en compte la concurrence des réseaux de Petri.
• 16h00-17h00 Synthèse d'un diagnostiqueur déterministe pour la prise de décision embarquée (Stéphanie Roussel, ONERA)
  • Résumé: Nous nous intéressons au problème de la synthèse d'un diagnostiqueur à base de modèle devant être intégré avec un algorithme de planification en vue d'une prise de décision embarquée. Les planificateurs que nous visons étant déterministes (pas de gestion de l'incertitude), le diagnostiqueur doit renvoyer à chaque étape un unique diagnostic. Nous utilisons alors une combinaison de systèmes de transition, logique temporelle et réseau de préférences conditionnelles booléennes (CP-Nets) pour spécifier le diagnostiqueur. Nous décrivons différentes réductions du  calcul d'un diagnostic vers le cadre de satisfaction booléenne et comparons des implémentations basées SAT et BDD sur un benchmark de type mission multi-robots soumis à différentes pannes.
• 17h00-18h00 Synthèse d'architecture embarquées et vérification fonctionnelle de programmes synchrones basées SAT/SMT (Rémi Delmas, ONERA)
  • Résumé: Dans cet exposé nous présenterons un panorama des applications de SAT et SMT conduites au DTIM pour l'assistance à la conception et à la vérification de systèmes embarqués, allant de la vérification de propriétés de safety pour des programmes synchrones écrits en lustre avec l'outil STUFF, à la synthèse de plans de câblage de poids minimal pour la connexion de capteurs au réseau avionique avec le langage eLogical et sa traduction en logique pseudo-booléenne, en passant par l'allocation de niveaux de DAL et de budgets de taux de défaillance aux composants d'un système avionique à partir d'informations issues d'analyses de safety (coupes minimales) et du profil d'utilisation de l'avion, à l'aide de solveurs SAT, pseudo-booléens et de programmation MILP.