Atelier B 4.x in a Nutshell

Atelier B is a software (CASE tool) for:

  • software-modelmodelling software and producing code that could be mathematically proved to comply with its specification. Both specification and implementation components are written using the B language (specification can be non-deterministic while implementation makes use of usual imperative programming language structures). For optimal results, specification has to be abstract while implementation contains detailed algorithms (if both specification and implementation contents are equals, only copy/paste functionality is proved). Most testing is replaced by mathematical proof: the process, based on a specific tool – a theorem prover – is mostly automatic, the elements that are not demonstrated automatically need some human interactions in order to have there demonstration completed.
  • Event-B system modelmodelling systems with the help of atomic, asynchronous, guarded events that describe their behaviour. As for software model, specification can be abstract and would be made more precise (refined) through a number of refinements (refinement column). Models have to be proved to be consistent (the behaviour described in a model have to comply with expected properties) and to refine each other. As for software models, the proof process is mostly automated with some human interactions when some demonstrations can’t be obtained automatically).

Below are some screenshots of the application: