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

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.

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.