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
- ABZ 2018 – from 5th au 8th June 2018 – Southampton, United Kingdom
- AFADL – GDR GPL: CLEARSY will give a presentation on the integration of third-party tools for automatic proof in Atelier B
- AI4FM 2011
- Double-Core SIL4 Architecture Presented During Open Source Innovation Spring (Paris)
- Atelier B 3.7
- Atelier B 3.7.1
- CLEARSY Saftey Platform 4.5.4 tool available
- Brama available in beta 1 version
- CLEARSY attended the SMBF 2007 Conference in Brazil
- CLEARSY participated in the prestigious International Conference on Formal Methods, FM 2015
- 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 attends the third world congress on formal methods: FM’19 from 7 ou 10 october 2019
- CLEARSY Safety Platform Handbook available
- CLEARSY Safety Platform presented at IFRN Parnamirim
- CLEARSY Safety Platform exhibited at conference RSSR 2019
- CLEARSY Safety Platform presented at Industry Day 2018
- CLEARSY Safety platform SK0 is on sale
- “B Dissemination Day 2008” Seminar in Brazil
- Composys, version 1.6
- B2007 Conference
- Nantes 2010 Conference : “From Research to Teaching Formal Methods – the B Method”
- Conference on formal methods – Oxford
- International Symposium on Software Reliability Engineering
- Talk at the conference SBMF 2017
- MASTER 2 course given at UFRN/IMD
- CSSP presented at Workshop on Software Development Technology
- Tutorial doctoral School ETMF 2017
- CLEARSY meets future users of CLEARSY Safety Platform on a worldwide tour.
- New version of Atelier B for Mac-OS
- Formal methods for cyber-physical systems – Shonan
- Hands-on session at IFRN Parnamirim
- Hands-on session at UFF Niteroi
- Computer Science seminar in Montreal/Canada
- Technical seminar Newcastle University
- Tutorial conference RSSR 2017
- Formal methods in action in the railways
- CLEARSY opened an office in Canton, Connecticut
- 19th Brazilian Symposium of Formal Methods
- CLEARSY organizes the first annual Meeting of the European H2020 Project INTO-CPS, on the 18th and 19th of November 2015 in Marseille.
- Engineering Complex Preponderant Software Systems Seminar in Toulouse
- Newcastle University Technical Seminar
- Dagstuhl Seminar 2013
- 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
- New Version of B4Free
- B4free as a free-fo-all tool
- RIMEL Project
- Collaboration with Labsoc
- Verification of the Coherence of the UML – ENST PA
- Globalplatform card specification v2.1.1
- RODIN: a three year Project
- CLEARSY IS PARTICIPATING TO THE INTERNATIONAL CONFERENCE ABZ 2021
- The new formal tool Atelier B 4.7 is available.
- Two decades of industrial exploitation of the B formal method.
- CLEARSY realizes the formal proof of the Control – Command – Signalling system of the HPMV project.
- Formal activities through the V cycle
Linked to this thematic