Software development in B
From ClearSy Tools
Contents |
What is B ?
B is not very different from other imperative programming languages like C or Ada. Almost the same features are available (sequencing, valuation, test, loop, modularity). The main difference resides in the fact that specification and implementation of a software are written using the same formalism, enabling a mechanical compliancy verification of the latter towards the former.
However, B has some restrictions, compared to other languages:
- loops should terminate (and it has to be mathematically demonstrated).
- a variable can't be implemented in more than one module.
- operations (functions) can't be used in the module where they are defined, but imported from other modules (exception: LOCAL_OPERATIONS).
What is a good B specification ?
This is a good question I have been asked so many times. There is no definitive answer, as it may vary depending on B expert modelers. However some hints can be provided to help you deciding if a B specification is "good" or not:
- Focus on the "What" instead of the "How". Specify the transfer function of your software/module instead of describing the different steps . Sequencing is not allowed in specification to prevent developers to copy/paste their code in their specification.
- Simplify your specification. Taking into account all the variables of your software in your toplevel module is not a good idea (exception: small software). Design details may be introduced later on.
Examples
Fuel level meter
We are considering here a software in charge of evaluating the remaining amount of fuel in a tank. For example, this information might be critical for a plane (because an error in the estimation might lead to a crash).
So we would like to develop a piece of software to would make the pilot (or the driver) aware of the situation (fuel level below a given capacity). This is in fact the main property of our software, independently from the way the fuel level is estimated.
I mention "estimation" because we are dealing with real world sensors that might fail at delivering accurate information. So I decide to use several redundant sensors to estimate the fuel level