La s\^uret\'e des logiciels
La sûreté des systèmes
programmés
Eric Goubault
25 juillet 1999
L'automatisation des processus de production amorcée dès les
prémices de la révolution industrielle s'est
accélérée depuis l'avènement de l'informatique. En
cette fin de siècle, aucun secteur de l'industrie ne pourrait se passer
d'ordinateurs qui, aujourd'hui, en calculant des critères de
décision, savent gérer des procédés complexes et
s'adapter à un environnement externe. La question primordiale est alors
celle de savoir si l'on peut faire confiance à ces machines ainsi
qu'à leurs logiciels. La " sûreté des systèmes
programmés " vise à répondre à cette question,
et plus particulièrement à celle de la validité de la
composante logicielle.
En 1944, le projet Whirlwind (Massachussetts Institute of Technology)
était un système programmé ayant pour but le
contrôle du trafic aérien, certes, uniquement militaire. Ces
circuits logiques étaient constitués d'une myriade de tubes
à vide qui calculaient des fonctions logiques, contrôlées
par programme. Quelques satisfactions pouvaient raisonnablement être
tirées de cette expérience, si ce n'est que la durée de
vie limitée des tubes causait une erreur fatale toutes les 20 minutes
environ. De nos jours, la durée de vie des composants est sans conteste
très supérieure à celle-ci ; pour autant, le
fonctionnement de ces automates modernes est encore bien capricieux, plus
à cause d'erreurs dans la programmation (c'est-à-dire le
logiciel) qu'à cause de problèmes dus aux circuits
électroniques de l'ordinateur.
Pour mieux s'en convaincre, citons quelques unes des plus spectaculaires et
récentes erreurs informatiques (ou " bug "[1]). L'explosion du vol 501 d'Ariane 5 après 40
secondes (un demi milliard de dollars de perte en matériel, et plus
grave, risque de décrédibilisation d'un programme de 7 milliards
de dollars) était due à un problème de conversion de
format de nombre dans le programme contrôlant le système de
référence inertiel. Une imprécision numérique dans
le calcul d'une horloge interne causa la mort de 28 soldats américains
pendant la guerre du Golfe après la défaillance d'un missile
antimissile Patriot. Des erreurs de calculs sont encore à l'origine de
blessures très graves infligées à 6 personnes entre 1985
et 1987 à la suite de trop fortes doses administrées par
l'appareil d'irradiation thérapeutique Therac-25. Plus récemment,
qui n'a pas eu les oreilles rebattues du fameux et insaisissable " bug de
l'an 2000 " ? Au delà de ces exemples catastrophiques, qui n'a
jamais pesté en s'apercevant de la perte de ses précieuses
données due au " plantage " impromptu d'un logiciel de
bureautique? Fatalité, ou problème intrinsèque à
l'informatique, comme semble en attester l'air le plus souvent
désabusé, mais nullement révolté, des victimes
dudit plantage?
L'informatique peut et doit être fiable, de même que le sont les
autres domaines de l'ingénierie (la mécanique,
l'électricité etc.). Il s'agit en effet d'un impératif
répondant aux enjeux technologiques et économiques de
l'informatisation. Ces enjeux sont majeurs comme l'actualité le montre.
L'activité que l'on appelle " Sûreté des
Systèmes Programmés "[2],
représentée au CEA/LETI par un peu moins de 25 personnes,
s'occupe précisément d'assurer le bon fonctionnement de
systèmes informatiques, et de mettre en place le savoir permettant
d'éviter de tels accidents.
Les logiciels critiques
Ce n'est nullement une singularité que le CEA se soit doté d'une
telle équipe. Le CEA, rappelons-le, a la charge " de donner la
maîtrise de l'atome et de ses applications dans les domaines de la
recherche, de l'énergie, de l'industrie, de la santé et de la
défense ". Cela implique la maîtrise d'oeuvre et
l'intégration de métiers très variés, dont celui
qui consiste à écrire des logiciels critiques et des logiciels de
simulation pour des réacteurs, mais aussi pour la simulation des armes
nucléaires. Par logiciel critique, on entend des logiciels dont les
erreurs pourraient mettre en péril la vie des hommes ou avoir des
répercussions très graves pour le système qu'ils
contrôlent. Les exemples catastrophiques décrits plus haut en font
partie.
Originellement, le Système de Protection Intégré
Numérique (SPIN) pour les centrales nucléaires de 1300 MW fut le
premier système critique informatique (opérationnel en 1982)
identifié comme tel au CEA. Son rôle est de suivre en permanence
les paramètres physiques du coeur de la centrale, de vérifier que
ceux-ci restent dans des valeurs acceptables, et de prendre des mesures
appropriées dans le cas contraire. En particulier, si la
température du coeur dépasse une certaine valeur, la
réaction nucléaire doit être stoppée par la chute de
barres autour des crayons de matière fissile.
Il existe bien d'autres systèmes critiques, hors CEA, que nous
côtoyons plus souvent que le coeur d'une centrale: dès 1983, avec
l'Airbus A310, les commandes de vol de certains avions sont
contrôlées par logiciel. D'ailleurs les transports regorgent de
tels systèmes. Par exemple le métro VAL (et maintenant METEOR)
est une ligne automatique gérée par logiciel. Les voitures haut
de gamme comportent des logiciels chargés aussi bien de gérer
l'allumage électronique que la fermeture des portes, l'ABS et le
déclenchement des airbags.
Par extension, les logiciels de transactions financières ou
boursières, bien que non critiques dans le sens originel du terme,
deviennent des éléments sensibles[3]. Le secteur des télécommunications, ou celui
de la micro-électronique, dans lesquels les pannes peuvent impliquer de
sévères sanctions financières[4], recèle de plus en plus de logiciels devant
être traité avec le même souci de qualité que les
logiciels critiques.
Idéalement, quand les méthodes de programmation et les techniques
de validation de logiciel, auxquelles le CEA participe pleinement, seront plus
mûres et mieux distribuées, c'est la qualité de tous les
logiciels qui bénéficiera des avancées faites dans le
logiciel critique. Plus les programmes deviennent complexes, plus les outils
logiciels se font indispensables dans la vie quotidienne, et plus les attentes
concernant les programmes " sûrs " seront grandes et
détermineront la vie des éditeurs de logiciels et des
constructeurs informatiques. La " sûreté des systèmes
programmés " est un secteur d'avenir, dans lequel le CEA s'est
engagé, fort de son expérience dans la maîtrise des
secteurs critiques. Certains systèmes critiques que nous avons
évoqués ont fait l'objet d'une collaboration ou d'accords
commerciaux avec le CEA, lequel a ainsi pu transférer certaines de ses
technologies à l'industrie.
Programmation et validation
Pour comprendre les actions menées au CEA concernant la
sûreté des systèmes programmés, il nous faut
commencer par expliquer brièvement comment les logiciels sont
conçus et intégrés.
La construction d'un logiciel
L'informatique s'est développée autour d'aspects très
expérimentaux. Trop souvent, la pratique veut que l'on procède
par essais successifs : programmation, test en exécutant sur
quelques données jugées typiques, puis correction des erreurs et
ainsi de suite jusqu'à satisfaction du programmeur, ou
épuisement du budget, voire du délai.
Cet état de fait s'est institutionnalisé au travers de
modèles de développement rationalisant cette démarche et
spécifiant les différentes étapes d'écriture puis
de validation du code. On distingue en général les phases
suivantes ; la première est une phase de spécification. Cette
phase n'est rien d'autre qu'une déclaration d'intention sur ce qui doit
être fait par le logiciel, dans quel environnement, et sur le
problème à résoudre. L'architecture du logiciel est
ensuite définie. Elle comporte le découpage des
fonctionnalités à programmer en fonctions plus
élémentaires et en " modules " aux interfaces claires,
afin de pouvoir diviser le travail au mieux parmi les ingénieurs
informaticiens (les développeurs). La définition des
différentes tâches est d'abord faite à grands traits, pour
en arriver finalement à la conception détaillée, qui
spécifie entièrement l'ensemble des fonctions à
programmer. Puis, vient le codage proprement dit. Ensuite, ou en cours de
codage, on essaie de vérifier le programme, s'appuyant sur ses
spécifications. Enfin, le programme final est testé en situation,
sur les machines et environnements cibles.
Ce schéma général est notoirement insuffisant pour donner
les garanties adéquates dans le cas d'un logiciel critique. Le test par
exemple, aussi sérieux soit-il, n'est qu'exceptionnellement exhaustif.
La complexité des programmes (de nos jours, des centaines de milliers de
lignes de code pour les logiciels critiques, et des millions pour les autres),
le nombre gigantesque d'états qu'il faudrait théoriquement tester
(des chiffres qui peuvent dépasser le nombre de particules dans
l'univers) pour être sûr de leurs comportements en toutes
situations, font que même avec les machines puissantes dont nous
disposons aujourd'hui, il nous faudrait peut-être quelques
millénaires, ou même bien plus encore, pour effectuer ces calculs.
Il serait utopique voire dangereux de penser que seule une petite portion de
ces tests, choisie pour décrire l'essentiel des comportements possibles,
suffirait à garantir le logiciel. Les " bugs ", au sens d'une
exécution erronée, amenant éventuellement à
l'arrêt brutal du programme, sont des événements rares mais
catastrophiques. Par exemple, le comportement général d'un
programme effectuant une division de nombres entiers est assez simple à
vérifier ; on peut tirer au hasard presque n'importe quel couple de
nombres pour tester l'implémentation de la fonction. Hélas, une
seule valeur du dividende (zéro) pose un problème grave à
l'exécution, et il faut une certaine chance pour tester cette valeur
singulière et s'apercevoir si le cas est traité correctement ou
pas.
Des modèles du logiciel
Quoiqu'il en soit, on ne peut traiter du logiciel, critique ou pas, comme d'une
boîte noire, dont on verra bien à l'usage si elle remplit son
rôle correctement. Aucun ouvrage, aucun pont, aucun bâtiment ne
serait construit, et encore moins certifié, sur de tels principes. Que
faire alors ?
Un scientifique n'étudierait pas un système physique en se
contentant d'énumérer ses configurations. Une seule
méthode est disponible en ingénierie qui puisse répondre
aux exigences de vérification et de justification des choix
effectués. C'est à travers la modélisation
mathématique que l'on peut donner des garanties sérieuses de bon
fonctionnement. Une formalisation mathématique représente en
concentré ce qui peut se passer ; c'est par le raisonnement formel
que l'on peut en extraire les propriétés essentielles du
système, sans tomber dans la fastidieuse énumération de
laquelle aucune compréhension des phénomènes ne peut
ressortir.
On pourrait être trompé en pensant que la simulation (sur maquette
ou sur ordinateur) ou le calcul d'un ouvrage d'art dans des conditions
extrêmes (de vent, de température, etc.) ressemble au test du
logiciel dans un cas très particulier. Ce serait oublier deux choses. La
première est qu'un tel ouvrage mécanique (un pont, un
bâtiment etc.) bénéficie des siècles
consacrés à la mécanique des milieux continus, à
l'élasticité, à l'étude des matériaux. Dans
ces conditions, les " bugs " sont assez bien délimités
; si un pont résiste à des conditions cycloniques, il a toutes
chances de résister au climat parisien[5]. La deuxième est que si on peut en
général utiliser un coefficient de sécurité (une
épaisseur double des piliers de soutènement par exemple) pour
améliorer la durée de vie d'une construction, il n'en est pas de
même pour un logiciel. Ce n'est certainement pas en doublant la taille du
code d'une fonction " critique " que l'on va améliorer, loin
s'en faut, la qualité d'un logiciel.
Les mathématiques sous-tendant la vérification des logiciels, ou
" sémantique ", sont en fait plus proches de la logique,
à qui on attribue d'ailleurs souvent la paternité historique de
l'informatique, que des équations aux dérivées partielles.
Une seule ligne de programme oubliée, une autre en trop, et c'est toute
la cohérence d'un programme qui peut être mise à bas, comme
on peut rendre faux un long raisonnement par l'utilisation d'une
hypothèse erronée.
Encadré 1: Sémantique de programmes
Un programme est une suite de commandes élémentaires, telles des
calculs sur des variables, ou des boucles
de traitement répétant un calcul un nombre quelconque de
fois ; le petit programme C[6]
suivant :
while (x < 100)
x=x+1 ;
opère une transformation simple sur la valeur de la variable x (qui peut
être quelconque avant exécution) : il ajoute un à x
jusqu'à ce que x soit supérieur ou égal à cent. La
sémantique traduit en termes mathématiques cette formulation
faite en langage naturel. Associons à chaque ligne de ce programme une
" étiquette ", 0 avant le mot clé while, 1 avant
l'incrémentation x=x+1, 2 après et 3 après le
point-virgule (en sortie de la boucle while). Nous allons également
associer à chaque étiquette une formule logique décrivant
les états possibles du programme à cette étiquette, pour
toutes les exécutions possibles (c'est à dire quelles que soient
les valeurs d'entrée de la variable x). Le programme donné en
exemple étant extrêmement simple, un état décrit un
ensemble de valeurs que peut prendre la variable x. Par exemple, si l'on
choisit une formulation ensembliste, un état en le point de
contrôle i (0, 1, 2 ou 3) est un ensemble Xi qui
vérifie le système d'équations,

En effet, les valeurs possibles de x en le point 1 sont soit celles que l'on
avait en 0 en supposant qu'elles permettent à l'exécution de
rentrer dans la boucle, donc x est inférieur à 100, soit celles
du point 2 en supposant que l'exécution boucle, donc nous savons
également que x est inférieur à 100. Si nous avions
écrit la première équation dans le format d'une
transformation de prédicats logiques, nous aurions
.
C'est en particulier ce genre de formulation qui est utilisé dans
l'outil CEA " CAVEAT "[7]. La plus
petite solution de ce système d'équations donne la
sémantique, et comme nous nous y attendons,

Nous avons prouvé que l'exécution, si elle se termine
(nécessairement en 3), la valeur de x est toujours supérieure
à cent, et en utilisant une sémantique un peu modifiée, on
pourrait aisément prouver que ce programme se termine toujours sans
erreur. Il va de soit que les équations, ainsi que leurs solutions, sont
nettement moins intuitives dans les cas réels.
Des outils nécessaires
C'est seulement une fois la définition mathématique
effectuée que l'on peut raisonnablement se poser des questions sur des
programmes. Il est possible alors, par exemple, d'aider le développeur
à trouver et justifier certains tests. Plusieurs techniques sont
disponibles et font l'objet de recherches au CEA (voir encadré 2).
Encadré 2: Quelques projets au LETI/DEIN
* AGATHA analyse des spécifications parallèles de haut
niveau et vise à générer automatiquement les tests
correspondants.
* CAVEAT est un prouveur de programmes écrits en C, utilisant une
sémantique logique des programmes.
* CLAIRE est un atelier de simulation logiciel de systèmes complexes. Il
permet de tester des composants et des logiciels sans avoir à concevoir
de banc test matériel peu adapté.
* GATeL (" Génération Automatique de Tests Lustre ")
est développé en collaboration avec le Laboratoire de Recherches
en Informatique de l'Université d'Orsay, et permet d'automatiser la
génération de tests pour des programmes écrits dans le
formalisme temps réel synchrone Lustre.
* OASIS est un système permettant de bénéficier des
bienfaits de l'approche Lustre tout en se débarrassant de certaines
contraintes temporelles. Il est envisagé de l'utiliser dans le cadre du
développement des nouvelles générations de systèmes
de protection.
* TWO est un projet européen auquel le CEA participe, visant à la
génération automatique de tests et à l'analyse automatique
des erreurs possibles que l'on pourrait rencontrer à l'exécution
de programmes écrits en C et C++.
Une première voie est d'utiliser la sémantique du langage pour
déterminer, par calcul, les environnements d'exécution (valeurs
d'entrée du programme par exemple) permettant d'exhiber certains
comportements caractéristiques d'un logiciel. Ces comportements
caractéristiques peuvent être, comme c'est le cas dans ce que l'on
appelle la génération de test structurel, d'atteindre un endroit
particulier du programme - un " point de contrôle - ou de suivre un
certain chemin, c'est à dire une certaine suite de points de
contrôle. Une deuxième est d'utiliser à sa place la
spécification du logiciel analysé, elle aussi convenablement
formalisée. Les environnements d'exécution ainsi trouvés
permettent ensuite de tester le programme. Cette confrontation détermine
partiellement si celui-ci se conforme à ses spécifications.
Ces recherches sont, on s'en doute, motivées par les pratiques de
développement décrites précédemment. Toutefois, ce
n'est pas tout ce que l'on peut faire sur le logiciel. Après tout, le
but ultime est de prouver le programme, ou au moins de prouver
mathématiquement que certaines " bonnes
propriétés "[8] sont toujours
satisfaites lors de l'exécution et que des " mauvaises
propriétés "[9] n'arriveront
jamais. L'idée est de se passer totalement de l'exécution du
programme pour ne plus faire appel qu'au raisonnement mathématique pour
trouver les erreurs. Un programme est donc conçu dans ce cadre comme une
formule de mathématiques[10] qu'il s'agit
de prouver. Le problème principal est de savoir comment faire cela
intelligemment, car la formule en question fait peut-être un million de
lignes !
Il n'y a donc pas d'autre solution que d'automatiser les calculs et les
preuves. Le CEA est amené ainsi à développer des outils de
vérification automatique. La détermination des tests implique
d'utiliser des techniques élaborées telles la résolution
de contraintes et la simplification algébrique. La preuve
nécessite des technologies et des recherches en démonstration
automatique.
Parfois, la preuve complète d'une propriété peut
résister au démonstrateur[11].
Il y a alors la possibilité d'approximer (ce que l'on appelle
plutôt abstraire) les propriétés et, tout comme les
numériciens le font pour simuler des systèmes physiques
complexes, de calculer ces approximations par des schémas
itératifs. C'est dans les grandes lignes, l'idée de départ
de l'interprétation abstraite[12], qui
est une des techniques employées au CEA.
Un autre axe de recherche et de développement au CEA concerne la mise au
point de systèmes (sur lesquels vont s'exécuter des logiciels),
suffisamment contraints pour pouvoir assurer automatiquement certaines bonnes
propriétés, en particulier dans le temps réel, mais
suffisamment expressifs tout de même pour pouvoir être utiles. Une
des particularités des logiciels critiques est que l'on peut se
permettre de brider un peu le langage utilisé, ou le système sur
lequel ils fonctionneront, pour en supprimer les aspects les plus dangereux, et
faciliter ainsi par construction leurs preuves. Cet axe complémentaire
se base sur des considérations mathématiques similaires, seules
garanties possibles du bon fonctionnement futur des logiciels.
Enfin, une recherche qui n'est pas effectuée au CEA, mais dont les
résultats ont été utilisés en particulier dans le
monde des transports concerne la synthèse automatique de programmes
prouvés, à partir des spécifications formelles.
L'idée (celle de la méthode B entre autres) consiste à
donner une définition purement logique de ce qu'un programme doit
effectuer comme calculs et comme tâches, et à en extraire ensuite,
par un processus de raffinement successif, la suite de commandes
vérifiant au mieux la spécification. La programmation est ainsi
comprise comme un procédé de preuve et d'explicitation d'une
spécification logique.
Le rôle du CEA
Le CEA (LETI/DEIN) effectue ces recherches et développements pour
assurer le bon fonctionnement, en premier lieu de logiciels critiques. Les
équipes y développent la théorie nécessaire, ainsi
que les prototypes démontrant leur applicabilité.
En amont, certaines des recherches les plus prospectives sont effectuées
en collaboration avec les meilleurs laboratoires universitaires. En aval, des
contrats d'études sont passés avec des grands industriels, qui
permettent d'une part de faire connaître le savoir faire du CEA et de
démarrer le processus de transfert vers l'industrie[13], et d'autre part, de tester les idées et de mieux
comprendre les besoins.
Il est naturel que d'autres branches de l'industrie souhaitent
bénéficier de l'expérience acquise dans le monde
nucléaire, secteur critique s'il en est. Le nombre de contrats
passés ces dernières années, avec l'aéronautique et
l'industrie automobile notamment, traduit l'intérêt croissant du
monde industriel pour la vérification de systèmes
informatiques.
En ce qui concerne les logiciels utilisés dans le nucléaire, le
CEA met ses outils[14] et son
expérience (au travers d'études de cas) à disposition des
équipes de vérification de l'Institut de Protection et de
Sûreté Nucléaire (IPSN). L'IPSN effectue les
contrôles nécessaires, sur demande de la Direction de la
Sûreté des Installations Nucléaires (DSIN), qui
dépend du Ministère de l'Économie, des Finances et de
l'Industrie. En parallèle, l'exploitant des centrales,
Électricité de France, rend des comptes à la DSIN et
impose des vérifications et des plans d'assurance qualité au
constructeur des centrales, FRAMATOME et, en cascade, à tous ses
sous-traitants, Schneider-Electric entre autres.
Conclusion et Perspectives
Il est important de comprendre que l'informatique est fondamentalement une
activité mathématique. Cela n'étonnera ni le physicien ni
l'ingénieur qu'il soit mécanicien, électronicien ou autre.
Des siècles de mathématiques ont façonné le langage
et clarifié les concepts et méthodes (calcul infinitésimal
ou différentiel etc.) utilisés par les ingénieurs et
techniciens dans tous les domaines. L'informatique est également une
science de l'ingénieur, qui trouve ses fondations dans des
théories mathématiques, parfois nouvelles. Pourtant, elle est
victime de son succès. Les développements de logiciels sont plus
rapides que ne le sont les développements théoriques, seule
assise solide pour les méthodes assurant la sûreté des
systèmes programmés. Et le travail ne s'arrête pas à
la seule théorie. De même qu'il est peu courant de chercher de
nouvelles molécules pharmaceutiques et d'en étudier le
comportement chimique dans le corps humain en commençant par les
équations de la mécanique quantique, il est difficile d'appliquer
aveuglément les résultats des théories informatiques. Des
techniques sont nécessaires qui permettent de maîtriser la
complexité inhérente au domaine. La théorie n'est
là essentiellement que pour donner les bons concepts de base (comme par
exemple en thermodynamique, la température et la pression). Parmi les
développements de la pratique auxquels la théorie et les
méthodes de validation du logiciel devront s'adapter prochainement,
figureront très certainement les applications distribuées (le
" Web " ou les réseaux de calculateurs) ainsi que les
programmes de simulation numérique qui posent des problèmes
nouveaux de vérification, concernant en particulier la précision
de leurs résultats[15]. Le CEA par son
implication dans un secteur critique phare, et le LETI en particulier, par sa
position de leader dans l'informatique et l'électronique, sont au
premier plan dans ce domaine, et se doivent d'y rester.
Encadré 3: Les " bugs " numériques
Un des grands paradoxes de l'informatique est que l'ordinateur est
utilisé pour calculer, mais qu'il calcule le plus souvent faux. Les
entiers représentables en machine ne correspondent nullement aux entiers
mathématiques, ils restent bornés. Les " flottants ",
c'est-à-dire les nombres réels informatiques n'ont qu'une
lointaine ressemblance avec leurs cousins mathématiques. Par exemple,
l'associativité de la multiplication n'est pas valide en
général dans les nombres flottants ; de même si une
valeur est non nulle, mais très petite, son carré peut être
nul ! Et pourtant la simulation numérique est devenue un outil
central de conception et de modélisation en ingénierie. Les
numériciens ont bien conscience de ce problème, et il est rare
que l'on ne confronte pas la simulation numérique à des
expériences grandeur nature. Néanmoins, des erreurs peuvent
subsister, bien moins visibles à l'exécution que
n'étaient certains des " bugs " catastrophiques
érigés en épouvantail au début de cet
article ; on peut considérer en effet qu'un calcul trop
imprécis voire complètement faux est une erreur de programmation
majeure, pouvant amener à des catastrophes. L'exemple du missile Patriot
cité dans l'introduction est à cet égard tout à
fait symptomatique. Le " bug " était simplement du au fait que
l'horloge interne de l'appareil dérivait, car ajoutant dans une
mémoire un dixième tous les dixièmes de secondes. Mais un
dixième, contrairement à ce que l'on pourrait croire, n'est pas
représenté de façon exact sur une machine (binaire) !
[1] " Cafard " en anglais, terme
technique consacré depuis qu'un de ces insectes se trouva
écrasé par un relais électronique, causant ainsi des
problèmes inexplicables sur un ordinateur Mark II pendant la
deuxième guerre mondiale. Le lecteur passionné pourra aller
admirer ce " bug " au " National Museum of American History of
the Smithsonian Institution ".
[2] Elle ne doit pas être confondue avec
la sécurité informatique qui est l'activité consistant
à éviter l'accès non autorisé à des
informations confidentielles.
[3] L'utilisation de l'informatique au coeur des
processus industriels est de plus en plus incontournable ; le logiciel
peut être adapté sans cesse aux besoins, contrairement à
des automates spécialisés. Malheureusement, cette capacité
à évoluer augmente les risques de " bugs ", car il est
bien difficile de maîtriser l'ensemble d'un logiciel pendant toute sa
durée d'utilisation.
[4] On se souvient tous du bug du
microprocesseur grand public Pentium, qui aurait semble t-il coûté
un milliard de dollars à Intel.
[5] Ici, une simulation peut recouvrir une
infinité de conditions possibles " moins dures ". N'oublions
pas néanmoins des phénomènes comme la résonance
(qui a détruit un pont au milieu du vingtième siècle aux
Etats-Unis) ou les phénomènes thermiques cycliques qui
fragilisent les matériaux.
[6] C est un langage courant dans le monde
industriel qui date des années 70.
[7] Voir encadré 2.
[8] Par exemple, les variables du programme
restent toujours dans des valeurs acceptables, ou dans le cas du système
de protection des centrales nucléaires, que l'arrêt d'urgence peut
toujours se faire lorsque cela devient nécessaire.
[9] Division par zéro, perte des
données etc.
[10] Comme les équations de
l'encadré 1.
[11] Quelle que soit la technologie
utilisée, le problème de la preuve exacte est en
général insoluble automatiquement, bien qu'elle soit accessible
dans bien des cas.
[12] Introduite à l'origine par P.
Cousot (Ecole Normale Supérieure) et R. Cousot (Ecole Polytechnique).
[13] Certains des prototypes sont dans ce cas
pris en charge commercialement par des industriels.
[14] Voir l'encadré 2 à propos
des différents projets.
[15] Voir l'encadré 3.