Atelier B Resources

This is an open-source repository for Atelier B. It covers both software development with B and the B method, and system modelling with Event-B. It contains a number of useful resources to operate the Atelier B formal tool to model, verify by proof, and to generate C source code.

Table of Contents

• Resources for Atelier B
  • Front matter
  • Preface
  • Glossary
• Part I: Introduction to Atelier B
  • 1 Introduction to B and Event-B
  • 2 Getting your hands dirty
• Part II: Modelling with B
  • 10 Introduction to B
  • 11 The B Method
  • 12 Files Architecture
  • 13 Example: Fuel Level
  • 14 Example: Switch
• Part III: Modelling with Event-B
  • 20 Introduction to Event-B
  • 21 Example: Security Policy
• Part IV: Proving with Atelier B
  • 30 Introduction to Mathematical Proof
  • 31 Writing Mathematical Rules
• Part V: Generating Code with Atelier B
  • 40 Introduction to Code Generation
• Part VI: The Rest of B
  • references
  • troubleshooting

The B Files

These files are the ones used in this repository. To use them, first create a project (software development ou system modelling as required), then open the project, right click and select "add components". Navigate to the directory where you have downloaded the B files. Select the files you wanted to import. Click OK. The files are attached to your project.

The B code files are listed here:

CH	Filename	Description
21	politique.sys	Test

Running the Code

There is a collection of source code files, duplicating the code in the text of this site.

• You will need the latest Atelier B Community Edition. Examples have designed with Atelier B 4.7.1 (and later): results are not guaranteed if an older version is used instead.