model checking

Systerel propose une gamme de solutions éprouvées industriellement pour l’analyse statique ou la preuve formelle de systèmes ou logiciels à l’aide de technologies à base de Model Checking.
Systerel Smart Solver (S3) est un moteur d’analyse basé sur les technologies SAT. Ce moteur est notamment utilisé dans le cadre des vérifications de sécurité pour de nombreux systèmes, notamment dans les domaines ferroviaire ou aéronautique.

La formation est étayée d’exemples et d’exercices permettant une mise œuvre concrète de Systerel Smart Solver en milieu industriel.

Objectifs

  • Acquérir des notions de model-checking
  • Savoir bâtir un modèle formel du système à vérifier
  • Apprendre à mettre en œuvre Systerel Smart Solver pour vérifier le comportement d’un système
  • Comprendre comment s’inscrit Systerel Smart Solver dans un processus certifiable

Pré-requis

  • Première expérience d’un langage de programmation
  • Connaissance des principes de modélisation
  • Connaissance de base en informatique et en mathématiques

Programme sur 2 jours

  • Introduction au Model Checking
  • Principe du langage HLL
  • Principes de modélisation avec HLL
  • Les outils de Systerel Smart Solver et leurs utilisations
  • Présentation d’un processus certifiable avec Systerel Smart Solver

Évaluation

Des questionnaires seront établis en début et en fin de formation afin d’évaluer les acquis.

Systerel Smart Solver

Modalités et contactCatalogue des formations

 

__

Activité enregistrée sous le numéro 93 13 12834 13 auprès du préfet de région Provence-Alpes-Côte d’Azur.