The Bourgeois Gentleman, Engineering and Formal Methods (Thierry Lecomte)

 https://www.researchgate.net/publication/343618644_The_Bourgeois_Gentleman_Engineering_and_Formal_Methods

 

Abstract. Industrial applications involving formal methods are still ex-
ceptions to the general rule. Lack of understanding, employees without
proper education, difficulty to integrate existing development cycles, no
explicit requirement from the market, etc. are explanations often heard
for not being more formal. This article reports some experience about a
game changer that is going to seamlessly integrate formal methods into
safety critical systems engineering.

Keywords: B method, safety platform, automated proof 

The Moliere's Bourgeois Gentleman claimed that "for more than forty years [he
has] been speaking prose while knowing nothing of it". What about imagining engineers
claiming the same assertion but about formal methods ? Formal methods
and industry are not so often associated in the same sentence as the formers are
not seen as an enabling technology but rather as difficult to apply and linked with
increased costs. Lack of understanding, employees without proper education, dif-
ficulty to integrate existing development cycles, no explicit requirement from the
market, etc. are explanations often heard for not being more formal. Our experience
with formal methods, accumulated over the last 20 years [2][3][4][5][7][8],
clearly indicates that not every one is able to abstract, rene, and prove mathematically.
The Swiss psychologist Piaget claimed that only one third of the
population is able to handle abstraction (1). However we are firmly convinced that
formal methods are a fundamental key to ensure safety for our all-connected
world. Several years ago, we imagined a new solution smartly combining the B
formal method, a diverse compilation tool-chain and a double processor architecture
[6]. At that time, our sole objective was to reduce development costs
but since then, given the full automation of the process, we are now considering
this it as a way to obtain quite easily control-command systems certiable at
the highest levels of safety. This paper briefly presents the technical principles
of this platform, the successful experiments/deployments/dissemination before
listing the remaining scientific and technological challenges to address in the
future.
(1) Skill acquired and developed during the so-called Formal Operational Stage 

 

la suite sur Research gate