B-method, a safe approach to software

One day, I was having a discussion about safety in the software development cycle of our project with a colleague. Then I remembered a subject I worked on in the old days, which was really interesting for me. As I am a huge mathematics fan, I remembered it very well, it was about creating a predicate evaluator for a tool used in the B-method.

Then, to B or not to B ? Let’s dive into the B-method, together.

What could it B ?

The B-method, is not about extracting nectar from flowers for making honey. It is rather:

1. a formal method; meaning that it is based on a mathematical formalism.
2. with proof; the proof guaranties that the model is consistent in all possible use cases.
3. used for modeling a system or developing software.

Though it is not very famous amongst software folks, the B-method is used in many big industrial projects, here are some of them:

KVB: Alstom — Automatic Train Protection for the French railway company (SNCF), installed on 6,000 trains since 1993 60,000 lines of B; 10,000 proofs; 22,000 lines of Ada

SAET METEOR: Siemens Transportation Systems. — Automatic Train Control, new driverless metro line 14 in Paris (RATP), 1998. 3 safety-critical software parts: onboard, section, line 107,000 lines of B; 29,000 proofs; 87,000 lines of Ada

EADS — Model of tasks scheduling of the software controlling stage separation of Ariane rocket

I hope that the B-method caught your attention now, let’s see more.

B in software

B-method software cycle (rf. methode-b.com)

Some specific terminology should be clarified:

The Abstract Model

Requirements are formalized into B specifications module by module. Non-formal and formal specification are very close (they both express what the software should do) to minimize errors

Some software properties are formalized into B. They strengthen the B model, since we must prove that they remain true when the modules are put together.

The Concrete Model

We must prove that the concrete model complies with its specification (the abstract model), since it is a sort of specialization of a more abstract model.

There is also what is called refinement, which is the idea of adding more details to the model to make it concrete. In B-software, it corresponds to an implementation (the last implementation is the program itself) of a model (specification abstract or refined).​​

Conclusion

There are many benefits to B-software:

• NO classic programming error in the code (overflow, division by 0, out of range index, infinite loop, aliases)
• Unit Test are no longer used
• Early detection of errors
• Frameworks like AtelierB or Rodin making it easy to generate healthy POO code in various languages (C++, Ada, C, …).

But all this comes with an overhead, which is the development speed and the scope or the type of applications that could be implemented with B without exploding complexity and budgets as well. Sometimes it is not necessary nor pragmatic to prove at each step the correctness of the model.