Documents

 Introduction

This repository contains Atelier B manuals, several reports and papers on the B method as well as some outdated resources.

Atelier B manuals

Atelier B 4.0

  • User Manual of Atelier B 4.0 [En] [Fr]
  • B Language Reference Manual [En] [Fr]
  • B Language User Manual [En] [Fr]
  • B Symbols [En] [Fr]
  • Type Checker Messages [En] [Fr]
  • Reusable Components Reference [En] [Fr]
  • Proof Obligations Reference [En] [Fr]
  • BART GUI User Manual [En]
  • BART User Manual [En]
  • Mathematical Rules Writing [Fr]

Atelier B 3.7.2 or Previous Version

  • Administrator Manual [En] [Fr]
  • Mdelta User Manual [En] [Fr]
  • Model Editor [En] [Fr]
  • Prover Reference Manual [En] [Fr]
  • Prover User Manual [En] [Fr]
  • Translators User Manual [En] [Fr]
  • Prover Reference Manual [En] [Fr]
  • User Manual [En] [Fr]
  • Xemacs Interface User Manual [En] [Fr]

Articles and reports on the B method

  • Applying a Formal Method in Industry: a 15-year trajectory (T. Lecomte) [En]
  • Ten Years Disseminating the B Method (T. Lecomte) [En]
  • MATISSE project Handbook
    • Board-level Storyboard [En]
    • Project Manager’s Handbook for Systems Construction [En]
    • Practitioners Hanbook [En]
  • Introducing Dynamic Constraints in B (J.R. ABrial, L. Mussat) [En]
  • Event-B Applied to Railways
    • Safe and Reliable Metro Platform Screen Doors Control/Command Systems (T. Lecomte) [En]
    • Formal Methods in Safety-Critical Railway Systems (T. Lecomte, T. Servat, G. Pouzancre) [En]
  • Event-B Applied to Car Diagnosis
    • How to diagnose a modern car with a formal B model? (G. Pouzancre) [En]
    • Modélisation en B événementiel des fonctions mécaniques, électriques et informatiques d’un véhicule (G. Pouzancre, JP. Pitzalis) [Fr]
    • Les Principes de Fonctionnement Formalisés (G. Pouzancre) [Fr]

Outdated resources

These resources are provided for historical reasons.

  • Cash Dispensing Machine [En] [Fr]
  • Building Access Control [En] [Fr]
  • Identikit Management System [Fr]