The B METHOD is a method of formal specification capable of rigorously re-transcribing the requirements of a set of specifications, by means of mathematical proofs, in order to prove their data consistency. This process is especially useful for removing any ambiguity in the properties initially expressed in natural language.
The B language can be used in protocols as well as in embedded computing. Moreover, the B method encompasses all modelling by the proof of a system, from the writing of its model to the installation of its software.
Although the uses of the B method are diverse (modelling of a system, formalisation of specifications …) the aim is the same: to use mathematical proofs to ensure the reliability and security of a system and to make sure that there are no computer bugs in the system.
The B method draws its legitimacy from the development of approved tools, which are used on a large scale both in the world of industry and in the university sphere, such as Atelier B. CLEARSY is the holder of Atelier B and is responsible for its development and for the maintenance of its development platform. Atelier B therefore constitutes a reference for the development of proven software.
Formal verification of specifications
Due to our experience in modeling and our ability to understand and abstract our clients’ needs, we are able to support operators, industry and originators in verifying specifications for systems and software.
The B Method, associated with other formalisms, is used to analyze, validate, reorganize and provide elements that may complete specifications.
This approach is applicable to every industrial sector. Today, it is used successfully in the automotive, bank, space and nuclear sectors.
Advantages of the formal verification
The advantages observed are :
- A more rapid focus on difficult areas
- Reliable and justifiable summary
- Direct and precise questionning
- Proof of coherence
- Achievable completeness
- Elimination of professional “unsaids requirements”
- Consideration of functional and dysfunctional aspects
For a return on investment that is positive in terms of:
- Decrease iin delayed features
- Gains in validation (Improved testability)
- More rapid convergence (Realization quality)
- Greater capitalization of knowledge
Linked to this thematic
- • CLEARSY and UFRN make cooperation agreement to promote international internships.
- • The formal development tool ATELIER B passes 10,000 downloads!
- • Extension of Line 14 of the Paris Metro: over 25 years of reliability thanks to the B formal method
- • Exciting News: Atelier B Community Edition 24.04 Available!
- • The White House highlights the use of formal methods in a new report.
- • 9ᵉ ABZ International Formal Methods Conference in Nancy from May 31 to June 2, 2023
- • Why does the Baseline 3.6.0 ETCS standard require a SIL2 DMI (train display)?
- • L’Atelier B Professional Edition 23.02 est disponible
- • A certified version of ATELIER B is planned for 2024
- • Formal activities through the V cycle
- • CLEARSY realizes the formal proof of the Control – Command – Signalling system of the HPMV project.
- • Two decades of industrial exploitation of the B formal method.
- • The new formal tool Atelier B 4.7 is available.
- • CLEARSY IS PARTICIPATING TO THE INTERNATIONAL CONFERENCE ABZ 2021
- • New version of Atelier B for Mac-OS
- • CLEARSY attends the third world congress on formal methods: FM’19 from 7 ou 10 october 2019
- • CLEARSY Safety Platform Handbook available
- • CLEARSY Saftey Platform 4.5.4 tool available
- • AFADL – GDR GPL: CLEARSY will give a presentation on the integration of third-party tools for automatic proof in Atelier B
- • CLEARSY Safety Platform exhibited at conference RSSR 2019
- • CLEARSY meets future users of CLEARSY Safety Platform on a worldwide tour.
- • CLEARSY Safety platform SK0 is on sale
- • CSSP presented at Workshop on Software Development Technology
- • CLEARSY Safety Platform presented at Industry Day 2018
- • ABZ 2018 – from 5th au 8th June 2018 – Southampton, United Kingdom
- • Conference on formal methods – Oxford
- • Hands-on session at IFRN Parnamirim
- • CLEARSY Safety Platform presented at IFRN Parnamirim
- • MASTER 2 course given at UFRN/IMD
- • Hands-on session at UFF Niteroi
- • Computer Science seminar in Montreal/Canada
- • Technical seminar Newcastle University
- • Formal methods for cyber-physical systems – Shonan
- • Talk at the conference SBMF 2017
- • Tutorial doctoral School ETMF 2017
- • Tutorial conference RSSR 2017
- • Formal methods in action in the railways
- • CLEARSY organizes a technical seminar that will take place at Sherbrooke University, October 20, 2016 (from 10h30 to 12h).
- • LCHIP project (Low Cost High Integrity Platform) will ease development of safety critical systems and software up to SIL4, the highest Safety Integrated Level.
- • CLEARSY opened an office in Canton, Connecticut
- • International Symposium on Software Reliability Engineering
- • 19th Brazilian Symposium of Formal Methods
- • Double-Core SIL4 Architecture Presented During Open Source Innovation Spring (Paris)
- • CLEARSY organizes the first annual Meeting of the European H2020 Project INTO-CPS, on the 18th and 19th of November 2015 in Marseille.
- • CLEARSY participated in the prestigious International Conference on Formal Methods, FM 2015
- • Engineering Complex Preponderant Software Systems Seminar in Toulouse
- • Newcastle University Technical Seminar
- • Dagstuhl Seminar 2013
- • AI4FM 2011
- • Nantes 2010 Conference : “From Research to Teaching Formal Methods – the B Method”
- • Teaching of the Formal Methods at the Bourges École nationale supérieure d’ingénieurs (ENSI de Bourges)
- • Teaching Formal Methods at the Ecole des Mines of Gardanne in 2010
- • “B Dissemination Day 2008” Seminar in Brazil
- • Atelier B 3.7.1
- • Atelier B 3.7
- • New Version of B4Free
- • CLEARSY attended the SMBF 2007 Conference in Brazil
- • Brama available in beta 1 version
- • Composys, version 1.6
- • B4free as a free-fo-all tool
- • B2007 Conference
- • RIMEL Project
- • Collaboration with Labsoc
- • AFADL’06
- • Verification of the Coherence of the UML – ENST PA
- • Globalplatform card specification v2.1.1
- • RODIN: a three year Project
- • B4Free
Linked to this thematic
Linked to this thematic
