English
CeV Contraintes et Vérification...

Projets en cours

COVERIF: Vers une combinaison de l’interprétation abstraite et de la programmation par contraintes pour la vérification de propriétés critiques pour des programmes embarqués avec des calculs en virgule flottante
type: ANR
partenaires: LIX, LIP6, LINA, I3S.
durée: 2015-2020
Le développement d’un ensemble de techniques et d’outils pour vérifier l’exactitude, la correction et la robustesse est un challenge important dans le domaine des logiciels embarqués critiques. L’objectif de COVERIF est de contribuer à relever ce défi en explorant de nouvelles méthodes basées sur une collaboration fine entre interprétation abstraite et programmation par contraintes. Plus précisément, il s’agit de repousser les limites inhérentes à ces deux techniques, d’améliorer la précision des estimations, de permettre une vérification plus complète des programmes utilisant des calculs sur les flottants, et de rendre ainsi plus robustes les décisions critiques liées à ces calculs.

Anciens projets

VACSIM: Validation de la commande des systèmes critiques par couplage simulation et méthodes d'analyse formelle
type: ANR
durée: 2011-2015
Le projet VACSIM vise à développer des contributions de nature à la fois méthodologique (définition de nouveaux modes d'utilisation des simulateurs, règles de couplage simulation/méthodes formelles) et formelle (adaptation, extension ou création de méthodes formelles) qui permettront la réalisation d'un démonstrateur, sur la base de l'outil ControlBuild, outil d'ingénierie numérique de la société Dassault Systèmes, illustrant, sur la base d'études de cas industriels, les bénéfices du couplage. Le but ultime du projet est de proposer un continuum de validation durant le cycle de vie de la commande des systèmes critiques basé sur des environnements d'ingénierie numérique.
PAJERO: Développement d’une plate forme logicielle horizontale dans la filière SaaS/Cloud/HPC/WorkForce Management mettant à la disposition des clients une solution optimisée et innovante pour l’association complexe de ressources humaines et de moyens
type: OSEO ISI
durée: 2011-2015
Pajero est un projet innovatif destiné à développer une plateforme d'optimisation basée sur le cloud. Proposé comme une application à la demande, il fournira un service à même de résoudre des problèmes complexes de gestion en temps réel. La rupture introduite par PAJERO est son positionnement horizontal c’est-à-dire une plateforme logicielle unique capable d’adresser les spécificités de différents segments de marché verticaux (santé, retail...) et d’interagir avec les applications type ERP/ERM existants. Pour atteindre cet objectif défini nous avons choisi une architecture de type SOA (Service Oriented Architecture – Architecture Orientée Services). Cette dernière correspond tout d’abord à l’état de l’art en termes d’organisation des systèmes d’information, elle permet de déployer et d’intégrer rapidement la solution au sein d’une infrastructure informatique existante. Elle facilite de plus la communication nécessaire entre la plateforme est les autres applications par l’utilisation de technologies standards d’échange de données (XML le plus souvent).
AEOLUS: Maîtriser la compexité du cloud
Le projet AEOLUS s'attaque aux problèmes scientifiques liés à l'antagonisme qui existe entre l'infrastructure comme service et la plateforme comme service au sein du cloud. La démarche s'appuie sur le développement de théories et d'outils pour automatiser le déploiement, la reconfiguration et la mise à jour de réseaux de machines hétérogènes et de tailles variables. Les résultats attendus de ces recherches devraient permettre de déployer, maintenir et administrer à coût maîtrisé l'architecture dynamique qui est au coeur des services offerts par le cloud.
MANCOOSI: Gestion de la complexité de l'infrastructure des systèmes à code source ouvert
type: FP7-ICT-2007-1
partenaires: Université Paris Diderot (France), Edge-IT (France), Université de L'Aquila (Italie), INESC-ID (Portugal), Caixa Magica (Portugal), Université de Nice-Sophia Antipolis (France), Université de Tel Aviv (Israël), ILOG (France), Université de Louvain (Belgique), Pixart (Argentine).
durée: 2008-2011
Mancoosi a pour objectif de développer les connaissances scientifiques et de concevoir les outils nécessaires à la gestion de la complexité des infrastructures basées sur un code source ouvert, infrastructures qui forment les briques de base du logiciel de demain. Mancoosi s'attaque aux problèmes difficiles qui surgissent lorsque l'on souhaite opérer une mise à jour efficace et sûre d'un ensemble de composants appartenant à une infrastructure logicielle complexe telle que celles que l'on peut trouver dans la distribution de logiciels à code ouvert. Ce sont parmi les systèmes logiciels les plus complexes, fait de plusieurs dizaines de milliers de composants qui évoluent dans le temps, sans système de conception centralisé, et qui fournissent un exemple réel de ce à quoi ressembleront les logiciels complexes et à évolution rapide de demain: les technologies développées par le projet Mancoosi devraient servir de base à la maintenance des systèmes du futur. Mancoosi fournira:
  • un modèle de l'infrastructure et des transformations qu'il sous-tend lorsqu'un composant est ajouté ou retiré;
  • des algorithmes avancés permettant de choisir l'évolution la plus efficace lors d'une mise à jour;
  • un forum capable d'attirer les meilleurs experts grâce à l'organisation d'une compétition internationale;
  • les outils qui incorporeront les avancés réalisées et l'état de l'art dans ce domaine.
CAVERN: Contraintes et abstractions pour la vérification de programmes
type: ANR Sécurité et Sûreté informatique
partenaires: IRISA, I3S, CEA-LIST, ILOG.
durée: 2008-2011
CAVERN se proposent d'étudier l'intégration d'abstractions dans les solveurs de contraintes actuellement en usage dans les divers outils des partenaires, afin de traiter plus efficacement les constructions des programmes impératifs telles que les boucles, les opérations sur la mémoire (références et structures dynamiques) et les calculs flottants. Le traitement efficace des ces constructions dans une approche de test à base de contraintes permettra de lever le verrou scientifique du passage à l'échelle de techniques de test automatique des programmes impératifs, ce qui permettra d'envisager leur utilisation dans le cadre de la certification indépendante des logiciels.
TESTEC: Test des Systèmes Temps réel Embarqués Critiques
type: ANR Technologies Logicielles
durée: 2008-2011
Le besoin de test fonctionnel explique l'émergence depuis quelques années d'environnements de génération automatique de tests à partir des modèles représentatifs des spécifications. La problématique principale à laquelle sont confrontés tous ces outils est la maitrise de l'explosion combinatoire tout en garantissant un taux de couverture requis, qui n'est calculé que sur le modèle de spécification. Dans ce cadre, le projet TESTEC cherche à lever deux principaux verrous technologiques:
  • Le premier verrou technologique que cherche à lever le projet TESTEC est l'optimisation des techniques utilisées pour les projets de grande taille, notamment par une gestion explicite du temps dans les modèles et par la gestion des variables continues et discrètes d'une application hybride.
  • Le second verrou technologique que cherche à lever le projet TESTEC est la réduction de la taille des tests déduits des modèles de spécification en utilisant les résultats de vérifications formelles conduites sur des réalisations ou des modèles d'implantation. L'objectif du projet est de proposer un démonstrateur de génération et d'exécution automatique de tests basé sur des environnements existants et intégrant les résultats scientifiques du projet.
DANOCOPS: Détection Automatique de Non Conformité entre un Programme et sa Spécification
type: RNTL
durée: 2004-2007
Pour les systèmes industriels critiques, la phase de validation peut représenter 50% du coût du système. Cette proportion ne cesse de s'accroître à cause de la complexité grandissante des systèmes et de la tendance actuelle à la sous-traitance d'une partie du développement du logiciel. Dans cette optique, il devient impératif d'offrir au donneur d'ordre concepteur du système des moyens puissants pour définir le logiciel attendu et vérifier le logiciel obtenu. Aujourd'hui, dans l'industrie, la vérification du logiciel repose sur le test et les revues de codes. Beaucoup de recherches se font sur des méthodes plus formelles via des programmes développés par raffinement prouvés corrects ou bien par génération à partir de modèles de plus haut niveau eux-mêmes vérifiés par model-checking ou par test. Pour vérifier le logiciel développé manuellement, à coté des méthodes de test, une voie complémentaire peut consister à rechercher automatiquement des erreurs dans le programme. Des outils prenant cette optique existent d'ailleurs déjà, mais ils se cantonnent à la recherche d'erreur d'exécution (débordement, overflow, ?) qui peuvent provoquer l'interruption du programme. Nous proposons dans ce projet Danocops de résoudre le problème plus général qui est de détecter des non-conformités aux spécifications. Une détection automatique des non-conformités aux spécifications pourrait compléter efficacement les processus de vérification actuels en ce qu'elle peut, avant de lancer une phase de test ou de revue de code, valider ou invalider certaines portions du logiciel, et permettre de centrer l'attention sur les pièces de code litigieuses, celles pour lesquelles la recherche de non-conformité n'aurait pas pu conclure. Nous proposons une technique innovante pour détecter des défauts de conformité aux spécifications. Cette technique est basée sur une transformation du programme et des spécifications en systèmes de contraintes. Ce type de transformation est déjà utilisé avec succès dans différents outils (INKA, BZ-TestingTools) pour la génération automatique de cas de tests développés par les partenaires. L'objectif du projet DANOCOPS est d'exploiter les potentialités de cette technique pour la recherche de défauts de conformité, de développer un outil capable de l'appliquer sur des programmes écrits en C/C++/JAVA et des spécifications écrites en UML/OCL et d'explorer l'utilisation de cette technique dans le cas de spécifications décrites en B et Lustre. Le projet DANOCOPS est un projet pré-compétitif et sa durée prévue est de 30 mois.
V3F: Validation et Vérification en présence de calculs en Virgule Flottante
type: ACI Sécurité Informatique
partenaires: CEA LIST, LIFC, LIG, I3S.
durée: 2003-2006
L'utilisation des nombres à virgule flottante pour la représentation des nombres réels est une source importante de défauts et de pannes potentielles pour les systèmes logiciels critiques. La modélisation de ces systèmes, associée à des techniques de vérification de modèles, de preuve et de génération de tests, constitue un des principaux vecteurs d'une meilleure maîtrise du processus de développement, et d'une amélioration de la fiabilité des systèmes intégrant du logiciel. Les techniques, notations et approches de modélisation aujourd'hui développées, font, pour l'essentiel, l'impasse sur la représentation flottante des données. En machine, les flottants constituent pourtant la principale représentation des données de type réel. La difficulté pour traiter correctement cette représentation des réels provient en grande partie des propriétés mathématiques extrêmement pauvres des flottants et de leurs dépendances vis à vis du matériel (même lorsque la norme IEEE 754 est respectée).
INKA: Génération automatique déterministe de données de test selon des critères de couverture structurelle
type: RNTL
partenaires: Axlog, Thomson-CSF Detexis, LIFC, LSR, I3S.
durée: 2000-2003
Le test structurel est coûteux et requiert des compétences spécifiques. En effet il nécessite une analyse fine de la structure du logiciel, et un raisonnement inversé pour déterminer les données d'entrées requises pour exécuter un fragment du logiciel. Ceci a pour conséquence que la plupart des logiciels mis sur le marché comporte de nombreuses séquences de code n'ayant jamais été exécutées. L'outil INKA génère automatiquement et de manière déterministe les données d'entrées à partir de la caractérisation des fragments à atteindre (critère de couverture). INKA est basé sur une technique originale (issue de nos recherches menées depuis plusieurs années) consistant à convertir le programme à tester et les fragments à atteindre en des systèmes de contraintes en utilisant la programmation logique à contraintes, et grâce aux moyens de résolution fournis par celle-ci, de calculer les solutions de ces systèmes qui constitueront un jeu de données d'entrées satisfaisant.