CentraleSupélec LMF, UMR CNRS 9021
Département informatique Laboratoire Méthodes Formelles
Bât Breguet, 3 rue Joliot-Curie Bât 650 Ada Lovelace, Université Paris Sud
91190 Gif-sur-Yvette, France Rue Noetzlin, 91190 Gif-sur-Yvette, France
Recherche

Table des matières

Modélisation hétérogène Modélisation

La modélisation d'un système complexe fait naturellement appel à différentes techniques de modélisation qui correspondent à des savoir-faire différents. La modélisation hétérogène permet de prendre en compte ces différentes approches dans la modélisation d'un système, ce qui permet d'utiliser la technique de modélisation la plus adaptée à chaque partie ou à chaque aspect du système.

Notre recherche porte sur la définition des interactions entre les différentes techniques de modélisation : comment interfacer un module réactif synchrone avec réseau d'opérateurs à flots de données, comment passer d'un temps discret non périodique à une séquence d'échantillons etc. Des travaux sont aussi menés sur la structure des interactions entre modèles : imbrication hiérarchique ou non, adaptation par traduction entre formalismes etc. Notre approche est opérationnelle : le but est de définir un modèle d'exécution qui permette de calculer le comportement du modèle du système ou de générer une implémentation du système à partir du modèle.

Un autre aspect de cette recherche est la vérification de propriétés du comportement de modèles hétérogènes, notamment par la modélisation formelle du recollement entre les traces d'exécution des composantes hétérogènes d'un modèle. Notre approche s'appuie sur la définition de langages permettant d'exprimer les contraintes sur les événements et l'écoulement du temps aux interfaces entres les composantes hétérogènes, avec un aspect denotationnel pour raisonner sur les propriétés, et un aspect opérationnel pour générer des traces à des fins de monitoring et de test.

Thèses encadrées

En cours

Baptiste Gueuziec
Raisonnement qualitatif et conception de systèmes complexes
LMF et CEA (Jean-Pierre Gallois), Université Paris-Sud


Soutenues

Valentin Fouillard
Modélisation et vérification de systèmes intégrants des facteurs humains
LRI, Université Paris-Sud (direction : Nicolas Sabouret), 2022
TheseVF-2022.pdf


Vassil Todorov
Intégration des méthodes formelles dans la conception des fonctions logicielles automobiles
LRI, Université Paris-Sud, CentraleSupélec, 2020
TheseVT-2020.pdf


David Oudart
Application de l'IDM aux systèmes de contrôle-commande des Smart Grids
EDF, LRI, CentraleSupélec et Université Paris-Sud, 2020
TheseDO-2020.pdf


Slim Medimegh
Analyse formelle de spécifications hybrides à partir de modèles SysML pour la validation fonctionnelle des systèmes embarqués
CEA, LRI, CentraleSupélec et Université Paris-Sud, 2018
TheseSM-2018.pdf


Hai Nguyen-Van
Formalizing Time and Causality in Polychronous Polytimed Models
LRI, Université Paris-Sud, 2018
TheseHNV-2018.pdf


Rachida Seghiri
Simulation orientée utilisateur des Systèmes d’Information des SmartGrids à base de modèles par points de vue
EDF, Université Paris-Sud XI et Supélec, 2016
TheseRS-2016.pdf


Daniel Chaves-Café
Modélisation Multi-paradigme pour la synthèse et la validation
de systèmes complexes en environnement multi-physique
Supélec et chaire Thales en conception analogique avancée, 2015
TheseDC-2015.pdf


Ayman Dogui
Modélisation explicite de l'adaptation sémantique entre modèles de calcul
Université Paris-Sud XI et Supélec, 2013
TheseAD-2013.pdf


Abderraouf Benyahia
Formalisation des sémantiques d'exécution hétérogènes pour la conception des systèmes embarqués
Université Paris-Sud XI et Supélec, 2012
TheseAB-2012.pdf


Bilal Kanso
Test des systèmes hétérogènes
École Centrale Paris et Supélec, 2011
TheseBK-2011.pdf


Cécile Hardebolle
Formalisation des modèles d’exécution et de leurs interactions
Université Paris-Sud XI et Supélec, 2008
TheseCH-2008.pdf


Mohammed Feredj
Études des méthodes de conception de composants domaine-polymorphes
Université Paris-Sud XI et Supélec, 2005
TheseMF-2005.pdf


Mokhoo Mbobi
Modélisation hétérogène non hiérarchique
Université Paris-Sud XI et Supélec, 2004
TheseMM-2004.pdf


Rapports

