Chroniques de : Chronic:
Autres dossiers �ducation Other records Education
- S'abonner Subscribe
- Foire aux Questions Frequently Asked Questions
- Le Devoir Le Devoir
- Flux RSS RSS feeds
- Publicit?/a> Advertising
- Horaire des films Schedule of films
- Petites annonces Classifieds
- Charme et prestige Charm and prestige
- Avis publics Public Notices
- Appels d'offres Calls for Tender
- M�t�o du Qu�bec Weather in Quebec
- Rencontres Meetings
- Carri�res Careers
Flux externes External Flow
Partenaires Partners
Ingénierie - À la traque des défaillances catastrophiques 工程 - 跟踪灾难性的故障
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 ?/em> 应用定理证明（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. 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. “我们的实验室所做的是试图找出所有可能的情况，不放过任何一个导致灾难的可能， ”Sofiene Tahar说。这位电气和计算机工程师在Concordia大学硬件验证组（Hardware Verification Group）领导25名研究人员。他的研究领域涉及我们的生活中从网络的无线通信网络到飞机的每一个系统，通过软件，微电子芯片。 “我的激情是确保系统正确的功能，无论是软件或硬件， ”他热情地说。
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!» 来到蒙特利尔之前，来自突尼斯 的Sofiene Tahar 在德国大学学习。 “我在德国学习了十年，我想获得一些北美的经验， ”他说。 “1995年，我在蒙特利尔大学做博士后,接下来的一年，我获得了Concordia 大学教师的职位。因此，我留在了蒙特利尔...我一点也不后悔！“ ;
Pour sauver Ariane 拯救 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.» 我们能拯救Ariane 501么 ？Tahar 教授对当今业界系统的复杂性感到惊讶。 “例如英特尔奔腾微处理器，他说。它包含超过10亿个晶体管！我们的确有技术制造这种”怪物“ ，但我们如何确保它正常工作？ ”事实上，微电子和软件产业花费大约70 ％的资源来检查其产品的可靠性（ 30 ％用来设计） 。 “从本质上讲，我们利用仿真技术”，他说。”试图模拟最重要操作的情况，但不可能想象去仿真所有情况，因为这需要数十亿年的时间。 ”
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. 为了说明他的做法，他指出，在1996年6月第一次发射的Ariane箭发生的严重事故。Ariane501发射40秒后爆炸，由于导航系统的失败，造成四个集群卫星的损失，价值3亿7千万美元。调查人员后来发现，在成千上万行的软件控制代码中，有一小组代码设计不当。据来自美国航天局的报道，Sofiene Tahar提倡的办法有可能在火箭失事前发现错误。
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). 事实上，Tahar教授的团队很高兴跟其它公司合作，“每当我们得到有趣的结果，都会与世界各地公司的合作。” Tahar说。他的小组目前有三个合作伙伴，爱立信蒙特利尔公司，意法半导体（欧洲最大的微电子制造商）和华为（中国排名第一的电子系统公司）。
«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.» “ 我们试着应用各种技术来帮助工业制造商验证他们的系统。 ”因此，几年前，该小组审查了PMC - Sierra公司设计的电子元件，这是一家加拿大生产各种通讯设备半导体部件的主要供应商。 “通过基于形式化方法的新技术，我们找到了电子线路的某个操作模式的故障“，Tahar 说： ”起初，该公司并不相信我们，他们拒绝接受我们的结果...但随后，他们认识到我们是正确的。 “mais elle a par la suite compris que nous avions raison.?/span>
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. 预测环境风险？在他的ACFAS 演讲中（星期一中午12时） ，Tahar 教授将讨论概率论在鉴别系统漏洞中的应用。
«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.» “我们在四年前已经开始探索这个领域," 他说。"有人指出，许多系统都有随机过程...试想放置在自然环境中的特定系统遇到天气变化。很多过程取决于概率。我们致力于随机系统的验证，也就是说，我们不仅观察该系统的运作，同时还有其随机行为。 “ 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.?/span>
Cette d�marche int�resse au plus haut point plusieurs autres chercheurs autant que des industriels. 这种方法对于其他一些研究人员以及工业极为重要。例如，英国剑桥大学的两位著名教授打算将Concordia团队开发的方法运用到一些领域，包括电信，软件设计，航空和汽车。此外，Rockwell Collins 公司（航空电子设备巨头）在去年夏天访问 Tahar 教授的实验室时留下了深刻的印象，他非常希望合作。
�Les choses vont vraiment tr�s vite pour nous!? remarque Sofiene Tahar avec enthousiasme. “这对我们来说来的太快了”， Sofiene Tahar 激动地说。
*** ***
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
R�agissez ?ce texte Comment on this
Publicit?- Un produit ou un service ? Advertising - A product or service? 