Le centre d’expertise « Modélisation formelle et preuve » de Systerel constitue l’une des plus importantes équipes européennes sur le sujet et dispose d’une expérience de plus de 25 ans dans la mise en œuvre industrielle des techniques formelles.

Utilisation des méthodes formelles

Pourquoi utiliser les méthodes formelles ?
Quelles techniques pour quelle problématique ?

Model Checking avec Systerel Smart Solver

Systerel utilise le Model Checking pour prouver des propriétés de sécurité d’artefacts du processus de développement de systèmes (spécification, conception, code, données) une fois les artefacts produits. Elle se base sur des modélisations/traductions dans le langage HLL et sur le moteur de preuve « Systerel Smart Solver » qui est un produit Systerel.

Méthode B logiciel

Systerel est l’un des leaders dans l’utilisation de la méthode B pour le développement de logiciels critiques dans un cadre industriel.

Vérification de données B OVADO²®

Systerel utilise la méthode formelle B OVADO²® afin de vérifier et de valider les données de configuration d’un système. Cette technique peut contribuer au Dossier de Sécurité du système demandé par les normes. Elle s’appuie sur l’outil OVADO²® propriété de la RATP et dont Systerel assure la distribution, la maintenance et les évolutions. L’outil permet également de générer des données.

Méthode B événementiel

Systerel utilise la méthode formelle B événementiel afin de prouver qu’un système respecte des propriétés de sécurité. Cette technique s’appuie sur la plate-forme RODIN dont Systerel assure la maintenance et les évolutions.

Modélisation SCADE

Systerel intervient sur des activités de conseil et d’expertise autour de la mise en œuvre de SCADE et de son couplage à d’autres technologies.

Langage HLL

Systerel utilise le langage HLL pour la vérification formelle de logiciels et systèmes critiques, tels que les CBTC, les postes de signalisation, les circuits logiques de contrôle-commande et tout autre usage nécessitant l’expression de contraintes à vérifier.

Outils de Vérification & Validation

Systerel a développé des solutions exploitant les méthodes formelles pour gagner en qualité et en productivité sur des activités de vérification et validation.