Résultats liés à « Biologie »

Réguler la barrière hémato-encéphalique
Benoit Vanhollebeke

Comment se mettent en place les barrières biologiques qui protègent le cerveau ?
Comment les franchir pour traiter les maladies du système nerveux central ?
Comment les restaurer lorsqu’elles sont déficientes ?

Dernières nouvelles:

Le Pr. Vanhollebeke présente ses recherches en vidéo

  • Le Prof. Benoit Vanhollebeke perce un mystère de la communication cellulaire – article dans Science. Lire le communiqué de presse: FR_Science_BVanhollebeke_Wnt signaling
  • Le Prof. Benoit Vanhollebeke fait partie des lauréats du Welbio Starting Grant 2017
  • L’équipe du Prof. Vanhollebeke décrit le mécanisme qui régit la formation des vaisseaux sanguins de notre cerveau (eLIFE, 8.6.2015) Communiqué de presse eLife
L’image de gauche est une reconstruction par microscopie confocale du réseau vasculaire cérébral d’un embryon normal, celle de droite celui d’un embryon qui est génétiquement déficient pour le complexe que nous avons découvert.

Biographie

Né en 1979. Docteur en Sciences, ULB (2008), Master en Sciences, ULB (2004), Bioingénieur, UCL (2003). Postdoctorat à l’University of California (San Francisco) dans le laboratoire du Pr. Didier Stainier. Benoit Vanhollebeke est Professeur assistant et chercheur au sein de l’Institut de Biologie et de Médecine Moléculaires (IBMM, ULB).

Cliquez ici pour lire davantage à ce propos

Projet

1. Les enjeux

barrire (1)Le cerveau est bien protégé. Abrité des chocs par la boîte crânienne, les méninges et le liquide céphalorachidien, il est en outre équipé d’un filtre biologique complexe: la barrière hémato-encéphalique. Cette interface hautement contrôlée entre le système sanguin périphérique et le système nerveux central assure l’homéostasie du liquide qui baigne le cerveau et le protège des pathogènes et des neurotoxines qui circulent dans le sang.

Les fonctions d’isolement et de protection du cerveau font cependant de cette barrière un obstacle majeur dans le traitement des maladies du système nerveux central, en excluant plus de 98% des molécules thérapeutiques potentielles.

A contrario, une barrière endommagée génère une accumulation excessive de fluide dans le cerveau qui participe à la physiopathologie d’un grand nombre de maladies telles l’accident vasculaire cérébral, les maladies neurodégénératives ou les pathologies neuroinflammatoires.

La recherche biomédicale sur la barrière hémato-encéphalique poursuit donc deux objectifs opposés : restaurer ses fonctions protectrices lorsqu’elle est endommagée et développer des méthodes permettant aux molécules thérapeutiques de la franchir.

barrire2 (1)

2. Le substrat anatomique: l’endothélium cérébral

vaisseauxCouplé à la pompe cardiaque, le système vasculaire véhicule les gaz dissous, les nutriments et les cellules sanguines à travers les différents organes du corps humain. Au sein de chaque organe, les cellules endothéliales qui tapissent les vaisseaux sanguins se spécialisent pour s’adapter aux nécessités locales.

Dans le foie, lieu de métabolisme privilégié, et dans de nombreux autres organes, la paroi de l’endothélium est poreuse et les échanges de part et d’autre des vaisseaux sanguins sont importants. En revanche, l’endothélium cérébral adopte un ensemble de propriétés, collectivement appelées barrière hémato-encéphalique, qui exercent un contrôle très strict sur la pénétration de molécules et de cellules dans le cerveau.

Le fonctionnement optimal des connexions synaptiques du cerveau requiert en effet un environnement ionique stable que la barrière hémato-encéphalique aide à maintenir. Elle exerce aussi un rôle protecteur en isolant le système nerveux central des composés – endogènes ou exogènes – qui circulent dans le sang et en excluant les pathogènes périphériques.

3. L’objectif fondamental : déchiffrer les signalisations de l’unité neurovasculaire

L’étanchéité de la barrière hémato-encéphalique repose sur diverses adaptations morphologiques et biochimiques des cellules endothéliales cérébrales: complexité des jonctions intercellulaires, limitation du trafic intracellulaire, expression d’une large gamme de transporteurs et d’enzymes métaboliques.

