Les numéros
de Liaison

6 juillet 2006 (no 20)
15 juin 2006 (no 19)
25 mai 2006 (no 18)
4 mai 2006 (no 17)
13 avril 2006 (no 16)
23 mars 2006 (no 15)
9 mars 2006 (no 14)
23 février 2006 (no 13)
9 février 2006 (no 12)
26 janvier 2006 (no 11)
12 janvier 2006 (no 10)
8 décembre 2005 (no 9)
24 novembre 2005 (no 8)
10 novembre 2005 (no 7)
27 octobre 2005 (no 6)
13 octobre 2005 (no 5)
29 septembre 2005 (no 4)
>15 septembre 2005 (no 3)
1erseptembre 2005 (no 2)
18 août 2005 (no 1)

1993-1994 à 2004-2005

Les photos de l'année

Les photos 2004-2005

Calendrier des parutions 2006-2007

L'équipe des publications Liaison

Liaison-région
Liaison-recherche
Liaison-Longueuil
Liaison-médecine
Liaison-médias
Information sur Liaison
Pour nous joindre


 

 


 

Liaison, 15 septembre  2005

 

 
Photo de Marc Frappier, du Groupe de recherche en ingénierie du logiciel.

Marc Frappier, du Groupe de recherche en ingénierie du logiciel.

Photo : Roger Lafontaine

 


Marc Frappier

La vie dans les mains du logiciel

SOPHIE PAYEUR

1979. Le Commandement de la défense aérospatiale de l'Amérique du Nord (NORAD) attaque un énorme missile. On découvre un peu plus tard que le projectile détecté n'était ni plus ni moins que la lune qui montait dans le ciel à la tombée du jour. L'«incident» est survenu lors des tout premiers jours d'utilisation d'un nouveau radar à grande portée.

Quelques années plus tard, entre 1985 et 1987, le Therac-25, un appareil utilisé en radiothérapie aux États-Unis et au Canada, entraîna la mort de six patients. Au terme de ces tristes événements, Therac-25 fut rappelé pour subir d'importants changements : l'appareil projetait des doses beaucoup trop massives de radiation.

Ces accidents sont loin d'être anecdotiques. On les compte par centaines et par milliers depuis l'avènement des ordinateurs, surtout lorsqu'ils sont impliqués dans des systèmes où la sécurité représente un facteur critique. Quel est le point commun reliant ces accidents? Des erreurs dans la conception du logiciel.

«La fiabilité des logiciels est-elle aujourd'hui acceptable?, lance Marc Frappier, du Groupe de recherche en ingénierie du logiciel. La réponse dépend du niveau de risque. Généralement, elle ne l'est pas dans les situations où des vies humaines sont impliquées, comme dans le cas de Therac-25. Les erreurs de conception de logiciel sont des problèmes encore très actuels.» Chaque année, les pertes engendrées par ces erreurs s'élèvent à un milliard de dollars.

Derrière des logiciels et des interfaces d'une convivialité étonnante se camouflent des masses infinies de lignes de programmation extrêmement complexes. Plus la complexité est grande, plus les risques d'erreurs sont accrus. «La plupart des utilisateurs n'ont pas idée de l'immense complexité des logiciels!» souligne Marc Frappier. À elle seule, une imprimante laser contient un million de lignes de code de programmation (LOC). Un commutateur téléphonique chez Nortel : 35 millions. Pour entretenir et rafraîchir le logiciel Windows chez le géant Microsoft, 10 000 personnes sont mobilisées. Les possibilités d'erreurs sont au moins aussi nombreuses que le nombre d'individus et de lignes de code impliqués.

Selon l'informaticien, les problèmes se nichent dans la méthode qu'utilisent la plupart des concepteurs, appelée Unified Modeling Language (UML), ou langage de modélisation objet unifié. Ce langage de programmation a recours essentiellement à des textes et à des dessins. «L'UML est basé sur la langue maternelle et les représentations graphiques. Il laisse une grande place à l'interprétation, d'où les possibilités d'erreurs. Tout est dans la conception : si un logiciel échoue, c'est qu'il est erroné depuis sa création.»

