Formal Methods : Application to the Railway Domain

Although formal program analysis techniques (see the work of Hoare and Dijkstra ) are quite old, they were first introduced in the 1980s. Formal methods make it possible to analyze the behavior of a software application described in a programming language. The correctness (good behavior, program termination, etc.) of a program is then demonstrated through a program proof based on the calculation of the weakest precondition .

It wasn't until the late 1990s that formal methods such as Z , VDM and/or the B method were used in industrial applications. Formal methods use mathematical notations to describe precisely the properties a software package must have.

As one of the pitfalls is the impossibility of implementing them in the context of an industrial application (large-scale application, cost and time constraints, etc.), – scaling up – can only be achieved through "sufficiently" mature, high-performance tools.

Although the use of formal methods is booming, it remains marginal in terms of the number of lines of code. Indeed, there are currently...