Thèmes de recherche :
Mes recherches visent améliorer le fonctionnement des systèmes informatiques distribués
Il s'agit de de reconsider les techniques d'analyse formelle largement répandues,
comme
la véfication de propriétés de logique temporelle,
ou
l'évaluation stochastique des performances des systèmes,
pour les amliorer dans un souci d'efficacité et les adapter au traitement de systèmes concrets,
souvent complexes et de très grandes tailles.
Des techniques compléntaires de réduction et de compression d'espace d'états ont été définies tels que
l'exploitation des symétries de fonctionnement des processus,
l'observation partielle des composantes du systèmes et
le codage symbolique des infomations conservées en mémoire.
Les approches proposées ont été mises en pratique pour des systèmes distribués
dont la spéfication est formellement décrite en résaux de Petri.
La version colorée de ces réseaux (dite symétrique)
a permis d'automatiser le calcul des symétries de façon particulièrement efficace.
Les réseaux de Petri récursifs temporels représentent une toute nouvelle extension
qui offre aux concepteurs la création dynamique de processsus concurrents et communiquants,
ainsi qu'une gestion temporisée de leurs événements.
Les premiers travaux ont permi d'exhiber des conditions suffisantes
pour une analyse d'accessibilité,
visant ainsi la véfication des propriétés de sûreté du système.
J'aborde aussi des techniques d'analyse de comportement dans le cadre de systèmes distribués dynamiques et complexes.
La difficult de l'analyse provient en particulier de la qualité de l'environnement,
souvent changeant de façon impredictible.
Dans un premier temps, des techniques formelles incluant la robustesse des circuits embarqués
plongés dans des environnements satellitaires perturbés
ont ? d?ntr? et mises en oeuvre.
Plus récemment, dans le cadre des systèmes d'intelligence ambiante dont le nombre
d'acteurs du système sont en nombre variable et en constante adaptation,
de nouvelles techniques de planification, semi-formelles et adaptatives, ont été définies
visant améliorer le comportement du système,
au regard des objectifs variables visés par chacun des acteurs.
Ces techniques sont mises en oeuvre dans le cadre d'un campus universitaire intelligent.
Mots clefs : model checking, logique temporelle, Eluation stochastique, graphe d'état quotient,
chaîne de Markov aggrégée, représentation symbolique, symétrie, observation, modularité
réseau de Petri, système à structure dynamique, système fini et infini, influence de l'environnement.
-
Projets
2016 : projet AmI sur l'intelligence ambiante (projet transversal LIP6)
-
Coopérations
laboratoire MISC - Université de Constantine
laboratoire informatique - Université USTHB ouari-boumédienne - Informatique