Rechercher dans la communauté

Ingénierie - À la traque des défaillances catastrophiques Le Devoir Claude Lafleur Édition du samedi 02 et du dimanche 03 mai 2009 Mots clés : Acfas, Sofiene Tahar, Ingénierie, Science, Université, Canada (Pays) Tout ce que vous avez toujours voulu savoir à propos de la « Formal Probabilistic Analysis Using Theorem Proving » La fusée Ariane 501 photographiée peu avant d'être installée sur son aire de lancement en juin 1996. Ariane 501 a explosé 40 secondes après son décollage, victime d'une panne de son système de navigation, ce qui a entraîné la perte des quatre satellites Cluster, d'une valeur de 370 millions de dollars. Photo: Agence France-Presse Toute machine complexe, tel un avion ou un réacteur nucléaire, est susceptible de connaître une défaillance catastrophique. Or, malgré toutes les études, analyses, vérifications et simulations, il est impossible de repérer toutes les possibilités de scénarios catastrophiques. C'est pourtant le défi que relève un chercheur de l'Université Concordia, qui imagine diverses méthodes pour y parvenir. «Ce que nous faisons dans notre laboratoire, c'est essayer de repérer tous les scénarios possibles pour ne pas en échapper un qui soit catastrophique», indique Sofiene Tahar, ingénieur en électronique et en informatique, qui dirige l'équipe de 25 chercheurs du Hardware Verification Group de l'Université Concordia. Son domaine de recherche touche tous les systèmes présents dans notre vie, des réseaux de communication sans fil aux avions, en passant par les logiciels et les puces électroniques. «Je me passionne pour le fonctionnement des systèmes, qu'il s'agisse de logiciels ou de matériels», dit-il avec enthousiasme. D'origine tunisienne, Sofiene Tahar a entrepris ses études universitaires en Allemagne avant de venir les compléter ici. «J'ai passé dix ans en Allemagne et je voulais acquérir une expérience nord-américaine, dit-il. En 1995, je suis donc venu réaliser un postdoc à l'Université de Montréal puis, l'année suivante, j'ai décroché un poste de professeur à l'Université Concordia. Je suis donc demeuré à Montréal..., ce que je ne regrette surtout pas!» Pour sauver Ariane Aurait-on pu sauver Ariane 501? M. Tahar s'émerveille devant la complexité des systèmes que l'industrie développe de nos jours. «Prenez par exemple le microprocesseur Pentium d'Intel, dit-il. Celui-ci contient plus d'un milliard de transistors! On a donc la technologie pour fabriquer ce genre de "monstres", mais comment s'assurer qu'il fonctionne correctement?» Or, justement, l'industrie de la microélectronique et du logiciel consacre environ 70 % de ses ressources à vérifier la fiabilité de ses produits (et 30 % à leur conception). «Pour l'essentiel, on a recours à des techniques de simulation, remarque-t-il. On essaie de simuler les principaux scénarios de fonctionnement, mais il est impossible de reproduire tous les cas imaginables, puisque cela prendrait des milliards d'années.» Son équipe cherche par conséquent à concevoir diverses autres techniques de repérage systématique des failles en recourant notamment à des méthodes de raisonnement mathématiques. Elle conçoit entre autres des logiciels qui appliquent systématiquement cette démarche de raisonnement mathématique. «On obtient de la sorte une couverture exhaustive de tout ce qui est possible», indique le chercheur. Pour illustrer son approche, il évoque le grave accident survenu lors du premier tir d'une fusée Ariane V, en juin 1996. Cette Ariane 501 a explosé 40 secondes après son décollage, victime d'une panne de son système de navigation, ce qui a entraîné la perte des quatre satellites Cluster, d'une valeur de 370 millions de dollars. Les enquêteurs ont par la suite découvert que, parmi les milliers de lignes de code des logiciels contrôlant les ordinateurs de bord, une petite série avait été mal conçue. Selon un rapport de la NASA, le genre de méthode préconisée par Sofiene Tahar aurait probablement pu détecter la faille avant le tir de la fusée. Collaborations De fait, les travaux de l'équipe Tahar intéressent tellement les entreprises que, «chaque fois que nous obtenons des résultats intéressants, cela donne lieu à des collaborations avec des firmes à travers le monde», rapporte M. Tahar. C'est ainsi que son groupe travaille actuellement dans le cadre de trois partenariats, l'un avec la firme Erikson, de Montréal, un autre avec STMicroelectronics (le plus grand fabricant microélectronique en Europe) et un troisième avec Huway (le numéro un chinois des systèmes électroniques). «On essaie d'appliquer diverses techniques pour aider les industriels à vérifier leurs systèmes.» C'est ainsi que, il y a quelques années, l'équipe a scruté une composante électronique fabriquée par la société PMC-Sierra, l'un des grands fournisseurs de semi-conducteurs utilisés dans une foule d'équipements de communication. «Grâce à l'une de nos nouvelles techniques, basée sur des méthodes formelles, nous avons découvert une défaillance dans l'un des modes de fonctionnement du circuit électronique, raconte M. Tahar. Sur le coup, l'entreprise ne nous a pas crus, elle a donc refusé nos conclusions... mais elle a par la suite compris que nous avions raison.» De la probabilité à la certitude Prévoir les aléas de l'environnement? À l'occasion de sa présentation au congrès de l'ACFAS (lundi midi), M. Tahar traitera de l'application de la théorie des probabilités à l'identification des failles dans les systèmes. «C'est un domaine de recherche que nous avons commencé à explorer il y a quatre ans, précise-t-il. On a fait l'observation que beaucoup de systèmes ont un comportement probabiliste... Pensons simplement à la variation des conditions météorologiques; lorsqu'on place un système quelconque dans un environnement physique, il y a beaucoup de comportements qui dépendent de probabilités. Nous nous intéressons à la vérification des systèmes probabilistes, c'est-à-dire que ce n'est pas seulement le fonctionnement du système qu'il faut vérifier, mais son comportement probabiliste.» Cette démarche intéresse au plus haut point plusieurs autres chercheurs autant que des industriels. C'est ainsi que deux professeurs émérites de l'Université de Cambridge, en Grande-Bretagne, ont l'intention d'appliquer les méthodes mises au point par l'équipe de Concordia à un ensemble de domaines, notamment les télécommunications, la conception de logiciels, l'aviation et l'automobile. Par ailleurs, un gestionnaire de Rockwell Collins (un géant de l'avionique) a été si impressionné, lors de sa visite des laboratoires de M. Tahar l'été dernier, qu'il désire absolument collaborer avec lui. «Les choses vont vraiment très vite pour nous!», remarque Sofiene Tahar avec enthousiasme. *** Collaborateur du Devoir *** - «Formal Probabilistic Analysis Using Theorem Proving», le lundi 11 mai à 15 heures. http://www.ledevoir.com/2009/05/02/248474.html (2/5/2009 9H07)