29
LSR IMAG 1 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test d’intégration Karim-Cyril Griche LSR/IMAG

LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

Embed Size (px)

Citation preview

Page 1: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

11

Test Structurel de programmes C à l'aide de la programmation logique

avec contraintes (PLC) : test d’intégration

Karim-Cyril Griche

LSR/IMAG

Page 2: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

22

Plan de la présentation

• Introduction

• Choix et objectifs

• Orientation prise : modélisation de fonctions– Comment modéliser?– Analyse des fonctions appelantes

• Perspectives

Page 3: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

33

Introduction

• Projet RNTL Inka en partenariat avec Thalès Systèmes Aéroportés, LIFC, I3S, Axlog

• Outil Inka : – Issu de la thèse de Arnaud Gotlieb– Test structurel unitaire de programme C en

utilisant la PLC

• Extension de Inka au test d’intégration

• Extension aux flottants (I3S)

• Extension aux pointeurs (LIFC)

Page 4: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

44

Outil Inka

• Fonctionnement :– Traduit un programme en un ensemble de

clauses prolog (Sicstus)– Réduit cet ensemble de clauses– Génère des tests visant la couverture

Programme C ÉquivalentProlog

Ensembleréduit Cas de

test

Inka

Page 5: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

55

Test unitaire

• Test unitaire : on remplace les appels de fonctions par des bouchons

int f(int x) { ... If (g(y)<0) ... ...}

But : couverture structurelle de f()

- On doit passer dans la branche THENdu if...then...else

Condition : résultat de g() négatif- On crée un bouchon bg() qui rend une valeurnégative quelle que soit la valeur de y

Page 6: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

66

Extension au test d’intégration

• Intégration : on remplace les bouchons par les véritables fonctions

Problème : Les véritables fonctions ne se comportent pas comme les bouchons

int f(int x) { ... If (g(y)<0) ... ...}

Int g(int x) { return x*x;}

L’intégration de g() pourla couverture structurelle de f() empêche le passagedans la branche THENdu if...then...else

-Détecter les nouveaux chemins impossibles au plus tôt-Mauvais bouchons erreurs d’exécution potentielles ou

masquage d’erreurs présentes

Page 7: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

77

Étude bibliographique

• Rares publications

• Essentiellement des méthodologies d’intégration portant sur l’ordre d’intégration des fonctions dans le logiciel

Page 8: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

88

Cadre de l’intégration dans Inka

• Le test d’intégration avec Inka s’effectue sur un ensemble de fonctions complet formant un sous-système d’un logiciel

• Pas de notion d’ordre d’intégration

• Objectifs : couverture structurelle

f

g h

g1 g2 h1 h2

...SousSystème

Logicielcomplet

main

Page 9: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

99

Problématique

• Ce sous-système est représenté sous forme de contraintes– Inka traduit une fonction C en un ensemble de

contraintes

– Un appel de fonction est traduit en un appel à la clause représentant la fonction

Explosion du nombre de contraintes à traiter si le nombre d’appel de fonctions est trop grand

Page 10: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

1010

Objectifs

• Trouver un moyen de « passer à l’échelle »– Modéliser les fonctions appelées de manière

réduite

• Définir des modèles réalistes :– Moins complexes que les fonctions originales– Équivalents vis à vis des besoins du test

(génération de données)

Page 11: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

1111

Orientation : Spécialisation de fonctions

• Modèles de fonctions optimisés : fonctions originales spécialisées pour leur utilisation dans le test

• Techniques étudiées :– Interprétation abstraite

• Calcul d’invariants

– Slicing intra-procédural• Découpe d’une fonction

– Evaluation partielle• Spécialisation de fonctions

• Approches heuristiques

Page 12: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

1212

Construction des modèles

• 2 critères : Un modèle doit– être plus simple que les fonctions originales– Disposer d’un modèle exact de chacune des

fonctions

• 2ème critère nous a amené à une architecture où les approximations se superposent

M1 M2 M complet

Ordre d’essai des modèles

Page 13: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

1313

Plan de la présentation

• Introduction

• Choix et objectifs

• Orientation prise : modélisation de fonctions– Comment modéliser?– Analyse des fonctions appelantes

• Perspectives

Page 14: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

1414

Heuristiques

• Gestion des appels de fonctions

• Étude de simplification de fonctions basée sur l’élimination de chemins compliqués

Page 15: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

1515

Gestion des appels de fonctions

