Ingénierie - À la traque des défaillances catastrophiques Engineering - tracking catastrophic failures
Mots clés : Acfas, Sofiene Tahar, Ingénierie, Science, Université, Canada (Pays) Keywords: Acfas, Sofiene Tahar, Engineering, Science, University, Canada (Country)
Tout ce que vous avez toujours voulu savoir à propos de la « Formal Probabilistic Analysis Using Theorem Proving » Everything you ever wanted to know about "Probabilistic Formal Analysis Using Theorem Proving"
Photo: Agence France-Presse Photo: Agence France-Presse
«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. " "What we do in our laboratory is try to identify all possible scenarios to not let escape one that may be catastrophic," said Sofiene Tahar, an electrical and computer engineer who heads the team of 25 researchers of the Hardware Verification Group at Concordia University. 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. His research touches every system in our life, from networks of wireless communication to aircraft, via software, and microelectronics chips. «Je me passionne pour le fonctionnement des systèmes, qu'il s'agisse de logiciels ou de matériels», dit-il avec enthousiasme. "My passion is for correct systems functionality, whether software or hardware," he says enthusiastically.
D'origine tunisienne, Sofiene Tahar a entrepris ses études universitaires en Allemagne avant de venir les compléter ici. Originally from Tunisia, Sofiene Tahar began his university studies in Germany before coming here. «J'ai passé dix ans en Allemagne et je voulais acquérir une expérience nord-américaine, dit-il. "I spent ten years in Germany and I wanted to acquire a North American experience," he says. 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. In 1995, I was hired as a postdoc at the University of Montreal and the following year I obtained a faculty position at Concordia University. Je suis donc demeuré à Montréal..., ce que je ne regrette surtout pas!» I therefore remained in Montreal ... what I particularly do not regret at all! ";
Pour sauver Ariane To save Ariane
Aurait-on pu sauver Ariane 501? Could we have saved Ariane 501? M. Tahar s'émerveille devant la complexité des systèmes que l'industrie développe de nos jours. Dr. Tahar marvels at the complexity of the systems developed by the industry today. «Prenez par exemple le microprocesseur Pentium d'Intel, dit-il. "Take for example the Intel Pentium microprocessor, he said. Celui-ci contient plus d'un milliard de transistors! It contains more than one billion transistors! We do have the technology to manufacture this kind of "monster", but how do we ensure it works correctly?" In fact, the microelectronics and software industry spends about 70% of its resources to check the reliability of its products (and 30% into designing them). "In essence, we resort to simulation techniques, he says. Trying to simulate the most important scenarios of operation, but it is impossible to imagine all cases, since it would take billions of years." 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. His team seeks to develop other techniques for locating systematic flaws in particular by using methods of mathematical reasoning. They design, among others, software programs that systematically apply this approach of mathematical reasoning. "We this way we obtain an exhaustive coverage of all possibilities," says the researcher. 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. "There have been such exhaustive coverage of all that is possible," says the researcher.
Pour illustrer son approche, il évoque le grave accident survenu lors du premier tir d'une fusée Ariane V, en juin 1996. To illustrate his approach, he points to the serious accident that occurred during the first firing of an Ariane V rocket in June 1996. The Ariane 501 exploded 40 seconds after takeoff, victim of a failure of its navigation system, which resulted in the loss of the four Cluster satellites, worth $ 370 million. Investigators have subsequently discovered that among the thousands of lines of software code controlling the onboard computers, a small series was poorly designed. According to a report from NASA, the kind of approach advocated by Sofiene Tahar could probably have detected the fault before the firing of the rocket. 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 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. In fact, Dr. Tahar's team interested companies so that "whenever we get interesting results, this leads to collaboration with companies throughout the world," says Tahar. So his group is currently working in three partnerships, one with the firm Ericsson in Montreal, another with STMicroelectronics (the largest microelectronics manufacturer in Europe) and a third with Huawei (the number one Chinese electronic systems company). 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 ya 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. "We try to apply various techniques to help industrial manufacturers verify their systems." Thus, a few years ago, the team scrutinized electronic components designed by the company PMC-Sierra, a major Canadian supplier of semiconductors used in a range of communication equipment. "With one of our new techniques, based on formal methods, we found a failure in one mode of operation of the electronic circuit," says Tahar. At first, the company did not want to believe us, it had refused our findings ... but they then realized that we were right. " «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 From probability to certainty
Prévoir les aléas de l'environnement? Predict the environmental risks? À 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. At his presentation at the Congress of the ACFAS (Monday noon), Dr. Tahar will discuss the application of probability theory to identify vulnerabilities in systems.
«C'est un domaine de recherche que nous avons commencé à explorer il ya quatre ans, précise-t-il. "This is an area of research we have begun to explore four years ago, he says. It was observed that many systems have a probabilistic behavior ... Just think of the change in weather conditions when a particular system is placed in a physical environment, there are many behaviors that depend on probabilities. We are interested in the verification of probabilistic systems, i.e., we not only look at the system operation, but also its probabilistic behavior. " 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 ya 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. This approach is of greatest importance to several other researchers as well as to the industry. For instance, two prominent professors from the University of Cambridge, Great Britain, intend to apply the methods developed by the team at Concordia to a number of areas, including telecommunications, software design, aviation and automotive. In addition, a manager of Rockwell Collins (a giant in avionics) was so impressed when he visited the laboratories of Dr. Tahar last summer, that he wants absolutely to work with him. 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. "Things are going really fast for us", says Tahar Sofiene enthusiastically.
*** ***
Collaborateur du Devoir Friend of Duty
*** ***
- «Formal Probabilistic Analysis Using Theorem Proving», le lundi 11 mai à 15 heures. - Probabilistic Formal Analysis Using Theorem Proving ", on Monday 11 May to 15 hours.
Vos réactions Feedback
Merci Monsieur Lafleur - par Michel Virard (mvirard@videotron.ca) Thank you Lafleur - by Michel Virard (mvirard@videotron.ca)
Le dimanche 03 mai 2009 14:00 Sunday 03 May 2009 14:00