ENSTA Bretagne : Systèmes Numériques et Sécurité

Validation formelle de modèles logiciels

ENSTA Bretagne Formation Continue référençable (Datadock)

Détails de formation

#Sciences et Technologies de l’Information et de la Communication
Objectifs
L’objectif du stage est une initiation à la modélisation formelle de logiciels et la vérification de propriétés sur ces modèles. La technique développée durant ce stage est basée sur la vérification de modèles dit « model-checking ». Les langages formels UPPAAL et FIACRE seront utilisés en guise d’illustration des concepts sur des cas d’étude et les outils de vérification UPPAAL (http://www.uppaal.com) et OBP-CDL (http://www.obpcdl.org) mis en œuvre.
La formation comporte un apprentissage :
- des concepts de modélisation formelle de logiciels basés sur des réseaux de processus communicants.
- des formalismes de modélisation formelle utilisés : langages UPPAAL et FIACRE : présentation des deux formalismes, édition des modèles, simulation, illustration sur des cas d’étude industriels.
- des principes de vérification formelle d’exigences sur les modèles : présentation des logiques formelles temporelles, langage d’observation, formalisation et vérification des propriétés, illustration sur de nombreux exemples.
Prérequis
Connaissance (même premier niveau) d’un langage de programmation de réseaux de processus, de la modélisation par automates d’états finis.
Pédagogie
Le stage comporte des séances de cours illustrée par de nombreux exercices et travaux pratiques sur machine (PC).
La journée de cours se déroule de 8h30 à 12h00 et 13h30 à 17h00.
Niveau du stage
Base
Dispositif d'évaluation
Évaluation à chaud en fin de formation par les stagiaires. Transmission au client, du compte-rendu d’évaluation et des feuilles d’émargement en complément de la facturation. Les attestations de stage sont remises directement aux stagiaires à la fin de la session de formation. Les stagiaires ou le responsable Formation Continue sont susceptibles de recevoir par mail, un « questionnaire de satisfaction à froid » quelques mois après le déroulement de la formation.
Programme détaillé
  • Introduction sur les méthodes formelles : enjeux, objectifs, difficultés et perspectives.
  • Principe des modèles à processus communicants (rappel)
  • Concepts de la vérification de propriétés sur des modèles à processus communicants (temporisés ou non), model-checking.
  • Modélisation UPPAAL, simulation et  validation sur outil UPPAAL.
  • Modélisation FIACRE, Modélisation CDL, simulation, validation sur outil OBP-CDL.
  • Présentation de logiques temporelles (linéaires type LTL et arborescentes type CTL)
  • Concepts des automates observateurs 
  • Formalisation de propriétés : formules logiques et observateurs
  • Vérification formelle de propriétés
Responsable de la formation et équipe pédagogique
Philippe Dhaussy
Enseignant-chercheur,
Membre de l'équipe MOCS, du laboratoire Lab-STICC, UMR CNRS 6285

contact

Catherine Le Lagadec
Enseignante
Responsable de la formation continue
02 98 34 88 24