Ces différentes adaptations sont le fruit d’une communication complexe entre les cellules endothéliales et divers composants cellulaires et acellulaires associés, qui ensemble forment une entité fonctionnelle cohérente, l’unité neurovasculaire.

Nous cherchons à définir le dialogue moléculaire entre les cellules endothéliales, les péricytes qui leur sont étroitement accolés et avec qui elles partagent une épaisse membrane basale, les astrocytes dont les projections tapissent la paroi des capillaires, les neurones qui les entourent et les cellules microgliales.

Plus particulièrement, notre approche s’articule autour de trois questions:

Quelle est la nature moléculaire des signaux qui instruisent les différentes caractéristiques de la barrière hémato-encéphalique au cours du développement embryonnaire et la maintiennent chez l’adulte?

Quelle est la source cellulaire de chacun de ces signaux?

Comment sont-ils perçus et interprétés par les cellules endothéliales?

Notre objectif à long terme est de développer, sur base de ces connaissances, des stratégies permettant de réguler la barrière hémato-encéphalique à des fins thérapeutiques.

4. Le défi : de nouvelles approches.

a. Un vertébré transparent: le poisson-zèbre

embryon_zebra

La mise en place de la barrière est précoce tant d’un point de vue développemental qu’évolutif.

Les vaisseaux sanguins gagnent leurs propriétés de barrière aussitôt qu’ils envahissent le tissu cérébral. Comprendre les mécanismes qui gouvernent l’instruction de la barrière hémato-encéphalique relève donc de la biologie du développement.

L’étude de la perméabilité vasculaire chez la souris de laboratoire, modèle de référence, est compliquée par la dispersion du système vasculaire au sein d’un tissu opaque.

La conservation évolutive de la barrière hémato-encéphalique permet cependant son étude chez des organismes vertébrés dont les caractéristiques de développement sont plus adaptées à l’évaluation des perméabilités vasculaires.

En particulier, nous centrons nos efforts sur l’utilisation d’un modèle vertébré en plein essor, le zebrafish ou poisson zèbre, qui possède les grands avantages d’être ovipare et transparent pendant son développement embryonnaire. Ces caractéristiques, combinées à sa petite taille, sa grande fertilité et la palette d’outils génétiques disponibles pour son étude, en font un modèle de choix pour la recherche en biologie vasculaire.

Les divers avantages de ce poisson tropical nous permettent donc de contourner les difficultés techniques qui ont traditionnellement ralenti la recherche sur la barrière hémato-encéphalique et de visualiser pour la première fois ses fonctionnalités en temps réel.

Nous utilisons une combinaison de criblages génétiques et chimiques, de transgénèse et de génération de mutants pour découvrir les molécules et les voies de signalisation qui gouvernent la mise en place et la pathophysiologie de la barrière hémato-encéphalique.

criblage

b. Un parasite ouvre la voie: le trypanosome africain

Dans notre recherche de moyens pour franchir la barrière hémato-encéphalique, nous nous inspirons des solutions évolutives mises en place par certains pathogènes microbiens dont le cycle de vie implique la colonisation du système nerveux central.

Nous focalisons notre attention sur le trypanosome africain, un parasite extracellulaire tropical qui provoque des ravages en Afrique subsaharienne en causant la maladie du sommeil. Ce parasite tue son hôte mammifère après avoir traversé la barrière hémato-encéphalique par des mécanismes encore mal connus.

Nous exploitons les techniques génétiques de parasitologie moléculaire pour disséquer l’interaction entre le parasite et les cellules endothéliales, afin d’une part de révéler de nouvelles stratégies de traversée de la barrière et d’autre part de mettre le parasite en défaut en bloquant son invasion du cerveau.

5. Un réseau collaboratif

La recherche en biologie vasculaire bénéficie grandement de la complémentarité des modèles zebrafish et murin. Alors que les caractéristiques du premier le positionnent idéalement pour découvrir de nouveaux gènes ou voies de signalisation difficilement prévisibles, le second offre un cadre physiologique de référence et d’autres outils génétiques et biochimiques permettant d’élargir l’analyse.

Dans ce contexte, une étroite collaboration a été établie depuis plusieurs années avec un expert de la barrière hémato-encéphalique chez la souris, le professeur Richard Daneman de l’Université de Californie à San Francisco.

