Génie Logiciel et Systèmes Distribués

Chef d'équipe: Belala Faiza

Thématique de recherche:

- Spécification et vérification formelles des systèmes répartis. Plusieurs études sont menées pour découvrir les avantages et les limites de chacun des modèles largement répandus dans le domaine des spécifications de systèmes concurrents. Plusieurs modèles  algébriques et logiques ont été proposés, ils sont attrayant  d'un point de vue théorique et  de part leur simplicité.

- Modélisation formelle des applications Cloud/Fog/Edge. Dans le contexte des systèmes émergents (Cloud, Fog, Edge, CPS, etc.), nous nous retrouvons en face d’un décalage néfaste entre la théorie (modèles formels et technique de vérification) et la pratique (standards et application industrielle).  et dans le souci de combler cet écart, nous proposons des méthodes formelles — basées sur la logique de réécriture et le langage Maude et les bigraphes de Milner pour  étudier ces systèmes d'actualité.

- Architectures Logicielles et Systèmes de Systèmes. Exploitation de certaines techniques formelles pour la spécification et l’analyse des applications  architecturales dynamiques : Le développement de modèles et langages pour la  description et la spécification d’architectures est crucial pour  répondre aux besoins de structuration et faire face ainsi à  la complexité des systèmes logiciels d’aujourd’hui. De plus, une bonne architecture peut aider à exhiber les propriétés cruciales d’un système (fiabilité, portabilité, interopérabilité, etc.).

- Spécification Formelle et validation des protocoles dans les réseaux Mesh. Ce domaine a largement intéressé certains membres de cette équipe. Il s'agit d'appliquer leurs compétences en termes de modèles concurrents pour étudier et proposer des algorithmes valides et efficaces, gérant le routage dans les réseaux mesh.

- Spécification et vérification formelles des systèmes répartis. Plusieurs études sont menées pour découvrir les avantages et les limites de chacun des modèles largement répandus dans le domaine des spécifications de systèmes concurrents. Plusieurs modèles  algébriques et logiques ont été proposés, ils sont attrayant  d'un point de vue théorique et  de part leur simplicité.

- Modélisation formelle des applications Cloud/Fog/Edge. Dans le contexte des systèmes émergents (Cloud, Fog, Edge, CPS, etc.), nous nous retrouvons en face d’un décalage néfaste entre la théorie (modèles formels et technique de vérification) et la pratique (standards et application industrielle).  et dans le souci de combler cet écart, nous proposons des méthodes formelles — basées sur la logique de réécriture et le langage Maude et les bigraphes de Milner pour  étudier ces systèmes d'actualité.

- Architectures Logicielles et Systèmes de Systèmes. Exploitation de certaines techniques formelles pour la spécification et l’analyse des applications  architecturales dynamiques : Le développement de modèles et langages pour la  description et la spécification d’architectures est crucial pour  répondre aux besoins de structuration et faire face ainsi à  la complexité des systèmes logiciels d’aujourd’hui. De plus, une bonne architecture peut aider à exhiber les propriétés cruciales d’un système (fiabilité, portabilité, interopérabilité, etc.).

- Spécification Formelle et validation des protocoles dans les réseaux Mesh. Ce domaine a largement intéressé certains membres de cette équipe. Il s'agit d'appliquer leurs compétences en termes de modèles concurrents pour étudier et proposer des algorithmes valides et efficaces, gérant le routage dans les réseaux mesh.

Mots Clés: Méthodes formelles; Logiques comportementales; Architectures logicielles; Méta modélisation et méta transformation, Systèmes complexes.