Prouver plutôt que tester

La solution préconisée par Marc Frappier est la méthode dite formelle. Celle-ci exige que les concepteurs travaillent plus fort, mais la démarche est pratiquement infaillible. «On peut comparer les fonctions du système logiciel au plan d'une maison, explique le professeur. Dans la méthode formelle, toutes les fonctions sont décrites principalement par notations mathématiques. Or, la notation mathématique implique nécessairement une preuve mathématique. C'est là toute la différence avec la méthode traditionnelle, qui ne peut pas prouver ce qu'elle décrit; elle ne peut que tester après coup.»

Basée sur un raisonnement rigoureux de logique mathématique, la méthode formelle comporte, par la preuve, la démonstration de sa propre correction. «La méthode formelle procure une forte assurance qu'il n'y a pas de bogue, précise Marc Frappier. Au contraire, les quelques tests effectués par l'UML ne démontrent pas l'absence d'erreurs, seulement leur présence. Or, tester tous les cas équivaudrait à intervenir dans un espace quasi infini, plus grand que ce que même des physiciens peuvent imaginer! Prouver est la seule façon de vraiment traiter tout l'espace d'un programme.» Puisque la programmation est un processus créatif, le risque d'erreurs demeure au sein des deux méthodes. Par contre, le taux d'erreurs entraîné par l'utilisation de la méthode formelle est de 0,01 %, un score fort enviable en informatique.

Les premiers travaux ayant conduit à la méthode formelle furent réalisés dans les années 1960. Trente ans plus tard, la méthode fait l'objet de quelques applications en milieu industriel, mais aujourd'hui encore, en dépit qu'elle soit d'une fiabilité exceptionnelle, elle demeure peu utilisée. «La méthode formelle a la réputation d'être plus dispendieuse, mais en bout de ligne, elle est aussi économique que les méthodes classiques, affirme le professeur. Par contre, elle exige des efforts considérables de la part du concepteur et demande une formation plus spécialisée.»

Marc Frappier cite en exemple la ligne 13 du métro de Paris, qui fonctionne sans conducteur. Conçue avec la méthode formelle, celle-ci a occasionné des coûts fort comparables à ceux des méthodes classiques. Règle générale, toutefois, la méthode formelle est réservée aux logiciels les plus critiques, ceux qui présentent un niveau de risque élevé. Dans ces cas, la méthode formelle se révèle effectivement plus coûteuse. «Plusieurs logiciels de la NASA exigent plus de six mois pour élaborer quelque 100 lignes de code, souligne le chercheur. Les conséquences de possibles erreurs de conception seraient dramatiques. Dans ce cas, la méthode formelle est toute désignée et s'avère rentable à long terme pour la NASA.»

Peu de chercheurs travaillant sur la méthode formelle s'intéressent aux situations critiques. Marc Frappier, lui, tente de mettre au point un logiciel qui facilitera grandement le recours à la méthode formelle. L'idée est de rendre la tâche plus facile aux concepteurs tout en leur économisant du temps. «C'est aussi une manière de réduire l'expertise nécessaire à l'utilisation de la méthode formelle, la rendant ainsi plus accessible», précise Marc Frappier. Un prototype de ce logiciel devrait être prêt dans deux ans. Sans doute aidera-t-il également à franchir l'obstacle majeur auquel se bute la méthode formelle : la nécessité de changer les méthodes de travail utilisées par les concepteurs.

Retour à la une

 

LIAISON est une
publication de
l'Université
de Sherbrooke

 

Éditeur :
Charles Vincent

Local F1-113,
Pavillon J.-S.-Bourque

(819) 821-7388

Liaison@USherbrooke.ca