Par ailleurs, le laboratoire garde des contacts privilégiés avec le laboratoire du professeur Didier Stainier (Max Planck Institute for Heart and Lung Research), et celui du professeur Etienne Pays (ULB), des experts de la biologie du zebrafish et du trypanosome africain respectivement.

6. Un financement déterminant

Ce projet ambitieux et novateur sert de base à l’établissement du laboratoire du Dr. Benoit Vanhollebeke au sein de l’Institut de biologie et de médecine moléculaires (IBMM) de l’ULB.

Cet institut multidisciplinaire regroupe plus de 250 scientifiques issus de la faculté des Sciences et de la faculté de Médecine. L’Institut d’Immunologie Médicale (IMI) et du Centre de Microscopie et d’Imagerie Moléculaire (CMMI) viennent compléter ce pôle d’excellence de l’ULB.

A travers ce financement catalyseur, non seulement un nouveau laboratoire sera créé, mais plus généralement une large communauté scientifique de l’ULB, et de l’IBMM en particulier, sera dotée d’un outil expérimental moderne qui permet régulièrement des découvertes majeures dans des domaines aussi variés que l’immunologie, la biologie cellulaire, les cellules souches, la régénération tissulaire, la biologie vasculaire, ou les neurosciences.

Autre

La fiche du projet disponible en PDF ici.

Des cellules souches aux circuits neuronaux
Pierre Vanderhaeghen

Cellules souches : mécanismes et applications aux maladies neurologiques.

Dernières nouvelles:

  • Etude publiée dans Cell Reports
  • Article dans The Economist , 31 Mars 2018 – Evolution: A history of big-headness
  • Le cerveau humain est un organe remarquable, mais comment a-t-il évolué jusqu’à nous donner ces capacités intellectuelles hors du commun ? L’équipe de recherche de Pierre Vanderhaeghen (ULB, WELBIO, VIB, KU Leuven) s’est tournée vers le génome pour trouver des réponses à cette question. Dans le dernier numéro de Cell, les chercheurs montrent qu’un ensemble de gènes qui ne sont présents que chez l’humain contrôlent des étapes clé du développement du cerveau. Ces gènes pourraient réguler la taille du cerveau spécifiquement chez l’humain; les implications de cette découverte sont importantes pour l’évolution et les maladies du cerveau humain – communiqué de presse CELL 31.5.18
  • Pierre Vanderhaeghen (ULB), Bart de Strooper (KUL) et Jean-Pierre Brion (ULB), révèlent que contrairement aux neurons de souris, les neurones humains sont extrêmement vulnérables à la maladie d’Alzheimer (Neuron, Mars 2017) – communiqué de presse – Neuron 2017
  • L’équipe de Pierre Vanderhaeghen démontre l’efficacité des nouvelles cellules cérébrales greffées (Neuron, 5 mars 2015 > PRESS RELEASE FREN ) Pour en savoir plus
  • Pierre Vanderhaeghen remporte un prestigieux European Research Council Advanced Grant
  • Pierre Vanderhaeghen est titulaire de la Chaire Axa in Neuroscience and Longevity
  • Pierre Vanderhaeghen publie une première mondiale en transplantant des cellules nerveuses du cortex cérébral humain sur un cerveau de souris qui se connectent avec celui-ci de façon fonctionnelle.

 

Biographie

PVDHPierre Vanderhaeghen. Né en 1967. Docteur en médecine (ULB), Docteur en Sciences biomédicales (ULB),  Chercheur et Professeur à l’ULB, Chercheur au sein du Vlaams Instituut voor Biotechnologie et KUL Center for Brain&Disease,  Co-Directeur de l’Institut de Recherche Interdisciplinaire en Biologie Humaine et Moléculaire (I.R.I.B.H.M., ULB), Titulaire de la Chaire Axa « Neuroscience et Longévité ». Membre de l’Académie Royale de Médecine de Belgique. Avec son équipe, il a découvert des mécanismes importants du développement cérébral et a développé un modèle original de développement du cortex à partir de cellules souches de souris. Il est lauréat de nombreux prix dont: le Prix Francqui (2011), Prix Roger de Spoelberch (2010), Prix Solvay (2009), Prix Clerdent (2008), Prix UCB (2006), Prix Horlait-Dapsens (1996), Prix Specia (1992), Prix Fleurice-Mercier (1987).

Le projet

