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’états (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

• Composants logiciel corrects
• Multiformalisme et analyse multifacette des systèmes
• Architecture logicielle
• Modèles probabilistes, sémantiques de la concurrence, outils de vérification associés.

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.