La maison Blanche met en avant l’usage des méthodes formelles dans un nouveau rapport publié.
Trois extraits très intéressants :
It is possible to demonstrate correctness using mathematical techniques called formal methods. These techniques, often used to prove a range of software outcomes, can also be used in a cybersecurity context and are viable even in complex environments like space.
Model checkers can answer questions about a number of higher-level properties. These algorithms can be used during production; however, they are limited in their scaled use due to their computational complexity.
Formal methods can accelerate market adoption in ways that traditional software testing methods cannot. They allow for proving the presence of an affirmative requirement, rather than testing for the absence of a negative condition.
CLEARSY développe la méthode B depuis 30 ans, méthode formelle avec preuve, utilisée avec succès pour les systèmes et logiciels les plus critiques.