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

Contactez-nous  Catalogue des formations

__

Systerel Smart Solver

__

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.