Résultats liés à « Nouvelles technologies »

IBM Faculty Award décerné au Pr. Jean-François Raskin

 jfraskinL’IBM Faculty award 2014 a été décerné au Pr. Jean-François Raskin pour ses contributions essentielles à la recherche sur la vérification assistée par ordinateurs. Le Pr. Jean-François Raskin développe en effet de nouveaux modèles mathématiques quantitatifs et hybrides pour les systèmes informatiques embarqués. Pour en savoir plus sur son projet

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

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

Dernières nouvelles:

  • 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.

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.

« Swarm intelligence » et robotique en essaim
Marco Dorigo

Interview de Marco Dorigo dans « les Chercheurs d’Avenir. »

La vidéo a remporté la compétition qui a mis l’équipe de Marco Dorigo face à des équipes prestigieuses provenant des institutions suivantes: NASA, MIT, Carnegie Mellon University, George Mason University, Technische Universitaet Munchen, University of California, Georgia Institute of Technology.

Dernières nouvelles:

  • Nouveau paradigme de coordination des systèmes multi-robots (Nature Communications, sept. 2017)

Il s’agit d’une avancée très significative dans le contrôle de systèmes multi-robots. En effet, auparavant, au sein d’un système multi-robots, chaque robot était indépendant et le paradigme de coordination était l’auto-organisation. Ceci implique une coordination stricte entre les robots, comme par exemple, dans le robot metamorphique (essaim composé de robots indépendants).  

Dans ce nouvel article, le Prof. Marco Dorigo prouve qu’il est possible d’obtenir cette coordination stricte via le concept de “mergeable nervous system”. 

Il a en effet montré qu’il est désormais possible à des robots de transférer toutes leurs informations/expériences et d’abandonner leur indépendance (merging) à un robot donné qui prendrait alors le contrôle de tout l’essaim.

https://www.nature.com/articles/s41467-017-00109-2

  • Le Prof. Marco Dorigo reçoit le IEEE Evolutionary Computation Pioneer Award 2016 pour ses recherches en intelligence artificielle.
  • Le Prof. Marco Dorigo reçoit le 21 avril 2015 les Insignes de Docteur Honoris Causa de l’Université de Pretoria.
  • Le Prof. Marco Dorigo reçoit le 2015 IEEE Frank Rosenblatt Award « pour ses contributions aux fondations de la swarm intelligence »
  • Le projet coordonné par Marco Dorigo « Swarmanoid » remporte le prix vidéo 2011 de l’ Association for Advancement of Artificial Intelligence et le Prix Wernaers 2012 pour la recherche et la diffusion des connaissances.
  • Marco Dorigo bénéficie de l’ ERC Advanced Grant 2010.

Biographie de Marco Dorigo

dorigo

Marco Dorigo, né en 1961. Docteur en Systems and Information electronic Engineering de l’Ecole Polytechnique de Milan (1992), Agrégé de l’Enseignement Supérieur de l’ULB (1995).

En savoir plus sur Marco Dorigo

Le projet

L'équipe de recherche du laboratoire du Dr. Marco Dorigo.

L’équipe de recherche du laboratoire du Dr. Marco Dorigo.

1. Intelligence artificielle et ingénierie robotique en essaim.

Le domaine de recherche du Pr. Marco Dorigo est l’ingénierie robotique en essaim, également appelée « swarm bot ».

Autrement dit la conception et la mise en oeuvre de système d’intelligence artificielle pour résoudre de multiples problèmes pratiques. Je m’inspire des modèles observés par les biologistes d’après l’étude des comportements des animaux sociaux, en particulier des fourmis pour créer des algorythmes qui vont permettre de programmer les robots.

2. Le « swarm bot » ou une collectivité de robots auto-organisés

Qui dit « swarm bot » dit collectivité de robots.

L’idée est de déveloper une légion de petits robots qui peuvent s’auto-assembler, interagir entre eux afin de se répartir une tâche à accomplir. Chacun fonctionnant à la fois en groupe et indépendamment les uns des autres. L’avantage réside dans le fait qu’ensemble, ils sont plus efficaces. Si l’un d’entre eux tombe en panne, les autres restent fonctionnels. Un aspect non négligeable lors d’une mission spatiale par exemple. En groupe, ils sont capables de franchir un obstacle, de se déplacer en terrain accidenté ou de porter une charge plus lourde.

Robots indépendants capables de s'assembler afin d'accomplir des tâches complexes

Robots indépendants capables de s’assembler afin d’accomplir des tâches complexes

3. Applications visées

A terme, on peut imaginer des applications telles que des interventions de secours lors de l’effondrement d’un immeuble ou l’envoi de robots dans un environnement hostile telle qu’une zone hautement radioactive, là où l’être humain ne peut opérer ou se déplacer.

Une "anarchytecture" accomplissant une mission et qui se désassemblera une fois la tâche achevée

Une « anarchytecture » accomplissant une mission et qui se désassemblera une fois la tâche achevée

4. L’avancée des recherches

Ce volet de la robotique est extrêmement novateur.

Aussi à l’heure actuelle, malgré les avancées significatives provenant notamment grâce à la recherche à l’ULB, il faut encore développer une méthodologie rigoureuse pour que le fruit de ces recherches puisse être appliqué.

Autres informations

Connaître le projet de Marco Dorigo en détails (en anglais) : Le projet en PDF

Quelques liens :

  • Marco Dorigo dans The Economist, le 14 août 2010 : Riders on a swarm © The Economist 2010
  • Marco Dorigo reçoit un prestigieux ERC Advanced Grant 2010 (en anglais) : cliquez ici

Budget (English)

The current expertise available at Prof. Dorigo’s lab covers all the necessities of the project except for the hardware construction of the robots. Accordingly, the main part of the requested funding is for the creation of a professorship in mechatronics oriented to the design and construction of advanced micro-robotic systems.  Additional funding is necessary for setting up a mechatronics lab. The goal is to fund the new chair for a period of five year and to have then the ULB taking over and provide the necessary funding for a permanent professor position. The necessary budget is estimated to 2,8 million of EUR over a period of 5 years, organized as follows:

Personnel

One senior researcher at professor level. Here the goal is to hire a mechatronics expert with proved research record in micro-robotics. The offered position will be “tenure track”, that is, it will become a permanent position after the end of the project.

One technician for the new mechatronics laboratory.

One postdoctoral researcher with a PhD in autonomous robotics and mechatronics.

One PhD student with a master in robotics.

Consommables

This concerns the material necessary for the construction of the robots.

Equipments

The set up of the new mecathronics laboratory will be the main investment. Additionally, computational nodes for running simulations will be necessary.

Develop budget table

The Marco Dorigo’s Projet explained in English

Click here to obtain the English version