Équipe « Spécification et vérification de systèmes »

Membres - Publications

Joelle Cohen, Catalin Dima, Lynda Mokdad, Nihal Pekergin, Minh-Anh Tran

La complexité croissante des systèmes rend l'analyse, l'évaluation des performances et la garantie de bon fonctionnement de plus en plus nécessaire. De plus, la prolifération de nouvelles applications et services, de nouveaux supports de transmissions et nouveaux équipements met la qualité de service (QoS), la sécurité, la vérification de propriétés temporisées, probabilistes, et quantitatives au coeur du développement de ces systèmes. La modélisation, l'évaluation des performances et la vérification deviennent des tâches essentielles, pour lesquelles il convient de développer de nouvelles méthodes afin de les adapter aux problèmes de complexité actuelle.

Dans cette thématique, les pistes suivies au LACL sont :

• la modélisation de systèmes complexes par réseaux de files d'attente, automates temporisés et/ou probabilistes,
• l'évaluation de performances, de dimensionnement et de qualité de service,
• la vérification de propriétés temporisées, probabilistes, quantitatives (nous avons notamment développé un prototype d'outil de model-checking stochastique),
• la comparaison stochastique, les solutions à forme-produit, le calcul d'entropie, la simulation à événements discrets pour l'analyse des modèles de sûreté de fonctionnement,
• la modélisation, la spécification et la vérification des propriétés de sécurité dans des systèmes multi-agents.

Catalin Dima, Frédéric Gervais, Christophe Gnaho, Régine Laleau, Farida Semmak

Dans cette thématique, les travaux de recherche portent sur la définition et l'utilisation de techniques et de notations formelles qui permettent de couvrir toutes les phases de développement de logiciels, depuis l'analyse des besoins jusqu'à l'implémentation. Les systèmes visés sont principalement les SI, en particulier les applications BD et les services web. L'objectif principal de l'équipe est la spécification et la vérification de propriétés de sûreté et de sécurité de ces systèmes.

Plus précisément, les axes de recherche sont actuellement développés :

• Combinaisons de paradigmes complémentaires :
  • diagrammes semi-formels, principalement graphiques (UML), et langages formels,
  • algèbres de processus et langages basés sur les états.
• Processus de dérivation formelle entre les différentes phases de développement : raffinement, synthèse automatique, ingénierie dirigée par les modèles.
• Ingénierie des besoins : étude de l'impact des exigences non fonctionnelles sur les besoins fonctionnels, variabilité, traçabilité.
• Prise en compte de la sécurité dans les processus de modélisation : spécification formelle, vérification formelle, implémentation de politiques de sécurité.

En résumé, cette thématique vise à rechercher des techniques qui favorisent une utilisation pragmatique des méthodes formelles dans le développement de logiciels sûrs.

Fabrice Mourlin, Elisabeth Pelz

Les membres de cette thématique ont proposé et étudié divers formalismes basés sur des algèbres de réseaux de Petri colorés (M-nets, S-nets, ABCD,…) permettant :

• une modélisation structurée aisée, par une compositionalité totale et des syntaxes simples
• des méthodes de vérification spécifiques assurant des bons compromis entre expressivité de modèles et efficacité, voire faisabilité de la vérification
• un prototypage rapide utilisant notre outil SNAKES

Ils ont validé ces propositions dans des domaines d'applications variés : protocoles de sécurité, systèmes temps-réel, réseaux d'interconnexions multi-stage, processus biologiques, protocoles pair-à-pair, …

Un deuxième thème de recherche porte sur la conception et la réalisation de mobilité d'agents en tant que principe de base d'une architecture logicielle. Cela va de la définition d'architecture par l'emploi d'algèbres de processus à la preuve de propriétés par l'usage de logiques temporelles. Des aspects novateurs étudiés concernent l'organisation d'agents au sein d'un espace de travail et la négociation d'agents lors de la migration d'un nœud à un autre du réseau. Nous appliquons nos résultats dans le cadre du calcul numérique et l'adaptation de codes existants au réseau d'exécution.

Frédéric Gava, Gaétan Hains, Sovanna Tan

D'un point de vue général, nous étudions aussi la programmation data-parallèle du point de vue des langages, du lien sémantique-performance, de son adaptation aux nouvelles plateformes matérielles (GPU, multi-cœurs, grappes dans le Cloud etc.) et de ses applications. Nous nous intéressons principalement à 3 thématiques.

Premièrement, nous travaillons au développement d'un langage de programmation de haut-niveau orienté fonctionnelle appelé BSML qui est conçu pour un modèle de parallélisme appelé BSP qui permet notamment la prédiction des performances des algorithmes sur une architecture donnée et évite les interblocages et le non-déterminisme inhérent à la concurrence. Nous nous intéressons à sa sémantique, la vérification de ses programmes, son utilisation pour l'implantation de bibliothèques ou de squelettes algorithmiques et son adaptation aux architecture parallèles modernes et hybrides (à plusieurs niveau de parallélisme).

Deuxièmement, nous travaillons sur la vérification de programme BSP en utilisant la logique de Hoare (adaptation pour BSP de l'outils WHY) et la vérification de formules CTL* pour les protocoles de sécurité en utilisant un algorithme BSP qu'on cherche aussi à vérifier en utilisant les travaux sus-mentionnés.

Dernièrement et plus récemment, nous travaillons sur une adaptation de BSML à des architectures hiérarchisées et hétérogènes mélangeant multi-cœurs, GPU et autre processeurs spécialisés.

Du côté des applications nous étudions et expérimentons depuis 2 ans sur l'optimisation et la prévision de performances pour les requêtes sur documents semi-structurés, en mode flux et depuis peu aussi en mode parallèle BSML. Enfin nous avons amorcé une étude de l'application des modèles de performance à la prévisibilité dans la supervision des centres de calcul en environnement virtualisé. Le thème des masses de données est abordé par des projets autour du traitement en flux et en parallèle des requêtes sur documents XML.