1 – ETAT DE L’ART

Le cortex cérébral est l’une des structures les plus importantes de notre cerveau: c’est lui qui contrôle nos mouvements, nos perceptions, et nos fonctions cognitives supérieures. Il est aussi la cible de nombreuses maladies neurologiques (accidents vasculaires, maladies dégénératives, troubles neuropsychiatriques, épilepsies), dont les causes restent souvent mystérieuses et dont la plupart restent incurables aujourd’hui.

Si la complexité du cortex lui confère sa puissance fonctionnelle, elle rend aussi son étude particulièrement difficile. Face à ce constat, notre équipe a développé des approches innovantes permettant de générer des « modèles réduits » du cerveau, s’appuyant sur les technologies émergentes des cellules souches pluripotentes (cellules ES embryonnaires et iPS induites à partir de fibroblastes de peau). Récemment, nos travaux ont ainsi permis de montrer que les cellules ES peuvent être transformées en neurones du cortex, selon un mécanisme qui récapitule une grande partie de la complexité corticale, mais au sein de boîtes de cultures cellulaires. Ces neurones peuvent ensuite être greffés au sein de cerveaux de souris, et sont alors capables de développer des projections nerveuses spécifiques avec le cerveau hôte.

2 – OBJECTIFS

La question cruciale de la fonctionnalité de ces neurones dans le cerveau après la greffe reste cependant incomplètement résolue, en particulier du fait des difficultés techniques des études fonctionnelles.

Cette question est non seulement importante d’un point de vue fondamental, mais aussi dans la perspective à plus long terme de l’utilisation de telles approches dans des stratégies de réparation de lésions du cortex cérébral, en général incurables aujourd’hui. C’est ce que nous nous proposons d’étudier dans le présent projet, en utilisant une approche multidisciplinaire, combinant techniques de biologie moléculaire, neuroanatomie, neurophysiologie et imagerie fonctionnelle, disponibles au sein de notre équipe et en collaboration avec d’autres groupes d’excellence de neurosciences de l’ULB.

Spécifiquement nous nous proposons d’appliquer une technique de développement très récent, l’optogénétique (jugée ‘technology of the year’ par la revue Science en 2010), qui permet de stimuler les neurones de façon spécifique par l’expression de protéines-canaux particulières, appelées ‘channelorhodopsins’ ou ChR, qui peuvent exciter les neurones après stimulation sélective par un rayon de lumière approprié. Cette technologie, qui révolutionne actuellement de nombreux autres domaines de la recherche sur le cerveau, permettra de contrôler avec une grande précision et efficacité l’activité des neurones greffés, et uniquement ces neurones, ce qui permet de réaliser des expériences fonctionnelles complexes avec une spécificité et une sensibilité inégalées.

cellules_souches_vers_neurones

3 – APPROCHES EXPERIMENTALES ET MISE EN OEUVRE

  •  Ce projet ambitieux nécessitera tout d’abord la génération de cellules souches, de souris ethumaines, exprimant la protéine ChR, par des techniques de biologie moléculaire et cellulaire maîtrisées au laboratoire.
  •  Ces cellules seront ensuite différenciées en neurones du cortex cérébral, grâce aux technologies spécifiques de ‘corticogenèse’ que notre laboratoire a inventées (Gaspard et al., Nature 2008;Nature Protocols 2009).
  •  La fonctionnalité de l’approche sera d’abord contrôlée, en combinant stimulation lumineuse et enregistrements électrophysiologiques in vitro, afin de vérifier la faisabilité de l’approche.
  •  Enfin, la stimulation optogénétique sera réalisée sur des neurones après greffe intracérébrale(chez la souris) grâce à des microfibres optiques, et le fonctionnement cérébral sera étudié par une combinaison de techniques d’enregistrements électrophysiologiques (ex vivo et in vivo), d’imagerie fonctionnelle, et d’analyse comportementale.
  •  Ces différentes approches seront tout d’abord réalisées avec des cellules souches embryonnaires de souris. Elles seront ensuite implémentées aux cellules ES et iPS humaines.

