Méthode formelle
La MÉTHODE B est une méthode de spécification formelle capable de retranscrire de manière rigoureuse les exigences d’un cahier des charges,
au moyen de preuves mathématiques, afin de prouver leurs cohérences.
CE PROCÉDÉ PERMET NOTAMMENT DE LEVER TOUTE AMBIGUÏTÉ SUR LES PROPRIÉTÉS INITIALEMENT EXPRIMÉES EN LANGAGES NATUREL.
LE LANGAGE B PEUT ÊTRE UTILISÉ SUR DES PROTOCOLES COMME SUR DE L’INFORMATIQUE EMBARQUÉE.
Télécharger notre brochure « Formal Methods in the Railways »
LA Méthode B
La méthode B englobe toute la modélisation par la preuve d’un système, de l’écriture de son modèles à son implantation logicielle, tout en respectant les données fondamentales d’origine.
FIABILITÉ, SÉCURITÉ
Bien que les usages de la méthode B soient divers (Modélisation d’un système, formalisation de spécification…) l’objectif est le même : s’assurer de la fiabilité, de la sécurité ainsi que de l’absence de bugs informatiques d’un système par des preuves mathématiques.
L’ATELIER B : DÉVELOPPEMENT DE LOGICIELS PROUVÉS
La méthode B tire sa légitimité du développement d’outils approuvés et utilisés à grande échelle, dans le monde industriel comme universitaire, tels que l’ATELIER B. CLEARSY est détenteur de ce dernier et se charge des évolutions et de la maintenance de sa plateforme de développement. L’Atelier B constitue ainsi une référence pour le développement de logiciels prouvés.
ÉTABLISSEMENTS ENSEIGNANT B EN FRANCE
• Université de Bordeaux 1
• Université de Belfort
• Université de Compiègne
• Université du Havre
• Université de Franche-Comté
• Université de la Rochelle
• Université de Limoges
• Université de Metz
• Université de Montpellier 2
• Université de Nancy 1
• Université de Nancy 2
• Université de Nantes
• Université de Paris 12
• Université de Rennes 1
• Université de Toulouse 3
• Université de Versailles
• CNAM IIE d’Evry
• CNAM de Paris
• CNAM de Poitiers
• ECOLE des Mines de Gardanne
• ECOLE des Mines de Nancy
• ECOLE Nationale Supérieure d’ingénieurs de Bourges
• ESIAL à Villiers les Nancy
• ENSI Bourges
• ENSIMAG de Grenoble
• ENSMA de Poitiers
• ENSSAT de Rennes
• Faculté des Sciences de Luminy à Marseille
• INP de Grenoble
• IUT de Nantes
• SUPELEC d’Evry
• CNAM IIE d’Evry
• CNAM de Paris
• CNAM de Poitiers
• ECOLE des Mines de Gardanne
• ECOLE des Mines de Nancy
• ECOLE Nationale Supérieure d’ingénieurs de Bourges
• ESIAL à Villiers les Nancy
• ENSI Bourges
• ENSIMAG de Grenoble
• ENSMA de Poitiers
• ENSSAT de Rennes
• Faculté des Sciences de Luminy à Marseille
• INP de Grenoble
• IUT de Nantes
• SUPELEC d’Evry
VÉRIFICATION FORMELLE DE SPÉCIFICATIONS
Grâce à notre expérience de la modélisation et à notre capacité à comprendre et à abstraire les besoins de nos clients, nous assistons les opérateurs, industriels et donneurs d’ordre dans leur tâche de vérification des spécifications et des cahiers des charges systèmes et logiciels.
La MÉTHODE B associée à d’autres formalismes est utilisée pour aider à analyser, valider, réorganiser et fournir les éléments qui permettent de compléter les spécifications et cahiers des charges.
Cette technique d’analyse de fiabilité des systèmes a la particularité d’être applicable à tous les domaines industriels. La validation formelle est ainsi utilisée aujourd’hui avec succès dans les domaines automobile, bancaire, spatial et nucléaire.
LES AVANTAGES DE LA VÉRIFICATION FORMELLE
LES BÉNÉFICES CONSTATÉS DE LA VALIDATION FORMELLE DE SYSTÈMES SONT :
• Une focalisation plus rapide sur les points difficiles
• Une synthèse fiable et justifiable
• Un questionnement direct et précis
• Des preuves de cohérences
• Une complétude atteignable
• La suppression de non-dits métier
• La prise en compte des aspects fonctionnels et dysfonctionnels.
POUR UN RETOUR SUR INVESTISSEMENT QUI S’APPRÉCIE EN TERMES DE :
• Diminution d’échecs tardifs
• Gains en validation (Testabilité améliorée)
• Convergence plus rapide (Qualité de réalisation)
• Amélioration de la capitalisation des connaissances logiciels prouvés.
