Validation formelle de modèles logiciels

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.

Connaissance (même premier niveau) d’un langage de programmation de réseaux de processus, de la modélisation par automates d’états finis.

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.

Base

É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.