AeLoS - Architectures et Logiciels Sûrs

Comment construire correctement des composants logciels à partir de leurs exigences, comment garantir le fonctionnement correct d'un composant logiciel en étudiant son modèle formel, comment maitriser la construction et l'évolution du logiciel à travers son architecture ?

Responsable : Christian Attiogbé
Pôle(s) de recherche :
SLS

Notre principal objet d'étude est le logiciel. Nous cherchons des méthodes pour garantir la correction des logiciels. Pour cela nous étudions leurs modèles sémantiques, leur construction correcte à travers des techniques de raffinement, leur vérification à travers des techniques de preuve ou de d'exploration d'etats (model-checking), leurs architectures et évolutions dans le temps.
Les systèmes complexes qui font interagir des composants physiques ou logiciels variés, d'importantes données, des contraintes de temps, des exigences de robustesse et de qualité sont difficiles à modéliser et à développer.



Nous attaquons ces difficultés à travers différentes thématiques qui gravitent autour des modèles. L'étude des modèles est alors déclinée selon différentes facettes dans le but de couvrir les différentes couches d'abstractions qui constituent un système (logiciel) :

  • Les services et composants qui interagissent dans le système
  • L'analyse des systèmes hétérogènes
  • L'architecture et l'évolution du système
  • Les modèles sémantiques variés (par exemple, des modèles logiques, à états, à composants, à services, à événements discrets, probabilistes, temporisés) et les techniques de vérification associées

 

Thématiques
Composants logiciels corrects

le défi de la construction par composition d'éléments de base est affronté ici. L'objectif est de proposer des concepts simples et des techniques d'assemblage de composants et services tout en garantissant la correction, à travers des modèles et méthodes formels, des techniques de vérification (preuve, exploration d'états, test). Nous explorons ici en particulier des techniques de test des transformations des modèles.


Multiformalisme et analyse multifacette des systèmes

l'hétérogénéité dans la composition est une des caractéristiques des systèmes complexes ; nous nous attaquons ici au défi de l'interopérabilité et de l'analyse globale du logiciel


Architecture logicielle

le défi de la construction par composition d'éléments de base est affronté ici avec une approche descendante. L'objectif est de décrire et étudier l'architecture globale du logiciel et de proche en proche l'études des services composés qui interagissent dans le logiciel. Le logiciel évoluant dans le temps (en fonction des exigences de son environnement), la prise en compte de l'évolution à différents stades représente un de nos champs d'études.


Modèles sémantiques de la concurrence et outils d’analyse associés

la maitrise de la complexité des logiciels passe par l'élaboration des modèles formels appropriés et leur analyse afin de s'assurer des propriétés attendues et de l'absence des propriétés non désirées. Nous étudions ici, les modèles basés sur les automates et notamment les modèles temporisés et les modèles probabilistes.


Par rapport à ces thématiques, les compétences des membres de l'équipe nous permettent d'explorer en particulier :

  • les modèles pour les services, composants et l'architecture globale ;
  • les méthodes de vérification par la preuve, l'exploration d'états et le test.
  • les systèmes réactifs, concurrents, embarqués et les systèmes d'information.