Cette approche multidisciplinaire nécessitera de nombreuses compétences complémentaires qui ne peuvent se retrouver au sein d’un seul groupe: elle sera donc réalisée en collaboration avec d’autres équipes de Neurosciences fondamentales et cliniques de l’ULB (laboratoires de Neurophysiologie, de Cartographie Fonctionnelle du Cerveau, et de Neurologie Expérimentale). Il bénéficiera également de nos contacts collaboratifs avec des groupes pionniers des technologies optogénétiques (Prs. K. Deissenroth, Stanford U., USA; A. Adamantidis, McGill U., Canada). En termes de moyens, le projet nécessitera en particulier (cf budget en annexe):

– l’acquisition d’équipements spécifiques (microfibres optiques, sources lasers)

– l’achat de matériel consommable (culture de cellules souches et chirurgie de souris)

– l’engagement de personnel hautement qualifié (chercheur postdoctoral).

Ce projet ‘high risk / high gain’, à la frontière des technologies des cellules souches et des neurosciences, permettra de progresser de façon importante dans notre compréhension de la fonction de neurones générés à partir de cellules souches, et d’étudier les mécanismes par lesquels ces neurones peuvent contribuer à la fonction cérébrale, et ainsi potentiellement à la réparation de lésions du cerveau.

BUDGET SUR BASE ANNUELLE

La durée du projet est évaluée à quatre ans.

NB: Etant donné son caractère risqué et multidisciplinaire, ce projet ne bénéficie à l’heure actuelle d’aucun financement spécifique.

Cliquez ici pour dérouler le tableau du budget

Voir aussi l’Institut de Neuroscience de l’ULB – UNI

Téléchargez la fiche projet en pdf: des cellules souches aux circuits neuronaux

Quelques publications:

Pyramidal neurons derived from human pluripotent stem cells integrate efficiently into mouse brain circuits in vivoEspuny-Camacho I, Michelsen K, Gall D, Linaro D, Hasche A, Bonnefont J, Bali C, Orduz D, Bilheu A, Herpoel A, Lambert N, Gaspard N, Peron S, Schiffmann S, Giugliano M, Gaillard A, Vanderhaeghen PNEURON, 77, 440-56, 2013
Ephrin-B1 controls the columnar distribution of cortical pyramidal neurons by restricting their tangential migrationDimidschstein J, Passante L, Dufour A, Van Den Ameele J, Tiberi L, Hrechdakian T, Adams r, Klein R, Lie D, Jossin Y, Vanderhaeghen PNEURON, 79, 1123-35, 2013
BCL6 controls neurogenesis through Sirt1-dependent epigenetic repression of selective Notch targetsTiberi L, Van Den Ameele J, Dimidschstein J, Piccirilli J, Gall D, Herpoel A, Bilheu A, Bonnefont J, Iacovino M, Kyba M, Bouschet T, Vanderhaeghen PNATURE NEUROSCIENCE, 15, 1627-35, 2012
An intrinsic mechanism of corticogenesis from embryonic stem cellsGaspard N, Bouschet T, Hourez R, Dimidschstein J, Naeije G, Van Den Ameele J, Espuny-Camacho I, Herpoel A, Passante L, Schiffmann S, Gaillard A, Vanderhaeghen PNATURE, 455, 351-7, 2008
Ephrin signalling controls brain size by regulating apoptosis of neural progenitorsDepaepe V, Suarez-Gonzalez N, Dufour A, Passante L, Gorski J, Jones K, Ledent C, Vanderhaeghen PNATURE, 435, 1244-50, 2005

Les preuves mathématiques pour assurer la correction des systèmes informatiques embarqués et d’intelligence artificielle
Jean-François Raskin

Développement de nouveaux modèles mathématiques quantitatifs et hybrides pour les systèmes informatiques embarqués, d’intelligence artificielle et l’analyse de la dynamique des systèmes biologiques.

Dernières nouvelles:

  • L’équipe du Pr. Raskin est partenaire du projet « Verifying Learning Artificial Intelligence Systems » du programme interuniversitaire Excellence of Science 2017-2021 avec des   équipes de la KULeuven et de l’Université de Namur.
  • Le Pr. Jean-François Raskin est élu par ses pairs dans le « working group 2.2 » de l’International Federation for Information Processing.
  • L’équipe du Pr. Jean-François Raskin remporte une Action de Recherche Concertée Advanced 2016-2021
  • Pr. Jean-François Raskin reçoit un mandat de Professeur Francqui pour les années 2015-2018
  • Pr. Jean-François Raskin is awarded with the 2014 IBM Faculty Award
  • Pr. Jean-François Raskin is awarded with the 2014 the silver medal of the Kurt Gödel Society for his prototype of  automatic synthetis

