Un code source peut être vérifié de façon automatique (méthodes formelles),
Au mieux, tu peux faire valider "des" théorèmes, mais rien ne prouve qu'ils sont valides et suffisant d'un point de vue sécurité. (en gros, est-ce que ta spec est complète et exhaustive ? elle ne l'est jamais !)
, mais ça se fait dans divers domaines sensibles (médecine, avionique, etc).
En avionique, non (difficile à faire qualifié DO178). En médecine, cela m'étonnerait. J'en ai vu dans le ferroviaire pour montrer que les systèmes complexes de feu ne pouvaient se bloquer (sorte de deadlock).
[^] # Re: Vote par correspondance
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Vote électronique. Évalué à 7.
Au mieux, tu peux faire valider "des" théorèmes, mais rien ne prouve qu'ils sont valides et suffisant d'un point de vue sécurité. (en gros, est-ce que ta spec est complète et exhaustive ? elle ne l'est jamais !)
En avionique, non (difficile à faire qualifié DO178). En médecine, cela m'étonnerait. J'en ai vu dans le ferroviaire pour montrer que les systèmes complexes de feu ne pouvaient se bloquer (sorte de deadlock).
"La première sécurité est la liberté"