> For the complete documentation index, see [llms.txt](https://b-method.gitbook.io/training-resources-for-atelier-b/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://b-method.gitbook.io/training-resources-for-atelier-b/guides-and-tutorials/applying-the-b-method.md).
# Applying the B Method
## Introduction
The B Method is a method of software development based on the B language. Based on an abstract machine notation and industry-strenght tool, it is used in the development of computer software. The B Method allows:
* to write specification models and to verify their correctness by proof
* to write (intermediate or final) refinements, to verify their correctness and their compliancy with their specification
* to check that final refinements, also called implementations, comply with implementability rules (also called B0 compliancy - B0 being the subset of B used only for implementation)
* to generate source code (C for Atelier B Community version, Ada for the Maintenance version) from implementation models.
Atelier B is the tool implementing the B Method. It has been qualified with the release of the parisian automatic metro line 14 in 1998. Version 4.7 is going to be certified in 2022.
Atelier B comes with a number of tools and features enabling an industrial use for certified applications, both for software development (mainly railway industry - [EN50158](https://standards.globalspec.com/std/14317747/EN%2050128) certification) and for system modeling (microelectronics - [Common Criteria](https://en.wikipedia.org/wiki/Common_Criteria) certification).
## The B Development Cycle
The B Method is composed of 3 main phases:
* the project management and the modeling
* the proof of the models
* the code generation
A B project is considered correct only when all proof obligations have been proved.
Proof and code generation are independent. Source code could be generated even if a B project is not demonstrated at 100%. Of course, such a source code comes with no garanty at all.
The proof is related to the B models, not to:
* *the natural language requirements*: traceability and coverage between requirements and B models have to be checked by humans
* the source code generated: code generator is not formally developed and proved - so other means are required to ensure a safe execution like software (and possibly hardware) diversity with the use of two different code generators and a runtime verification of their execution with a voter (2 out of 2 architecture).