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é, etc.
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 ?
Conférences dédiées aux méthodes formelles
Systerel intervient régulièrement dans plusieurs conférences et workshops spécialisés dans les méthodes formelles, en France comme à l’international.
La société a participé au Forum Méthodes Formelles du LAAS‑CNRS à Toulouse, au NII Shonan Meeting organisée par l’Institut National d’Informatique du Japon, à la conférence ABZ sur les méthodes formelles d’état, qui réunit une communauté internationale, ainsi que des workshops autour de la plateforme RODIN.
Ces participations témoignent de l’engagement de Systerel à contribuer aux échanges scientifiques et à l’évolution des pratiques dans le domaine des méthodes formelles.