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.