# 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

![The B method is composed of number of steps - each step is actionable as a Atelier B command.](https://1197517861-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2FjYhGiEkFHAcSNj4UKngj%2Fuploads%2F0nv5cz7xRibV8zFoV1WF%2Fb-method.png?alt=media\&token=afc9d4ad-a648-4a1a-bd15-c1b0a7059405)

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:

* *<mark style="color:orange;">the natural language requirements</mark>*: traceability and coverage between requirements and B models have to be checked by humans
* <mark style="color:orange;">the source code generated</mark>: 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).


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://b-method.gitbook.io/training-resources-for-atelier-b/guides-and-tutorials/applying-the-b-method.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.