Biographie

Né en 1972. Docteur en Sciences des Facultés Universitaires Notre-Dame de la Paix (Namur), Post-doctorat à UC Berkeley et au Max-Planck Institute de Saarbrücken. Professeur et ancien Président du Département d’Informatique de la Faculté des Sciences de l’ULB. Il a été notamment Professeur invité à l’Ecole Polytechnique Fédérale de Lausanne et à L’Ecole Normale Supérieure de Cachan.

Cliquez ici pour lire davantage à ce propos

Projet

1. APPLICATIONS COMPLEXES ET LOGICIELS CORRECTS

Screen Shot 2013-12-05 at 18.06.04

Aujourd’hui, de nombreuses applications complexes et critiques, telles que l’assistance au pilotage d’un avion ou la régulation du rythme cardiaque par un pacemaker, sont mises en œuvre à l’aide de programmes informatiques.

Pour ces applications critiques, il est primordial de s’assurer que le logiciel construit est correct.

Ecrire un logiciel correct est une tâche difficile. Un logiciel peut en effet comporter plusieurs centaines de milliers de lignes de code et une seule erreur dans un programme peut avoir des conséquences désastreuses.

Malheureusement,  il est encore plus difficile de prouver (mathématiquement) qu’un logiciel ne contient aucune erreur.  Aussi, des recherches sont menées pour concevoir des algorithmes, et donc des programmes informatiques, capables de construire des preuves de correction.

Notre projet de recherche se situe précisément dans le domaine fascinant de la « vérification assistée par ordinateur » (V.A.O). Dans ce cadre, nous développons de nouveaux modèles mathématiques et l’algorithmique nécessaire à leur analyse automatique.

2. AU-DELA DU MODELE BOOLEEN : EXTENSIONS QUANTITATIVES ET MODELES HYBRIDES

Screen Shot 2013-12-05 at 18.06.13Les modèles et les notions de corrections développés jusqu’à présent dans le domaine de la vérification assistée par ordinateur peuvent être qualifiés de « Booléens ». En effet, ils permettent d’établir qu’un programme est correct ou non. Ils ne permettent pas d’établir des critères de qualité plus fins.

Par exemple, un logiciel pour pacemaker doit opérer des choix en « temps réel » en fonction du comportement du cœur du patient. Si des arythmies sont détectées, le logiciel commande l’émission et l’intensité d’impulsions électriques qui auront pour effet de rétablir un rythme cardiaque plus adéquat.

La correction du logiciel qui pilote les impulsions électriques est donc primordiale. Au surplus, il faut trouver une solution qui soit la plus parcimonieuse possible. En effet, afin de garantir une qualité de vie optimale au patient, le pacemaker ne doit intervenir que si cela est nécessaire.

Pour modéliser cette notion d’optimalité, nous avons donc besoin de modèles mathématiques plus riches qui permettent de modéliser des quantités (comme la fréquence des interventions du pacemaker) et de raisonner sur ces dernières.

3.LE PROJET :  DEFINIR UNE THEORIE SOLIDE POUR DEVELOPPER DE NOUVEAUX OUTILS POUR LA VERIFICATION DE SYSTEMES COMPLEXES

Screen Shot 2013-12-05 at 18.06.25Pour développer ces nouveaux outils informatiques, nous avons besoin de faire des progrès dans notre compréhension des propriétés fondamentales des nouveaux modèles mathématiques envisagés et de leurs algorithmes d’analyse.

Théorie des automates et les logiques associées

La théorie des automates finis est un des socles fondamentaux sur lesquels reposent les algorithmes de vérification de propriétés de correction des logiciels embarqués.

Depuis quelques années, des travaux de recherche visent à étendre ces théories avec des aspects quantitatifs : soit en ajoutant des variables à valeurs numériques aux automates finis pour contrôler plus finement leur exécution, soit en considérant les automates non plus comme définissant une fonction Booléenne mais une fonction dont la valeur est prise dans un domaine  infini, comme les réels ou les rationnels par exemple.

Ces modèles de calcul plus riches permettent la modélisation de systèmes informatiques plus complexes.

