méthodes formelles

Vérification formelle de systèmes ou logiciels développés en SCADE, C, Ada

Systerel propose une gamme de solutions éprouvées industriellement pour l’analyse statique ou la preuve formelle de systèmes ou de logiciels à l’aide de technologies à base de Model Checking.

Systerel Smart Solver est un moteur d’analyse basé sur les technologies SAT.

Une large gamme de services

 

Associé à des traducteurs et outils spécialisés, Systerel Smart Solver offre une large gamme de services :

  • Analyse statique de code
  • Preuve de propriétés – certification
  • Preuve des propriétés définies par l’utilisateur avec outils d’analyse de contre-exemples
  • Génération automatique de tests (fonctionnels/structurels)

Synopsis

 

 

  1. Écriture de l’objet de l’analyse : propriétés de sécurité, objectifs de tests, critères d’optimisation…
  2. Modélisation sous forme de propriétés
  3. Traduction automatique du système en un modèle évaluable grâce à un traducteur spécialisé (C, Ada, SCADE…)
  4. Analyse du système et production des résultats (preuves, contre-exemples, tests…)

Avantages

  • Analyses et preuves automatiques
  • Complétude des analyses
  • Modélisation exacte (sans abstraction par rapport aux constructions du langage initial)
  • Conforme aux processus de certification
  • Équipe dédiée d’experts (technologie et outils)

Fonctionnalités

  • Analyse statique de code : absence de comportements non spécifiés (OOB, UMR, OVF, DIV0), absence de code mort
  • Preuve des propriétés définies par l’utilisateur
  • Analyse de contre-exemples de propriétés réfutées
  • Génération automatique de tests (fonctionnels ou structurels)
  • Preuve d’équivalence entre la spécification et le code ou entre différents codes

Langages : C (C99 avec restrictions), Ada (avec restrictions), SCADE (v5, v6)

Certifiable Systerel Smart Solver (cS3) logo_certifiable smart solver

  • Analyses certifiables de la conformité d’un système à un ensemble de propriétés (sécurité, spécification…)
  • Conforme à la norme EN 50128:2011, outil de classe T2 pour systèmes SIL4
  • Basé sur la diversification, la vérification de l’équivalence séquentielle et une vérification des preuves a posteriori

Applications industrielles

Vérification de sécurité pour de nombreux systèmes y compris :

  • Systèmes de poste à enclenchement (à base de relais et informatisés)
  • CBTC (Communication-Based Train Control System)
  • ERTMS (European Railway Traffic Management System)
  • Systèmes de régulation de débit d’air (avionique)

 

En savoir plus

Découvrez la présentation de Systerel Smart Solver lors du cycle de conférences sur les méthodes formelles au LAAS – CNRS, le 16 octobre 2014

 

Contactez-nous