Sciences et Technologies de l'Information
Sommaire : Trois questions à Frédéric Blanqui, prix Specif | L'actualité de la semaine : | Dans les entreprises | Enseignement | Théories et concepts | La recherche en pratique | Manifestations | Le livre de la semaine | Détente |
 |
 |
 |
 |
| Vendredi 13 décembre prochain : le web sémantique, une vision de la toile à s'approprier. Une journé de l'AILF. Inscrivez-vous | Retenez la date : l'Asti organise sa première école d'été, à Saint-Malo/Dinard, du 1er au 12 septembre 2003. Thème fédérateur : "Image numérique interactive : créer, simuler, interpréter". |
"Je compte mener de front l'approfondissement théorique et les applications pratiques."
Asti-Hebdo : Votre thèse "Théorie des types et récriture" a été
primée par Specif. Elle va très loin dans l'abstraction de la logique et
de l'informatique théorique, et pourtant elle vise des objectifs pratiques et
mÍme industriels. Pouvez-vous nous préciser comment ?
Frédéric Blanqui : Mes recherches visent à améliorer les assistants à la démonstration utilisés dans la certification de programmes, de protocoles, etc. Pour prendre un exemple, significatif actuellement, les programmes Java enfouis dans les cartes à puce sont certifiés à l'aide d'assistants comme Coq, développé à l'Inria. D'autres chercheurs travaillent sur la certification de stimulateurs cardiaques, ou de systèmes de contrôle aérien à la Nasa.
Un tel travail de certification/preuve exige la formalisation de tout un environnement (sémantique des instructions. spécifications). Un outil comme Coq comporte donc à la fois un langage de programmation (en l'occurrence, comparable à ML), qui permet de définir des fonctions et de faire des calculs, un outil de description formelle des spécifications, et enfin le système d'aide à la démonstration qui permet d'établir la preuve à proprement parler à l'aide de tactiques semi-automatiques.
L'objectif de mon travail est de rendre ces systèmes d'aide à la démonstration plus souples et plus faciles à utiliser. L'idée maîtresse est de faciliter à l'utilisateur la définition des fonctions et des prédicats qu'il utilise. Dans un système comme Coq, les fonctions se définissent par récurrence. Ce mode d'expression n'est pas toujours très pratique. Il faut donc lui offrir un langage plus naturel et qui permette davantage d'automatisation. C'est le cas des langages à base de règles de réécriture. Ceux-ci ont aussi l'avantage de réduire la taille des preuves, qui peut devenir problématique dans certains cas.
Tout cela pose un certain nombre de problèmes théoriques et pratiques. Il faut en effet s'assurer de la cohérence logique d'un tel système, et aussi savoir si la correction des preuves faites par l'utilisateur peut Ítre effectivement vérifiée. D'o˜ l'aspect abstrait de ce travail passionnant.
Asti-Hebdo : Quel cheminement vous a conduit à ces questions ? Etes-vous au départ un logicien, un mathématicien, un informaticien ?
F.B. J'ai plutôt commencé par l'informatique, dans une optique pratique, puisque je suis entré à l' Ensimag. Je me suis ensuite intéressé à la logique, puis à l'informatique théorique. Mais, à vrai dire, les aspects théoriques m'ont toujours attiré. Dès mes études d'ingénieur, j'ai travaillé les mathématiques pures (à l'Institut Joseph Fourier de Grenoble).
C'est pourquoi, une fois obtenu mon diplôme d'ingénieur, après un séjour d'un an au Canada, je me suis lancé dans une thèse, à l'université d'Orsay, avec Jean-Pierre Jouannaud qui, à l'époque, dirigeait l'équipe Démons du LRI. Il est maintenant directeur du LIX, le laboratoire d'informatique de l'École polytechnique.
Cela m'a conduit à entrer en relations avec l'Inria, en particulier le projet Logical.
Asti-Hebdo : Comment allez-vous maintenant vous orienter ?
F.B. : Je vais poursuivre ma carrière de chercheur. Ma thèse apporte des solutions à un certain nombre de problèmes, mais il reste beaucoup de questions ouvertes et d'améliorations possibles.
Notez, par exemple, que les recherches sur la preuve de programmes se sont développées sur deux axes : vérification automatique et assistance à la démonstration. Actuellement, on observe une tendance à la coopération des deux communautés. En effet, d'une part, la vérification automatique a ses limites, qui appellent donc une intervention humaine. D'autre part les utilisateurs d'outils d'assistance sont demandeurs d'automatismes, quand ils sont possibles. Nous allons donc vers une intégration des deux types de systèmes.
Je compte mener de front l'approfondissement théorique et les applications pratiques. Je viens de faire un séjour post-doctoral à Cambridge (Royaume-Uni) sur la certification de protocoles cryptographiques. C'est dans ces perspectives que s'inscrit maintenant mon travail au LIX et ma collaboration à des projets comme Logical, de l'Inria. Vous trouverez plus de détails sur ma page web personnelle.
Le site de l'Information awareness office (Darpa).
"Depuis le 12 novembre 2002, à 21h précises - à líinstant mÍme o˜ le Premier ministre intervenait pour la première fois sur le thème du développement de la société de líinformation (présentation, notamment, du plan RESO 2007) - une nouvelle version graphique et ergonomique du site thématique www.internet.gouv.fr vous est proposée. Un site que nous souhaitons plus clair, plus pédagogique, plus ergonomique et donc plus facile à consulter. En attendant une version encore plus interactive. "
Le communiqué de l'April note : " Tout en se cachant derrière une écriture confuse, la Commission européenne ouvre la porte au brevetage des méthodes commerciales, des logiciels, des mathématiques, des idées ...alors qu'informaticiens et économistes s'accordent pour dire que le droit d'auteur suffit pour protéger les logiciels. Le brevet favorise les gros acteurs de type Microsoft et entrave l'innovation. La Commission propose en fait de légitimer la pratique illégale de l'Office Européen des Brevets, au lieu de reprendre le contrôle sur cette organisation."
Par ailleurs on trouvera sur le site d'April une note Informatique de confiance ou informatique déloyale ? relative à ces thèmes.
Principales conclusions (en résumé) :
Dans sa conclusion à la présentation publique de l'étude, Jean-Pierre Corniou, président du Cigref, a souligné les progrès, mais aussi appelé à poursuivre un travail en profondeur : "Nous manquons de métriques de performance... il faut rendre visibles les atouts des technologies bien employées... nous devons aider à développer la science (des SI), permettant de raisonner sur des objets identifiés et dans un langage commun. Il faut mettre de l'ordre dans les modèles... trop marqués par le marketing et les vaines promesses". P.B.
Pointeurs :
MIT
technology review ,
Lucene
Mais tout de mÍme, communique encore le CNRS, l'Observatoire des sciences et techniques (OST) a publié (télécharger en PDF) une analyse sur les participations françaises et internationales au 5e programme cadre de recherche et développement (PCRD). Líétude, consultable en ligne, comporte trois grandes parties : "Analyses internationales", "Analyses des participations françaises" et "Conclusions et perspectives".
Dans cette troisième partie, líOST souligne notamment "la montée en puissance" des laboratoires académiques français, facteur encourageant pour líentrée dans le 6e PCRD qui vient díÍtre lancé.
Session 1 : De l'utilité des standards et des normes pour décrire et partager
Session 2 : Entre nouveauté et continuité, des enjeux à l'appropriation
Le formulaire
de pré-inscription en ligne
Les renseignements : téléphone et télécopie :=
01 43 73 32 82 - mél. : lexipraxi@ailf.net
L'organisateur est Patrick Saint-Jean.
Intitulé Guide du management des systèmes d'information, l'ouvrage fera référence. Le corps du texte est encadré de définitions et de références bibliographiques ainsi que de pointeurs sur des sites web. Il est clair que les auteurs ont pensé par priorité à leurs collègues enseignants. On s'en convaincra par comparaison avec "Le bon usage des technologies expliqué au manager" (Alain Fernandez, Editions d'organisation 2001), nettement plus "In"voire "buzzwords". Ici, tout privilégie le sérieux et la construction logique, dans le détail aussi bien que dans le plan d'ensemble, en trois parties :
Pour "classique" qu'il soit, l'ouvrage est bien de son temps. On appréciera en particulier l'ouverture sur un thème qui est aujourd'hui central pour le DSI au coeur de son entreprise : l'alignement stratégique, et son complément architectural, l'urbanisation fonctionnelle. Et sur le plan technique, la large place faite aux orientations du jour : EAI, XML, UMTS... mais tout de mÍme pas Web sémantique ni mÍme Multimédia.
Confortablement installé à la maison dans son fauteuil, l'ordinateur sur les genoux, la victime - un homme de 50 ans, père de deux enfants - s'était plongée dans la rédaction d'un rapport pendant près d'une heure, selon une lettre adressée au Lancet, un hebdomadaire médical britannique paraissant samedi.
Le jour suivant, il a commencé à développer des cloques douloureuses sur le prépuce et le scrotum, qui se sont ensuite infectées, puis ont disparu sans nécessiter d'antibiotiques. Le chercheur s'est souvenu avoir légèrement déplacé l'ordinateur, alors qu'il était absorbé par son ouvrage, pour se débarrasser d'une sensation de bršlure.
Les manuels conseillent habituellement de ne pas poser l'ordinateur portable directement sur la peau, mais en l'occurrence le patient était habillé. "Cette histoire doit Ítre prise au sérieux", écrit l'auteur de cette correspondance, Claes-Goran Ostenson de l'Institut Karolinska de Stockholm (département de médecine moléculaire).