Project Creation
Two kinds of project
Atelier B allows you to create 2 types of projects:
Software development
A software development project allows the construction of a model of a sequential software. The model contains the specification and design of the functions performed by the software, specification and design being distinct. The design can then show the sequencing of functions from imported components specified and designed in the same way. The dependency graph of a software project is a tree with the highest level component as its root. The software is obtained by translating each implementation-type component into source code.
The development cycle of a software project is detailed below consists of two branches: one for code generation, the other for model proof. It is possible to generate code without proving the model, but there is no guarantee that the software will be flawless. It is also possible to use dumb specifications (an operation specified by skip): the scope of the proof is in this case considerably reduced, the use of this technique must then be justified and supervised.
System modelling
A system modelling project builds a model of a system, in the broadest sense of the term (e.g. an aircraft, a railway crossing, a processor, an administrative procedure). The model represents the state variables of the system and the atomic events that modify, one after another, its state. This model implies an asynchronous and non-deterministic "execution" of its events. Any system can then be modelled, its specification can be equipped with properties and then proven to match those properties. The dependency graph of a system modelling project is a refinement column that contains an abstract machine at the root and eventually a succession of refinements.
A system model does not contain an implementation.
How-to
To create a project, you can either:
select the menu Atelier B / New / Project
use the shortcut Ctrl+Shift+P
click on the yellow + on the toolbar
The 2-step project creation wizard show up.
Leave wokspace as local (default). Type in a project name. Select a project type: either software development or system modelling.
Click Next than click Finish (no need to modify default parameters).
Finally the project is created, named first, and empty.
Last updated
