"Data validation based on a formal specification of the safety requirements: 20 years of industrial experience"

  29th Brazilian Symposium on Formal Methods (SBMF 2026, https://lnkd.in/eyw_U65P), Rio de Janeiro, 1 to 4 December.

"Data validation based on a formal specification of the safety requirements: 20 years of industrial experience", by thierry lecomte, Dalay Almeida, Ph.D. and Vincent Germain, PhD (CLEARSY) with Michael Leuschel (Heinrich-Heine-Universität Düsseldorf).

Two decades of academic and industrial research had to meet for this to work.

On one side a rule language that separates the safety logic from the data formats.
On the other a solver that grew from a research animator into an engine analysing B machines of ten million lines.
Neither would have sufficed alone.
And above all the work rests on human intelligence.
The rules are written by engineers who understand what a system does and what it must never do.
The tools check the data against those rules, they do not write them.

The result is used in certified railway applications carrying nearly billions of passengers.