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)

• 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)

Systerel Smart Solver est une solution de preuve performante. Elle permet d’accroître la confiance dans le niveau de sécurité d’un système tout en réduisant considérablement le temps et le coût de validation associés.

Les différentes mesures réalisées sur des projets de taille industrielle montrent des gains en performance significatifs sur la validation de propriétés de sécurité : des activités de validation qui demandaient plusieurs mois auparavant se font désormais en quelques heures.

L’application à une échelle industrielle de Systerel Smart Solver par de grands acteurs du ferroviaire (Hitachi, Alstom, RATP, SNCF…), et la démonstration, sur des cas représentatifs, de sa capacité à adresser la grande majorité du parc des postes actuellement déployés par la SNCF par exemple, confirment la maturité de mise en œuvre de la vérification formelle pour le développement et le déploiement de systèmes d’enclenchement opérationnels.

Par ailleurs, Systerel met à disposition des universitaires des licences Systerel Smart Solver à des fins d’expérimentations ou prototypages. L’ONERA utilise actuellement une licence Systerel Smart Solver.

Contactez-nous

En vidéo

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