Validation formelle de modèles logiciels

Durée Date Lieu Tarif Nombre de participants Niveau
3 jours Du 15 au 17 mai 2017 ENSTA Bretagne
(Brest)
 1 370 ¤* de 3 à 12  base

*Prix par personne, net de taxe

Objectifs

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 « modelchecking ». 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 oeuvre.

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.

Niveau du stage

Base : a pour objectif l’acquisition de connaissances théoriques et/ou pratiques de base dans le domaine traité.

Pédagogie

Le stage comporte des séances de cours
illustrées par de nombreux exercices et travaux pratiques sur machine (PC).

Documents fournis aux stagiaires

Supports de cours (polycopié, sujets et corrigés des travaux pratiques).

Dispositif d'évaluation

Evaluation à 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.

Equipements

Ordinateurs type PC et microC-OSII fournis pour le stage.

 

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-CD
  • 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 – Responsable du pôle STIC de l’ENSTA Bretagne. Spécialiste en modélisation et validation formelle de logiciels embarqués.

Contact

Cet e-mail est protégé contre les robots collecteurs de mails, votre navigateur doit accepter le Javascript pour le voir ,
Responsable formation continue
Tél : 02 98 34 89 74
Fax : 02 98 34 87 90