Hautement recommandées dans le cadre de développement exigeant un haut niveau de sécurité, les méthodes formelles apportent :
- Une rentabilité plus élevée : réduction des coûts et des délais
- Une meilleure qualité du logiciel
- Des composants logiciels plus faciles à réutiliser et plus fiables
Les méthodes formelles permettent de répondre aux besoins de certification des logiciels critiques en assurant la fiabilité et l’absence de dysfonctionnement d’un système ou d’un logiciel.
Les applications dans de multiples domaines industriels sont possibles : analyses de sûreté de fonctionnement de systèmes critiques embarqués, évaluation des performances temporelles d’un système temps réel distribué,…
Techniques et outils
- la méthode B pour le développement de logiciels critiques
- le B système (Event-B) pour la modélisation de systèmes et la réalisation d’une preuve de leur sécurité
- les techniques de Model Checking basées sur SAT pour la vérification de systèmes réactifs
- les outils SCADE, Control-Build ou Simulink pour la modélisation de systèmes de contrôle-commande
- les techniques de validation formelle de données critiques
Ses expertises sont valorisées à travers le développement d’outils spécifiques adaptables aux besoins de ses clients (Systerel Smart Solver, Systerel IXL Builder, OVADO²®).
Quelles techniques pour quelle problématique ?
Cycle de conférences sur les méthodes formelles
Systerel fait partie du comité de programme et intervient régulièrement dans le cadre du cycle de conférences « Forum Méthodes Formelles » au LAAS-CNRS à Toulouse.
Systerel Smart Solver – octobre 2014
==
Les méthodes formelles dans l’industrie aujourd’hui – octobre 2014
===
La RATP, acteur essentiel de la promotion des méthodes formelles dans le ferroviaire – octobre 2014