L’informatique fondamentale est sous-jacente à tous les domaines de l’ingénierie des logiciels et des protocoles en procurant les outils nécessaires au développement rigoureux des sciences et technologies de l’information et de la communication. L’informatique fondamentale traite de l’abstraction, la modélisation et tous les aspects liés à la structure, le traitement, la transmission et la reproduction de l’information dans son contexte. Les domaines principaux de l’informatique fondamentale couvrent de nombreux aspects scientifiques et évoluent de paire avec les domaines d’applications visés. Nous pouvons citer les aspects fondamentaux suivants: la théorie des automates, la théorie des langages formels (i.e. hiérarchie de Chomsky), les méthodes formelles, les techniques formelles de vérification, de test et de monitorage, la calculabilité et la théorie de la complexité. Elle couvre aussi tous les aspects liés à la mise en pratique de ces méthodes sous la forme d’outils logiciels pour la vérification, le test et le monitorage aussi bien que des plateformes de validation intégrant tous ces techniques. Ces dernières étant bien adaptées au traitement des systèmes de grande taille.  Les domaines d’application de l’informatique fondamentale sont nombreux et servent notamment de base à la définition, la vérification et la mise en oeuvre de logiciel mais aussi à la construction de compilateurs de langages de programmation (classe des sciences du compilateur) et la formalisation mathématique de la plupart des systèmes communicants. Parmi les méthodes constructives de l’informatique fondamentale, nous devons insister sur la conception de systèmes formels à partir des graphes, des automates, des logiques, des machines d’états finis et des diagrammes, et la mise en place des syntaxes et sémantiques pour ces systèmes. Les systèmes et leurs aspects fonctionnels et non-fonctionnels décrits, entre autres par des logiques mathématiques, par des graphes ou par des automates permettent leur vérification (étayée par des preuves ou par le « model checking ») et leur test ou leur monitorage. La logique mathématique est utilisée dans de nombreux domaines d’application, ce qui a conduit à de nombreuses extensions (e.g. propositionnelle, combinatoire, Boole, modal, etc.). Dans le domaine de la spécification formelle, différentes logiques telles que la logique des prédicats, la logique modale temporelle sont utilisées pour décrire le comportement prévu des systèmes logiciels et matériels. Ils peuvent ensuite être vérifiés en utilisant des techniques de « model-checking » ou de preuve. La vérification formelle a pour objectif d’évaluer, de manière précise et sans ambiguité, la correction d’un programme, la sécurité d’un système critique ou tout simplement l’adéquation du fonctionnement d’un système vis-à-vis d’un cahier des charges. Les techniques de vérification formelle les plus connues sont : le « model checking », le test et la preuve. Le « model checking » permet de vérifier une propriété donnée en explorant les différents états d’un modèle fini du système. Le test formel vérifie l’implantation du système avec un ensemble de scénarios choisis de manière méthodique ou même aléatoire. La vérification par la preuve consiste à raisonner sur le système en établissant une série d’axiomes et de théorèmes intermédiaires à partir desquels il devient possible de déduire la propriété à prouver.  Les outils fournis par l’informatique fondamentale permettent de tester formellement les propriétés dites fonctionnelles et non-fonctionnelles (i.e. la sécurité) des systèmes modélisés. Les méthodes de descriptions susmentionnées (telles que les logiques, les automates ou les langages formels) permettent de modéliser statiquement ou dynamiquement des systèmes complexes, qu’ils soient de type ‘boite blanche’ ou ‘boite noire’.  Les modèles formels permettent en outre de définir le système sous test mais permettent également définir des algorithmes pour la génération de tests. Toutes ces descriptions formelles servent de base pour la génération de différent types de test (i.e. unitaire, intégration, non-régression, interopérabilité, stress, performance, etc.) pour lesquels des algorithmes dédiés sont étudiés et mis en oeuvre. Ces algorithmes font notamment l’objet d’étude de calculabilité et de complexité, domaines cruciaux de l’informatique fondamentale. Ils permettent d’ouvrir de nouvelles perspectives pour la recherche sur les approches de test formelles actif et de monitorage. Ceci en générant des suites de tests abstraits instanciés par unification dans un univers mathématique rigoureusement défini (test actif) ou en établissant les liens d’isomorphie entre une trace d’exécution avec une propriété fonctionnelle (voire non fonctionnelle) formellement définie (techniques de monitorage). Les algorithmes sous-jacents (« backward/forward checking », « random walk », etc.) permettent aujourd’hui de tester des systèmes dont la taille et la complexité sont grandissantes.  Le développement des outils logiciels pour la vérification et le test ainsi que la mise en place des plateformes de validation sont aussi une partie essentielle de ce domaine.  Ces thématiques incluent un certain nombre de domaines bien représentés au sein de l’Institut Mines-Télécom: modèles formels des systèmes communicants, méthodes de vérification basés sur la preuve et le « model checking », méthodes de vérification de la compilation, techniques de vérification pour les systèmes embarqués, méthodes de test et de monitorage basées sur des approches formelles.

Equipes impliquées : LabSoc de Télécom ParisTech; LOR et INF de Télécom SudParis.