🧑‍🎓
Training Resources for Atelier B
  • Introduction
  • Guides and Tutorials
    • Installation
    • Training Videos
    • Training Slides
    • Applying the B Method
      • Project Creation
      • Code Generation
      • Mathematical Proof
        • 🔥Writing Mathematical Rules
          • Introduction
          • Introduction to the Theory Language
          • How to write mathematical rules
          • Using Automatic Prover Mechanisms
          • Guards in a nutshell
          • Normalisation of Expressions
          • Common pitfall
          • All guards in the theory language
    • Extending Atelier B
      • Syntax
      • Examples
    • Programming the CLEARSY Safety Platform
  • Examples and Case-studies
    • Fuel Level
    • Switch
    • Security Policy
    • Verified Software Competitions
  • Additional Resources
    • Glossary
    • References
    • Frequently Asked Questions
Powered by GitBook
On this page
  • Introduction
  • The B Development Cycle

Was this helpful?

  1. Guides and Tutorials

Applying the B Method

PreviousTraining SlidesNextProject Creation

Last updated 3 years ago

Was this helpful?

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 - certification) and for system modeling (microelectronics - 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).

EN50158
Common Criteria
The B method is composed of number of steps - each step is actionable as a Atelier B command.