PROGRAMMATION

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 dépend de conditions initiales variables (exemple : paramètres fournis lors d'un appel, ou lecture d'informations captées dans l'environnement). L'enjeu est alors de s'assurer que l'on aura les effets souhaités – ce qui soulève la question de spécifier les comportements désirables (ou indésirables) ; nous y reviendrons plus bas –, et ce dans tous les cas. Ce dernier point fait écho à ce qui précède : alors que, pour les systèmes analogiques, nos mathématiques portent d'emblée sur des plages entières de valeurs, la complexité spécifique du logiciel (et des systèmes matériels basés sur des circuits logiques) provient de la nécessité intrinsèque d'étudier exhaustivement, et souvent un par un, une multitude de cas de figure (sans perte de généralité, on ne s'attarde pas ici sur le cas intermédiaire des programmes numériques). Le travail qui en résulte est principalement un travail de raisonnement logique. La difficulté vient de ce que le nombre de cas à considérer tend à s'élever très vite avec l'augmentation de la complexité des systèmes, des fonctions à réaliser, de la multiplication des combinaisons, etc.

En pratique, ceux qui sont chargés de concevoir et de réaliser un système programmé raisonnent constamment : par cas sur les valeurs traitées, par récurrence sur le nombre de tours de boucle effectués, etc. En règle générale, il s'agit d'un mélange de bon sens, de réutilisation de résultats antérieurs et d'expérimentation. Mais ces raisonnements sont rarement explicites, sinon ils présenteraient les deux défauts rédhibitoires d'être beaucoup trop longs et beaucoup trop fastidieux. Ils sont par conséquent humainement impossibles à vérifier... sauf si la tâche est assistée par ordinateur : c'est précisément ici qu'interviennent les méthodes formelles. Leur objectif, partant d'une spécification formelle du système étudié, décrivant la fonction qu'il doit réaliser au moyen de formules, est d'assurer que celle-ci est respectée par le système réalisé. Techniquement, le travail porte sur des expressions formelles issues de la spécification ou du code du programme. Les méthodes formelles sont très variées et offrent toute une gamme d'outils, visant notamment une aide à la spécification, à la structuration du raisonnement, à l'automatisation des démonstrations, à [...]

1  2  3  4  5 …
pour nos abonnés,
l’article se compose de 12 pages