Formal Method
The B Method is a formal specification method capable of rigorously transcribing the requirements of a specification,
by means of mathematical proofs, in order to prove their coherence.
THIS PROCESS ALLOWS TO REMOVE ANY AMBIGUITY ON THE PROPERTIES INITIALLY EXPRESSED IN NATURAL LANGUAGES.
THE B LANGUAGE CAN BE USED ON PROTOCOLS AS WELL AS ON EMBEDDED COMPUTING.
The B Method
The B Method encompasses all the proof modelling of a system, from the writing of its model to its software implementation, while respecting the original fundamental data.
RELIABILITY, SECURITY
Although the uses of the B Method are diverse (modelling a system, formalising a specification, etc.), the objective is the same: to ensure the reliability, safety and absence of computer bugs of a system through mathematical proofs.
THE ATELIER B: DEVELOPING PROVEN SOFTWARE
The B Method draws its legitimacy from the development of approved tools used on a large scale in the industrial and academic world, such as Atelier B. CLEARSY is the owner of the latter and is responsible for the evolution and maintenance of its development platform. Atelier B is thus a reference for the development of proven software.
SCHOOLS TEACHING B IN 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
FORMAL VERIFICATION OF SPECIFICATIONS
With our experience in modelling and our ability to understand and abstract our clients’ needs, we assist operators, manufacturers and clients in the verification of system and software specifications.
The B Method is used in combination with other formalisms to help analyse, validate, reorganise and provide the elements that complete the specifications.
This technique of system reliability analysis has the particularity of being applicable to all industrial fields. Formal validation is successfully used today in the automotive, banking, space and nuclear fields.
THE BENEFITS OF FORMAL VERIFICATION
THE BENEFITS OF FORMAL SYSTEMS VALIDATION ARE
– Faster focus on difficult issues
– A reliable and justifiable synthesis
– Direct and precise questioning
– Evidence of consistency
– Achievable completeness
– Removal of unspoken business issues
– Consideration of functional and dysfunctional aspects.
FOR A RETURN ON INVESTMENT THAT CAN BE APPRECIATED IN TERMS OF
– Reduction in late failures
– Gains in validation (improved testability)
– Faster convergence (quality of implementation)
– Improved capitalisation of proven software knowledge.