Ines Sarray
Conception de systèmes de reconnaissance d'activités humaines
Université de Nice - Sophia Antipolis
21 mars 2019
Sabine Moisan


Jérôme Hugues
Architecture in the Service of Real-Time Middleware, Contributions to Architecture Description Languages
HdR INP Toulouse
22 février 2017


Yann Hourdel
Towards an abstraction-compatible specification language for systems
École Polytechnique - LIX
7 décembre 2015
Daniel Krob


Thomas Friedlhuber
Model Engineering in a Modular PSA
École Polytechnique - LIX
26 septembre 2014
Antoine Rauzy, Mohamed Hibti


Carlos Ernesto Gómez Cárdenas
Modeling Functional and Non-Functional Properties of Systems Based on a Multi-View Approach
Université de Nice - Sophia Antipolis
20 décembre 2013
Frédéric Mallet, Julien DeAntoni


Boris Golden
A Unified Formalism for Complex Systems Architecture
École Polytechnique - LIX
13 mai 2013
Daniel Krob, Marc Aiguier


Mon HdR et ma thèse

Modèles, systèmes, hétérogénéité
Université Paris-Sud XI et Supélec, 2011
mémoire et présentation

Intégration de modules synchrones dans la programmation par objets
Université Paris-Sud XI et Supélec, 1993
mémoire

Réalisations

Tagged Events Specification Language

TESL est un langage (Tagged Events Specification Language) et une bibliothèque Java pour la spécification de la synchronisation de l'exécution de différentes parties de modèles hétérogènes. Il est utilisé dans ModHel'X pour synchroniser l'exécution des composantes hétérogènes d'un modèle. Il peut être utilisé seul pour décrire les relations temporelles et les relations de causalité entre des horloges, qui peuvent avoir des échelles de temps de nature et vitesse d'écoulement différentes.

Sa sémantique formelle est publiée dans l'archive des preuves formelles en Isabelle/HOL.

Travaux réalisés dans le cadre du projet Usine Logicielle du pôle de compétitivité System@tic

L'équipe de recherche « Systèmes et Informations Hétérogènes » a contribué aux sous-projets MoDriVal et OpenDevFactory du projet Usine Logicielle. Ces contributions sont distribuées sous licence Eclipse Public License et disponibles sur le serveur de logiciels du Département Informatique.

  • ModHel'X est une plateforme de modélisation hétérogène dotée d'un moteur d'exécution pour la simulation de modèles hétérogènes.
  • ADLV est un langage et un outil de description d'applications à contrôle synchrone qui permet de générer des observateurs pour le model-checking à partir de propriétés exprimées globalement sur l'application. ADLV permet aussi de déployer l'application sur la plateforme d'exécution microCCM (sous-projet Inflexion d'Usine Logicielle).

Modules synchrones et programmation par objets

Ces travaux, relativement anciens, consistent à intégrer l'approche réactive synchrone dans la programmation par objet. Cela se traduit par l'implémentation en C++ d'un modèle d'exécution pour modules réactifs synchrones libSync, d'un traducteur de code intermédiaire OC (généré à partir de code source Lustre ou Esterel) en classes C++ occ++, et d'un compilateur de description de module mdlc qui permet de créer de nouvelles classes synchrones par composition de classes synchrones existantes.

Le code source de ces outils, bien que toujours disponible, n'est plus maintenu et risque même de poser des problèmes de compilation.

Modules synchrones et Ptolemy Classic

Ptolemy est une plateforme de modélisation et de conception hétérogène. Elle permet d'utiliser conjointement différentes techniques de modèlisation, appelées domaines, pour modéliser un système.

Le traducteur ocpl permet de transformer la description d'un module synchrone en code intermédiaire OC en une étoile Ptolemy Classic d'un des domaines suivants : SDF, DE, SR, CGC et SRCGC.

Domaine SRCGC de Ptolemy Classic

Le domaine SR (Synchronous Reactive) conçu par Stephen Edwards pour Ptolemy Classic permet de combiner des modules réactifs synchrones en utilisant des boucles de retroaction instantannées. Le comportement du système est calculé par itération. Le nombre maximal d'itérations nécessaire pour atteindre le point fixe est déterminé par la topologie du système, ce qui permet de calculer un ordonnancement statique des modules qui le composent.

Dans le cadre d'une collaboration avec Thomson-CSF Optronique, Mathilde Roger et Vincent Legrand, élèves de troisème année en option Systèmes Informatiques à Supélec en 1997-1998, ont développé SRCGC, domaine de génération de code C dual de SR, sous ma supervision et celle de Xavier Warzee.