|
Présentation détaillée du Projet |
|
|
Page 3 sur 4
Une suite d’outils de test et d’analyse de modèle. Intégrer les activités de validation dans un processus de type IDM.
Le sous-projet MoDriVal est centré sur la vérification de systèmes complexes à différents stades de leur développement depuis leur spécification et leur modélisation jusqu’à la recette du produit final. La notion de système complexe est restreinte ici à ceux dont la complexité résulte de la présence simultanée de composantes logicielles et matérielles, que ces matériels soient des processeurs existants, des System on Chip (SoC) ou des Network on Chip (NoC).
Plusieurs thèmes sont abordés dans le sous-projet:
- La testabilité, à travers diverses techniques de génération automatique de tests, notamment par des méthodes statistiques ou à partir d’exigences formalisées.
- La vérification automatique de propriétés de comportement de modèles de logiciels ou de programmes.
- La simulation d’architectures matérielles supportant l’exécution des logiciels, à des fins de prévision de performance ou de consommation d’énergie.
La première famille de techniques investiguées concerne spécifiquement la synthèse de tests c'est-à-dire les moyens de calculer les données d’entrée du test en fonction de la propriété à mettre en évidence. Plusieurs techniques sont étudiées, comme la génération de tests à partir de modèles formels d’exigences ou celle à partir d’une distribution de taux de couverture de la structure du logiciel à tester. La seconde famille de techniques abordées dans MoDriVal porte le nom d’analyse statique par interprétation abstraite. Au lieu d’exécuter le programme à tester pour un jeu de valeurs numériques d’entrée, on raisonne mathématiquement sur l’exécution du programme pour des valeurs symboliques, c'est-à-dire quelconques, des entrées, en ne prenant en compte dans le raisonnement que ce qui est pertinent pour la classe de propriétés à établir. Deux classes de propriétés sont considérées : une majoration aussi précise que possible des erreurs d’arrondi des calculs numériques, et la vérification d’absence de débordement mémoire pendant l’exécution du programme. Enfin la troisième famille de techniques de validation étudiée dans MoDriVal concerne l’exécution d’un logiciel sur du matériel simulé par logiciel afin de prédire avec précision le temps de cette exécution et l’énergie qu’elle consommera. Ces prédictions sont essentielles pour l’insertion de logiciel dans de petits objets tels que les téléphones portable ou les cartes à puce, dans des phases de développement où seuls des modèles logiciels des processeurs cibles sont disponibles. |
