Projets
- 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.
- AEOLUS, Aeolus is an ANR funded research project whose main objective is to tackle the scientific problems that need
to be solved in order to bridge the gap between Infrastructure as a Service and Platform as a Service solutions, by developing theory and tools to automate deployment, recon figuration, and upgrades of variable sized, non-homogeneous machine pools.
We expect that the results of this research work will allow to efficiently deploy, maintain, and administer, in a cost-effective way, the dynamically changing distributed architectures which are at the heart of Cloud services.
- VACSIM, Validation de la commande des systèmes critiques par couplage simulation et méthodes d'analyse formelle.
Anciens projets
- MANCOOSI, Gestion de la complexité de
l'infrastructure des systèmes à code source ouvert, (programme européen
FP7-ICT-2007-1).
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, Constraintes et abstractions
pour la vérification de programmes (ANR Sécurité et Sûreté informatique).
- Membres du projet: IRISA, I3S, CEA-LIST, ILOG.
- Description: CAVERN se proposent
d'étudier l'intégration d'abstractions dans les ré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 (ANR Technologies
Logicielles).
- Membres du projet: EDF
Recherche et Développement, TNI
Software, I3S, IRISA, LABRI,
LURPA.
- Description: 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.
- ACI V3F, Validation et
vérification en présence de calculs à virgule flottante.
- Membres du projet: LIFC, I3S, IRISA,
LIST.
- Description: 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 leur dépendance vis à vis du matériel (même
lorsque la norme IEEE 754 est respectée).
- RNTL Danocops,
Détection automatique de non-conformités d'un programme vis à vis de sa
spécification.
- Membres du projet: Thales systèmes aéroportés, Axlog, I3S,
LIFC, LSR.
- Description: 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.