2. Méthodes formelles
Les méthodes formelles sont des techniques informatiques d'une grande rigueur permettant, à l'aide de langages spécialisés et de règles logiques, de s'assurer (idéalement) de l'absence de tout défaut de programmes informatiques – ce qui est crucial en particulier lorsque ceux-ci mettent en jeu des vies humaines –, de logiciels ou de démonstrations mathématiques.
• Besoins et enjeux
En quelques décennies, la miniaturisation des processeurs a permis leur introduction dans des équipements de toutes tailles et dédiés à toutes sortes de tâches, qu'il s'agisse d'électroménager, de centrales nucléaires, d'appareils médicaux, de cartes à puce, d'automates bancaires, de systèmes de télécommunications, d'automobiles ou d'avions de ligne. Tous ces équipements sont donc pilotés ou contrôlés par des programmes logiciels, et cela change complètement la donne quant aux dispositions à prendre pour éviter les défaillances. Pour mettre au point la partie analogique de ces systèmes, les moyens mathématiques à mettre en œuvre relèvent de l'analyse, plus précisément du calcul différentiel. Sommairement, on a affaire à des fonctions continues, produisant en sortie des effets voisins lorsque les déviations en entrée sont petites. Les systèmes discrets, et tout particulièrement les programmes, sont en revanche fondamentalement instables. Au niveau des portes logiques ou des instructions machine, le moindre changement de bit a potentiellement des effets arbitrairement grands. Dans un programme exprimé dans un langage de haut niveau, une modification minime dans une valeur, une expression ou une instruction conduit tout aussi facilement à d'énormes différences de comportement. Observons en passant l'importance de cette caractéristique du logiciel, sa flexibilité : par comparaison avec un système matériel, il est très facile d'intervenir sur un programme pour le corriger, en changer les fonctionnalités, mais aussi d'y introduire des erreurs (y compris en voulant le corriger).
Abstraitement, l'exécution d'un programme reste un enchaînement de décisions distinctes. L'enchaînement précis qui se déroule […]
… pour nos abonnés, l'article se prolonge sur 11 pages…