Pourtant, de nombreuses questions fondamentales sur ces formalismes restent ouvertes : quelle est l’expressivité des différentes classes d’automates? quelles sont les logiques équivalentes aux automates?  quelles nouvelles notions de corrections peuvent être formalisées? ces formalismes sont-ils robustes ?

Algorithmes ou semi-algorithmes pour les modèles quantitatifs.

Les problèmes de vérification que nous devons considérer sur les modèles quantitatifs sont généralement plus complexes que pour les modèles classiques, d’un point de vue conceptuel mais également d’un point de vue calculatoire.

Plusieurs problèmes importants (comme le problème d’inclusion de langages) ont déjà été montrés indécidables pour les extensions quantitatives. D’autres problèmes restent décidables mais le coût de leur résolution est très nettement accru.

Néanmoins, pour les problèmes indécidables, il convient de comprendre la frontière de décidabilité et également de proposer des solutions approchées -basées par exemple sur l’interprétation abstraite- ou encore des semi-algorithmes symboliques afin d’obtenir des solutions qui ont un intérêt dans la pratique.

Pour obtenir des résultats significatifs dans ce domaine, nous avons donc besoin de faire des avancées majeures dans notre compréhension des problèmes situés à la frontière de l’informatique théorique et des mathématiques. Ces avancées seront la base de nouveaux outils informatiques d’analyse de systèmes complexes.

Les systèmes « hybrides »

Un système informatique embarqué est typiquement un système « hybride » puisqu’il vise à contrôler un processus physique -dont l’évolution est continue- par l’intermédiaire de décisions discrètes qui auront en retour un effet sur l’évolution continue du système.

Les systèmes biologiques sont également des systèmes de nature hybride. En effet, la concentration d’une protéine évolue de façon continue dans le temps alors que l’activation ou l’inhibition d’un gène résultant dans le changement de mode de fonctionnement biochimique d’une cellule est typiquement un événement discret.

Ce dernier point est important pour comprendre l’une des applications que nous visons.

4. APPLICATIONS VISEES : systèmes embarqués  et  modélisation des systèmes biologiques

VERS LA CERTIFICATION DES SYSTEMES EMBARQUES

Les systèmes informatiques embarqués sont une cible privilégiée pour ces nouveaux modèles mathématiques. Les nouveaux outils de vérification que nous développerons permettront une conception plus rigoureuse de ces systèmes informatiques embarqués. Ils permettront également de certifier leur correction à l’aide de preuves mathématiques.

Il y a actuellement une demande importante pour des avancées en vérification assistée par ordinateur dans des domaines aussi importants que l’informatique pour les applications spatiales, l’aéronautique, les équipements médicaux, les microprocesseurs, la sécurité nucléaire, etc.

MACHINE LEARNING ET SYSTEMES D’INTELLIGENCE ARTIFICIELLE

Recently, artificial intelligence (AI) has made substantial progresses in a series of applications domains: driverless cars, IBM’s Watson program, deep learning techniques for playing Go, are popular examples. But those recent AI’s progresses also trigger important new questions about the future: what AI systems will be able to do, what they should be allowed to do, and what the implications are for humans.

The ongoing debate has motivated the AI and computer science communities to investigate what constitutes “safe AI” and whether it is possible to develop such “safe AI” systems that can be trusted. Quoting Dr. Guruduth Banavar, Vice President of IBM Research: ”Artificial intelligence is not without its risks. But we believe the risks are manageable. And that the far greater risk would be to stifle or otherwise inhibit the development of a technology with the potential to greatly improve the quality of life around the world. […] To reap the societal benefits of AI systems, we will first need to trust it. […] Trust is built upon accountability. As such, the algorithms that underpin AI systems need to be as transparent, or at least interpretable, as possible.” In this project, we want to push this research agenda and we claim that AI systems must also be mathematically verifiable. The trust in system is particularly important for systems that are safety critical (this is the case for example for driverless cars).

Our project aims at providing theoretical foundations and algorithmic methods to support the design of safer artificial intelligence systems that use learning. Tackling this important, timely and ambitious research agenda, requires on the one hand, extending verification models, and design methodologies, and verification algorithms to cover AI systems that learn, and on the other hand, improving learning methods so that they provide guarantees that can be used in verification.

As a starting point for our research, we will build on mathematical models and algorithms that we have developed in a recent project founded by European Research Council. In the context of this project, we have generalized transition systems and automata – models of computation in the classical approach to verification – by the more flexible, and mathematically deeper, game-theoretic and stochastic frameworks.

