
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.
De plus, 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.
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.
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.

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

Liés à cette thématique
- ABZ 2014 – Du 2 au 6 juin à Toulouse
- ABZ 2018 – Du 5 au 8 juin 2018 à Southampton, Royaume-Uni
- AFADL – GDR GPL : CLEARSY fera une présentation sur l’Intégration d’outils tiers de preuve automatique dans l’Atelier B
- AI4FM 2011
- Architecture bi-processeur SIL4 présentée au Forum IFSTTAR « Sûreté et sécurité dans les transports »
- Architecture bi-processeur SIL4 présentée au Printemps de l’Innovation Open Source
- Atelier B 3.7
- Atelier B 3.7.1
- Atelier CLEARSY Safety Platform 4.5.4 disponible
- B4Free
- Brama disponible en version beta 1
- CLEARSY à la Conférence SBMF 2007 au Brésil
- CLEARSY a participé à FM 2015, conférence internationale relative aux méthodes formelles
- CLEARSY a participé à la conférence Formal Methods 2015
- CLEARSY organise un séminaire technique à l’Université de Sherbrooke (Québec) le jeudi 20 octobre 2016 de 10h30 à 12h.
- CLEARSY présente le projet LCHIP au congrès Lambda Mu de la Maîtrise des Risques – 13 oct à St Malo
- CLEARSY participe au troisième congrès mondial sur les méthodes formelles: FM’19 du 7 au 10 octobre 2019
- CLEARSY Safety Platform Handbook disponible
- CLEARSY Safety Platform présentée à IFRN Parnamirim
- CLEARSY Safety Platform présentée à la conférence RSSR 2019
- CLEARSY Safety Platform présentée pendant l’Industry Day 2018
- CLEARSY Safety platform SK0 est en vente
- Colloque « B Dissemination Day 2008 », au Brésil
- Composys, version 1.6
- Conférence B2007
- Conférence de Nantes 2010 : “La Méthode B, de la Recherche à l’Enseignement”
- Conférence Formal Methods – Oxford
- Conférence internationale SBMF 2017
- Conférence ISSRE 2016
- Conférence SBMF
- Cours de master 2 pour l’UFRN/IMD
- CSSP présentée au Workshop on Software Development Technology
- École Doctorale ETMF
- Engineering Complex Preponderant Software Systems Seminar in Toulouse
- Nouvelle version de l’Atelier B pour Mac-OS
- Méthodes formelles et systèmes cyber-physiques – Séminaire à Shonan
- Travaux pratiques à IFRN Parnamirim
- Travaux pratiques à UFF Niteroi
- Séminaire d’informatique à Montréal/Canada
- Séminaire technique à l’université de Newcastle
- Tutoriels organisés pour des chercheurs et des ingénieurs de l’industrie
- Tutoriel conférence RSSR
- Les méthodes formelles appliquées au ferroviaire
- Projet LCHIP et architecture double processeur: premier starter kit
- CLEARSY s’installe aux Etats-Unis
- 19ème conférence brésilienne sur les méthodes formelles
- CLEARSY recevra les 18 et 19 novembre 2015 la première rencontre annuelle du projet européen H2020 INTO-CPS.
- Séminaire ISCLP – Ingénierie des Systèmes Complexes à Logiciels Prépondérants
- Séminaire technique à l’Université de Newcastle
- Séminaire Dagstuhl 2013
- Enseignement des Méthodes Formelles à l’ENSI de Bourges
- Enseignement des Méthodes Formelles à l’École des Mines de Gardanne en 2010
- Nouvelle version de B4Free
- Version gratuite de l’outil B4Free
- Projet RIMEL
- Collaboration avec Labsoc
- AFADL’06
- Vérification de la cohérence de modèles UML – ENST
- Globalplatform card specification v2.1.1
- RODIN : un projet de 3 ans
- CLEARSY PARTICIPE À LA CONFÉRENCE INTERNATIONALE ABZ 2021
- Assigning safe processing to meanings
- Le nouvel Atelier B 4.7 est disponible.
- Deux décennies d’application industrielle de la méthode formelle B.
- CLEARSY réalise la preuve formelle du système Contrôle – Commande – Signalisation du projet HPMV.
- Les activités formelles dans le cycle en V
Liés à cette thématique
Liés à cette thématique