• Un appel de fonction : clause représentant la fonction– + : les appels de fonctions sont traités

naturellement– - : Mise à plat du système sous test lors de

l’intégration

• Idée : Opérateur de gestion des appels de fonctions– Limitation de la profondeur de mise à plat– Développé et en cours d’évaluation/calibrage

Page 16: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

1616

Gestion des appels de fonctions

f

g

h

k

i

j

Dg(x)

Di(x)

Page 17: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

1717

Heuristique : poids sur les branches

• Idée : éliminer les branches définies comme complexes

• Définir un poids pour chaque opération/fonction et pondérer les branches/chemins d’une fonction

• Introduire un mécanisme de préférence des branches à faible poids – Quand c’est possible, utiliser la branche avec le

poids le plus faible

Page 18: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

1818

Poids sur les branches

Int g(int x) … if Cond … else y=h(w);…

Poids faible

Poids très fort

f

g

h

Page 19: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

1919

Plan de la présentation

• Introduction

• Choix et objectifs

• Orientation prise : modélisation de fonctions– Comment modéliser?– Analyse des fonctions appelantes

• Perspectives

Page 20: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

2020

Analyse des fonctions appelantes

• 3 possibilités : 1. Un modèle par fonction.

2. Un modèle par fonction et par fonction appelante.

3. Un modèle par fonction appelée et par appel dans la fonction appelante.

Page 21: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

2121

Un modèle par fonction

• On remplace tous les appels du sous-système par un appel au modèle– + : rapidité de construction– - : modèles moins optimisés

Page 22: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

2222

Un modèle par fonction et par fonction appelante

• On remplace tous les appels à g() dans f() par des appels à mg()– + : existe un contexte du modèle

– - : modèle général

f(x) :...If (z>5) ... y = g(z)...

w = g(x*x)...

g(x) :if (x>0) return xelse return -x

mg(x) : return x

Contexteélimine les cheminsinutiles

f(x) :...If (z>5) ... y = mg(z)...

w = mg(x*x)...

Page 23: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

2323

Un modèle par fonction appelée et par appel dans la fonction appelante

• Chaque appel de fonction est remplacé par un appel au modèle de la fonction pour cet appel.– + : modèles plus optimisés, contexte précis– - : nombre de modèles

Page 24: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

2424

Un modèle par fonction appelée et par appel dans la fonction appelante

f(x) :...If (z>5) y = g(z)else y = 2...w = g(x)...

g(x) :if (x>0) return xelse return -x

mg1(x) : return x

mg2(x) : g(x)

C1

C2

f(x) :...If (z>5) y = mg1(z)else y = 2...w = mg2(x)...

Page 25: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

2525

Contexte d’utilisation

• Besoin d’information : Contexte d’utilisation – Contexte d’un appel de fonction donné par la fonction

appelante

• Contexte d’utilisation défini en 2 parties :– Contexte d’appel : Information sur les domaines des

variables d’entrée de la fonction

– Objectifs de génération : Information sur l’utilisation faite des résultats de l’appel à la fonction et notamment des branchements qui en dépendent

Page 26: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

2626

Un contexte d’appel

Int f(int x) { ... If (x>0) y=g(x);...}

Contexte =g() appelé uniquementavec des valeurs positives

• Un contexte d’appel est formé par l’ensemble des chemins depuis le début de f() jusqu ’à l’appel à g()

• Il peut être représenté par un ensemble de contraintes

Page 27: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

2727

Un objectif de génération

Int f(int x) { ... If (g(y)>=2) ... else ...}

Obj. Gen. = Notre modèle doit pouvoirproduire des sorties <2 et d’autres >=2 si c’est possible

Page 28: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

2828

Perspectives

• Le contexte d’appel : – Point de départ au calcul d’un invariant sur

domaines de sortie– Utiliser une technique inspirée de l’évaluation

partielle pour éliminer certaines parties d’une fonction

• Les objectifs de génération : – Envisager le « slice » d’une fonction connaissant

l’utilisation qui doit en être faite

Page 29: LSR IMAG 1 Test Structurel de programmes C à l'aide de la programmation logique avec contraintes (PLC) : test dintégration Karim-Cyril Griche LSR/IMAG

LSRIMAG

2929

Travaux en cours et perspectives

• Premières expérimentations concluantes

• Définition des poids des heuristiques d’élimination de chemins compliqués et évaluation

• Prototype implémentant les différentes méthodes pour évaluer leurs résultats