We intend to pursue this research work in collaboration with researchers active in the area of learning and articifical intelligence. To this aim, we have recently established a collaboration with a world renowed team at KULeuven.

MODELISATION DES SYSTEMES BIOLOGIQUES

Notre projet inclut également un pan novateur qui vise spécifiquement la recherche en biologie.

En effet, les modèles mathématiques hybrides que nous développons sont également bien adaptés à la modélisation et l’analyse de la dynamique des systèmes biologiques.

Certes, les biologistes possèdent des outils performants pour la modélisation de leurs systèmes, mais ces outils sont basés principalement sur les équations différentielles, soit les mathématiques du continu.

Malgré une réelle demande provenant des biologistes pour des outils de modélisation hybrides, plus adaptés à la nature -même des systèmes qu’ils étudient, les avancées dans ce domaine sont encore timides : seulement une dizaine de laboratoires au monde travaillent sur cette question.

Pour progresser de manière significative dans ce domaine, nous collaborerons avec des collègues spécialisés en biologie théorique, notamment via l’engagement d’un post-doc formé à la modélisation des systèmes biologiques qui pourra nous fournir des études de cas réalistes sur lesquels nos nouveaux formalismes mathématiques pourront  être appliqués.

Notre recherche permettra donc de faire avancer la modélisation de la dynamique des systèmes biologiques en la rendant plus simple, plus efficace et en somme, plus proche de la réalité.

 

5. GROUPE DE METHODES FORMELLES et VERIFICATION ASSISTEE PAR ORDINATEUR (ULB)

Screen Shot 2013-12-05 at 18.06.34Le groupe « Méthodes Formelles et Vérification Assistée par Ordinateur » a été créé en 2000 au sein du Département d’Informatique de la Faculté des Sciences de l’ULB.

Le groupe est la référence belge dans le domaine de la vérification assistée par ordinateur (V.A.O.) et de nombreux chercheurs étrangers visitent régulièrement Bruxelles pour collaborer avec le groupe du Prof. Jean-François  Raskin.

Le groupe coordonne par ailleurs le Centre Fédéré en Vérification  du FNRS qui rassemble toutes les équipes universitaires belges actives dans le domaine de la V.A.O.

Le groupe est également très actif dans le concert de la recherche européenne et a participé  (comme membre ou coordinateur)  à plusieurs projets de recherche européens d’envergure : FP7 NoE, FP7 STREP, ESF Eurocores, ESF Networks, COST Actions, etc.

Dans les prochains mois, le groupe du Pr. Raskin participera également à un nouveau projet de recherche européen, financé par l’action Future and Emerging Technologies du 7e Programme Cadre qui visera à mettre au point de nouveaux outils de développement de systèmes informatiques complexes à l’aide de la théorie des jeux.

Le groupe a une expertise reconnue dans les thématiques suivantes: systèmes hybrides et temps-réels, systèmes à espaces d’états infinis, model checking, algorithmes symboliques basés sur les antichaînes, algorithmes de synthèse basés sur la théorie des jeux.

Budget sur 4 ans

RESSOURCES HUMAINES

Deux chercheurs post-doctorants avec une expérience de recherche en informatique théorique travailleront sur les fondations mathématiques et algorithmiques.

Ils développeront également des outils de vérification pour les nouveaux formalismes.

Ces chercheurs collaboreront avec un biologiste ayant une expertise en modélisation des systèmes biologiques pour appliquer les théories et outils développés.

FONCTIONNEMENT ET EQUIPEMENTS

Afin de développer l’expertise en modélisation des systèmes biologiques, des échanges scientifiques de moyenne durée seront organisés chez des collègues étrangers spécialisés dans la modélisation de tels systèmes à l’aide d’automates (IST Austria, UPenn et UC Berkeley).

Par ailleurs, des ordinateurs performants seront nécessaires au développement des outils informatiques pour l’analyse de modèles mathématiques complexes. Ces équipements seront également utilisés pour l’analyse de modèles de systèmes embarqués et de systèmes biologiques.

L’analyse de ces modèles requiert des ressources de calcul importantes et dédiées.

Cliquez ici pour dérouler le tableau du budget

Autre

La fiche du projet disponible au format PDF ici.