Il existe certes des méthodes qui vont pouvoir prouver le comportement d'un logiciel, comme le langage B de J.R. Abrial. [1]
Cependant c'est une méthode tres couteuse (en temps, en argent) qui n'est utilisé que pour des portions critiques de code, mais qui à tout de même été utilisée pour des projets à succès comme Météor [2] (un métro automatique, comme celui de la ville de rennes)
Des méthodes similaires sont utilisées chez Airbus mais ce n'est pas infaillible, cela demande un effort de modelisation, de descriptions d'états et ça ne garantie pas que le programme fera ce que l'on veut (on peut très bien prouver un additionneur qui soustrait).
Il est impensable aujourd'hui de garantir un programme sans bugs, même si les techniques de Model Checking avancent et qu'a défaut de prouver on tente d'éprouver le code, mais la meilleur façon d'éprouver un code, c'est tout de même de le rendre public !
[^] # Re: Pas exactement
Posté par TiTiX . En réponse au journal La sécurité informatique au 20h de TF1. Évalué à 1.
Cependant c'est une méthode tres couteuse (en temps, en argent) qui n'est utilisé que pour des portions critiques de code, mais qui à tout de même été utilisée pour des projets à succès comme Météor [2] (un métro automatique, comme celui de la ville de rennes)
Des méthodes similaires sont utilisées chez Airbus mais ce n'est pas infaillible, cela demande un effort de modelisation, de descriptions d'états et ça ne garantie pas que le programme fera ce que l'on veut (on peut très bien prouver un additionneur qui soustrait).
Il est impensable aujourd'hui de garantir un programme sans bugs, même si les techniques de Model Checking avancent et qu'a défaut de prouver on tente d'éprouver le code, mais la meilleur façon d'éprouver un code, c'est tout de même de le rendre public !
[1] http://www.atelierb.societe.com/index.htm(...)
[2] http://www.siemens-ts.com/pages/produits/Meteor.htm(...)
--
TiTiX