Construire des logiciels fiables

Les « bugs » informatiques, c’est-à-dire les erreurs involontaires de programmation, peuvent avoir des conséquences désastreuses, quand elles ont lieu dans un logiciel critique, comme dans un centre d’appel téléphonique d’urgence (cf. la panne des numéros d'urgence en France en juin 2021), ou pire dans le système de sécurité d’une centrale nucléaire. Nous allons voir comment la programmation défensive formellement vérifiée, en complément des méthodes traditionnelles du génie logiciel, permet de réduire significativement les risques de telles erreurs. En passant, nous discuterons de pensée floue, puis de formalisation mathématique en l’illustrant sur des problèmes proches des « sudokus » (en fait les problèmes SAT booléens).

À première vue, les erreurs involontaires de programmation logicielle, plus ordinairement appelées « bugs », ont des causes multiples : erreurs d’étourderie ou d’inattention (par exemple, interversion des noms « i » et « j ») ; contresens sur la signification d’un morceau de programme ou du cahier des charges (censé donné la description du comportement attendu du logiciel) ; sur-interprétation d’un cahier des charges ambigu, incomplet ou contenant du non-dit ; vraie erreur de raisonnement (par exemple mauvaise compréhension d’un concept, utilisation d’une hypothèse implicite fausse) ; etc. Pour empêcher ou détecter de telles erreurs lors du développement logiciel, l’état de l’art recommande de combiner un ensemble de « bonnes pratiques ». En pratique, il reste cependant toujours des bugs qui sont détectés bien trop tard, une fois que le logiciel est déjà entré en service.