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]