Vérification formelle de systèmes ou logiciels développés en SCADE, B, Ada
Systerel Smart Solver est une gamme de solutions éprouvées industriellement pour la preuve formelle de systèmes ou de logiciels, ainsi que la génération automatique de cas de tests à l’aide du Model Checking (technologie SAT) et du langage HLL.
Systerel Smart Solver est une solution de preuve performante, permettant de renforcer la confiance dans le niveau de sécurité d’un système tout en réduisant considérablement le temps de validation et les coûts associés.
Une large gamme de services
Associé à des traducteurs et outils spécialisés, Systerel Smart Solver offre une large gamme de services :
- Analyse de code : détection de comportements non spécifiés
- Preuve des propriétés définies par l’utilisateur
- Analyse de contre-exemples des éventuelles propriétés réfutées
- Génération automatique de tests (fonctionnels, structurels ou de conformité)
- Preuve d’équivalence entre différents artefacts d’un processus de développement
Langages : B, Ada (avec restrictions), SCADE (v5, v6), vos DSL
Avantages
- Analyses et preuves automatiques
- Complétude des analyses
- Modélisation exacte (sans abstraction par rapport aux constructions du langage initial)
- Certificat T2 selon la norme EN50128:2011 et processus de mise en œuvre associé dans le cadre de développements jusqu’à SIL4
- Équipe dédiée d’experts (technologie, langage et outils)
Synopsis
- Expression en langage naturel de l’objet de l’analyse : propriétés de sécurité, objectifs de tests, critères d’optimisation…
- Formalisation sous forme de propriétés en langage HLL
- Traduction automatique du système en un modèle évaluable grâce à un traducteur spécialisé (B, Ada, SCADE, votre DSL…)
- Analyse du système et production des résultats (preuves, contre-exemples, tests)
Langages : C (C99 avec restrictions), Ada (avec restrictions), SCADE (v5, v6)
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)
Les mesures réalisées sur des projets de taille industrielle montrent des gains de temps 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’utilisation Systerel Smart Solver par de grands acteurs de l’industrie ferroviaire tels qu’Alstom, Hitachi, RATP, SNCF ou encore Thales, ainsi que la démonstration, de sa capacité à adresser la grande majorité du parc des postes actuellement déployés par la SNCF, illustrent la maturité de mise en œuvre de la vérification formelle dans le développement et le déploiement de systèmes d’enclenchement opérationnels.
Notre Offre
Licences
Nous proposons une offre annuelle progressive incluant un périmètre d’outils et la maintenance associée.
Par ailleurs, Systerel met à disposition des universitaires des licences Systerel Smart Solver à des fins d’expérimentations ou prototypages. Le CEA-List et l’ONERA font partie des établissements académiques ayant bénéficié de ce type de licence.
Consulting
Création de solutions clé en main intégrant Systerel Smart Solver au sein de leur processus industriel.
Réalisation de modèles de propriété et d’environnement, mise au point de la preuve.
Génération de tests de conformité B2BT depuis un modèle HLL.
Formation
Vous souhaitez renforcer vos compétences dans la mise en œuvre et ses applications ? Nous proposons une formation concrète, illustrée par des exemples et des exercices, permettant une mise en de œuvre concrète de Systerel Smart Solver en milieu industriel. Découvrir notre programme de formation.
De plus, Systerel est à même de concevoir une formation sur mesure, en fonction de vos besoins spécifiques.
Ils ont fait confiance à Systerel
