Forum Méthodes Formelles Cycle de conférences

"Le Model-Checking en action"

Toulouse Jeudi 16 Octobre 2014 Salle de Conférences LAAS-CNRS Plan d'accès Toulouse Accueil au LAAS-CNRS : Inscription par mail auprès de F. Decavele Pôle AESE

Retransmis en direct :

• Grenoble INRIA Minalogic : Informations & Inscription
• Saclay Labex Digicosme : Informations & Inscription

Programme

08h45 -09H00 Accueil des participants

09h00-09h05 « Courte introduction à la journée » Slides/Vidéo
Agusti Canals (CS Communication & Systèmes)

09h05-10h00 « Introduction au Model-Checking » Slides/Vidéo
Radu Mateescu (INRIA Grenoble)

10h00-11h00 FIACRE/TINA

• « Présentation de l’outil » Slides/Vidéo
  Bernard Berthomieu (LAAS-CNRS Toulouse)
• « Model checking temporisé, application à l’avionique » Slides/Vidéo
  Eric Jenn (THALES Avionics)

11h15 -11h30 : Pause Café

11h30-12h30 CADP

• « Présentation de l’outil  » Slides/Vidéo
  Hubert Garavel (INRIA Grenoble)
• « Application de CADP à la vérification de matériel » Slides (Video non disponible suite à un incident technique)
  Abderahman Kriouile et Massimo Zendri (STMicroelectronics)

12h30-14h00 Repas

14h00-14h45 Outil SYSTEREL Smart Solver

• « Présentation de l’outil »
  Nicolas Breton  (SYSTEREL) Slides/Vidéo
• « Utilisation de la preuve formelle par la RATP »
  Evguenia Dmitrieva (RATP) Slides/Vidéo

14h45-15h30 UPPAAL

• « Présentation de l’outil et de son application dans l'industrie » Slides/Vidéo
  Kim G. Larsen  (Aalborg University/UP4ALL)

15h30-16h00 Pause café

16h00-16h45 Retour d’expérience sur le model checking

• « Présentation des outils utilisés et leur application » Slides/Vidéo
  Mickael Dierkes (Rockwell Collins)

16h45-17h30 : Table Ronde animée par Mattéo Bordin (Adacore) Vidéo
« ROI sur le Model checking (reprenant les idées fortes exposées dans la journée) : les gains, à quels endroits du cycle de vie, les limites … »

home