Atelier B

Developed by ClearSy, Atelier B is an industrial tool that allows for the operational use of the B Method to develop defect-free proven software (formal software). Two versions are available: Community Edition available to anyone without any restriction, Maintenance Edition for maintenance contract holders only. It is used to develop safety automatisms for the various subways installed throughout the world by Alstom and Siemens, and also for Common Criteria certification and the development of system models by ATMEL and STMicroelectronics. Additionally, it has been used in a number of other sectors, such as the automotive industry, to model operational principles for the onboard electronics of three car models. Atelier B is also used in the aeronautics and aerospace sectors.


References in zbMATH (referenced in 15 articles )

Showing results 1 to 15 of 15.
Sorted by year (citations)

  1. Halmagrand, Pierre: Soundly proving B method formulæusing typed sequent calculus (2016)
  2. Vekris, Dimitris; Lang, Frédéric; Dima, Catalin; Mateescu, Radu: Verification of $\mathrmEB^3$ specifications using CADP (2016)
  3. Vekris, Dimitris; Dima, Catalin: Efficient operational semantics for $EB^3$ for verification of temporal properties (2013)
  4. Jacquel, Mélanie; Berkani, Karim; Delahaye, David; Dubois, Catherine: Tableaux modulo theories using superdeduction. An application to the verification of B proof rules with the Zenon automated theorem prover (2012)
  5. Jacquel, Mélanie; Berkani, Karim; Delahaye, David; Dubois, Catherine: Verifying B proof rules using deep embedding and automated theorem proving (2011)
  6. Leuschel, Michael; Massart, Thierry: Efficient approximate verification of B and Z models via symmetry markers (2010)
  7. Attiogbé, J.Christian: A stepwise development of the Peterson’s mutual exclusion algorithm using B abstract systems (2005)
  8. Butler, Michael; Leuschel, Michael: Combining CSP and B for specification and property verification (2005)
  9. Ferreira, Carla; Butler, Michael: Using B refinement to analyse compensating business processes (2003)
  10. Abrial, Jean-Raymond; Cansell, Dominique; Laffitte, Guy: “Higher-order” mathematics in B (2002)
  11. Abrial, Jean-Raymond; Cansell, Dominique; Méry, Dominique: A mechanically proved and incremental development of IEEE 1394 tree identify protocol (2002)
  12. Chartier, Pierre: ABS project: Merging the best practices in software design from railway and aircraft industries (2002)
  13. Doche, Marielle; Gravell, Andrew: Extraction of abstraction invariants for data refinement (2002)
  14. Cansell, Dominique; Méry, Dominique: Abstraction and refinements of features (2001)
  15. Bert, Didier; Cave, Francis: Construction of finite labelled transition systems from B abstract systems (2000)


Further publications can be found at: http://www.atelierb.eu/en/industrial-references-for-atelier-b/