CAVERN ANR-07-SESUR-003 http://www-anr-ci.cea.fr Sécurité et Sûreté Informatique			ACCUEIL
Accueil Partenaires Outils Publications Réunions Modèle Rapport Délivrables Poster Présentation Finale	En augmentant la confiance que nous portons dans la fiabilité et la sûreté des logiciels, les techniques de test prennent une place essentielle lors de la certification des systèmes complexes. En particulier, les normes DO-178 pour l’avionique civile et militaire, Critères Communs pour les cartes à puces ou CEI 61508 dans le cadre général des transports et de l’énergie présentent de nombreuses exigences en matière de test logiciel. Pourtant, le test reste un des points les plus coûteux dans le processus de développement des logiciels et un des enjeux majeurs dans ce domaine concerne son automatisation. Bien que des progrès très significatifs aient été accomplis ces dernières années, le point d’achoppement des techniques de test automatique actuelles concerne leur passage à l’échelle. D’une part, il est bien connu que certaines constructions des langages sont difficiles à traiter de manière automatique dans leur plus grande généralité (boucles, références et structures dynamiques, etc.) et d’autre part, la construction d’outils capables de tester des programmes comprenant des constructions non-linéaires (disjonctions, expressions arithmétiques non-linéaires, etc.) ou manipulant des données à la fois entières, réelles et structurées réclame une expertise dans des domaines variés. Le projet CAVERN (Constraints and Abstractions for program VERificatioN)  vise à augmenter le potentiel de la Programmation par Contraintes pour la vérification automatique de programmes impératifs. L’idée classique sur laquelle se fonde cette approche consiste à construire, à partir de la description d’une situation que l’on cherche à atteindre, un système de contraintes représentant l’objectif. Cet objectif peut être positif lorsqu’il représente un objectif de test, la solution du système de contraintes correspond alors à un scénario représentatif de l’objectif, c’est ce principe qui est utilisé dans les outils de génération de tests avec des objectifs de couverture structurelle ou fonctionnelle. Cet objectif peut à l’inverse être négatif dans le but d’identifier des menaces particulières, dans ce cas on confronte la négation d’une propriété qui doit être vraie au système de contraintes extrait du programme à vérifier. Dans cette seconde utilisation, l’existence d’une solution du système de contraintes résultant correspond à l’existence d’un contre-exemple qui peut-être soumis au programme pour mettre en évidence un ou plusieurs défauts. Parfois, l’insatisfiabilité du système de contraintes, lorsqu’elle peut-être établie, démontre que la propriété est vérifiée par le programme. Ce procédé repose actuellement sur l’utilisation de résolveurs de contraintes « génériques »  développés pour d’autres applications (optimisation combinatoire, aide à la décision, etc.). L’originalité du projet CAVERN réside dans l’exploitation des techniques d’abstraction pour construire des résolveurs de contraintes dédiés au test automatique des programmes. En effet, en analyse statique, ces dernières années ont vu le développement de techniques puissantes de calcul sur des domaines abstraits variés (polyèdres, congruences, octogones, etc.) et ce projet se propose d’explorer l’utilisation de certains résultats obtenus dans ce domaine pour développer des résolveurs ayant de fortes capacités de déduction en présence de constructions typiques des programmes impératifs. La principale retombée scientifique attendue de ce projet est une compréhension intime de l’apport des techniques d’abstraction pour le test automatique à base de contraintes des programmes impératifs. Le projet regroupe quatre partenaires fortement impliqués dans le développement de résolveurs de contraintes et leurs applications à la vérification des programmes : l’équipe-projet Lande de l’IRISA à Rennes (LANDE) -- Coordinateur l’équipe « Contraintes et Preuve » du laboratoire I3S de l’Université de Nice – Sophia Antipolis (CeP) le laboratoire LIST du CEA à Saclay (CEA) la Société ILOG à Gentilly (ILOG) De plus, le projet accueille un partenaire associé étranger : Andy King de l’Université du Kent Concrètement, les partenaires du projet CAVERN se proposent d’étudier l’intégration d’abstractions dans les résolveurs de contraintes actuellement en usage dans leurs outils propres, 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.
Date de dernière mise à jour : 31/01/2012