Sites Inria

Forum Méthodes Formelles

Le Model-Checking en action

Cockpit Airbus A350 © Airbus

Le prochain Forum Méthodes Formelles sera retransmis le 16 octobre 2014 de 8h45 à 17h30 à Inria Grenoble - Rhône-Alpes. Ce forum est un cycle de conférences créé par le pôle Aerospace Valley afin de sensibiliser les entreprises aux méthodes formelles pour la conception de systèmes et de logiciels sûrs, en diffusant l'expérience acquise en ce domaine par les grands acteurs de l'aéronautique et de l'espace.

  • Date : 16/10/2014
  • Lieu : Inria Grenoble - Rhône-Alpes
  • Organisateurs : Cette conférence est organisée par Aerospace Valley et Minalogic, et accueillie par Inria Grenoble Rhône-Alpes.

Après les trois journées précédentes (respectivement consacrées à un panorama des méthodes formelles, puis à l'analyse statique et à la preuve), cette quatrième journée abordera le thème du model checking qui, avec l'analyse statique et les techniques de preuve, constitue un autre pilier des méthodes formelles (voir le diagramme ci-dessous, dû à Xavier Leroy).

Cette journée comportera un exposé général d'introduction au model checking, suivi de la présentation de quatre outils de model checking utilisés dans l'industrie. Elle se clôturera par un débat autour d'une table ronde.

Cette conférence est organisée par Aerospace Valley et Minalogic et accueillie par Inria Grenoble - Rhône-Alpes.

Pour la première fois, cette conférence sera également diffusée en direct à Saclay, ce qui témoigne de l'intérêt grandissant pour le Forum Méthodes Formelles.

Programme

  • Présentation de la journée par 
Frédéric Lang (Inria Grenoble - Rhône-Alpes) et Guillaume Saint-Marcoux (Minalogic)
  • Courte Introduction à la journée, 
Agusti Canals (CS Communication & Systèmes)
  • Introduction au Model-Checking,
 Radu Mateescu (Inria Grenoble - Rhône-Alpes)
  • FIACRE/TINA
    • Model checking temporisé, application à l'avionique
      
Eric Jenn (THALES Avionics)
  • CADP 
    • Présentation de l'outil
      Hubert Garavel (Inria Grenoble - Rhône-Alpes)
    • Application de CADP à la vérification de matériel
      
Abderahman Kriouile et Massimo Zendri (STMicroelectronics)
  • Outil Systerel Smart Solver
    • Présentation de l'outil
      
Nicolas Breton (SYSTEREL)
    • Utilisation de la preuve formelle par la RATP
      Evguenia Dmitrieva (RATP)
  • UPPAAL
    • Présentation de l'outil et de son application dans l'industrie
      
Kim G. Larsen (Aalborg University/UP4ALL)
  • Retour d'expérience sur le model checking
    • Présentation des outils utilisés et leur application
      
Mickael Dierkes (Rockwell Collins)

Retrouvez le programme détaillé sur

lire la suite

Keywords: Systèmes critiques Minalogic Preuve Méthodes formelles Aerospace Valley

Haut de page

Suivez Inria tout au long de son 50e anniversaire et au-delà !