est destinée au dépôt

Résumé

Le Fonds Français pour l'Environnement Mondial [FFEM] a financé deux phases de projets de développement visant à appuyer la mise en place de la politique forestière malgache définie par la loi n°97 017. Les acquis et les résultats obtenus dans le cadre de ces deux phases [FFEM 2002[START_REF] Diane | Une vue de près du droit de l'environnement Malgache[END_REF]et COGESFOR 2009-2013] s'organisent principalement autour de l'appui et de l'accompagnement des acteurs dans le processus de mise en place des contrats de TGRNR GELOSE visant la conservation par la valorisation.

Cependant, le massif forestier d'Ambohilero concernée par ces projets fait aujourd'hui l'objet de la mise en place d'une Réserve de ressources naturelle (catégorie VI de l'UICN concernant les Nouvelles aires protégées de Madagascar -Le quota de prélèvement est fixé à partir des résultats d'inventaires de la zone et du diagnostic socio économique. Il fixe les objectifs de production et fournira des données sur les volumes et qualités exploitables annuellement ainsi que sur les prévisions des recettes et dépenses attendues, -Les plans d'aménagement prévoient une rotation de coupe de 60 ans -La coupe concerne uniquement les bois supérieurs au diamètre minimal d'exploitabilité

[DME] Il s'agit de coupes de proche en proche des arbres qui appartiennent à la liste des essences cibles et atteignant 50 cm à 1,30 m. de hauteur situés dans la zone de production.

Les conditions détaillées de la valorisation économique des filières des produits forestiers dans le cadre d'une gestion forestière communautaire GELOSE.

L'exploitation raisonnée des VOI concerne les bois de deuxième, troisième et quatrième catégorie de la classification des bois de Madagascar. Ces conditions de l'exploitation raisonnée de bois d'oeuvre sont les suivantes :

-Obtention annuelle d'un permis d'exploitation délivré par le DREF, -A partir du zonage retenu dans le PAGS, délimitation préalable de l'assiette annuelle de coupe, -Marquage des souches par des étiquettes plastiques blanches et élaboration du procèsverbal, -Coupes de proche en proche sans distinction d'essences des arbres marqués par des bûcherons locaux, membres de la coopérative MITSINJO, -Abattage des arbres par utilisation des scies passe-partout et équarrissage à la scie de long

  rôle des TGRN dans l'articulation des politiques de conservation et de valorisation des forêts : cas concret à Didy dans le cadre de l'intégration des contrats GELOSE dans le SAPM Ramenason Rasolonirina, Guybertho Randrianarivelo To cite this version: Ramenason Rasolonirina, Guybertho Randrianarivelo. rôle des TGRN dans l'articulation des politiques de conservation et de valorisation des forêts : cas concret à Didy dans le cadre de l'intégration des contrats GELOSE dans le SAPM. Rôle et place des transferts de gestion des ressources naturelles renouvelables dans les politiques forestières actuelles à Madagascar, Dec 2013, Madagascar. pp.9. cirad-00935062

que le massif forestier d'Ambohilero constitue un cas exceptionnel et unique à Madagascar par l'existence d'un cas d'exploitation forestière à l'intérieur d'une zone ciblée par la nouvelle aire protégée -corridor forestier Ankeniheny Zahamena. En

	application de l'arrêté
	ministériel n° 45 328 du 14 décembre 2011 portant délégation de gestion de la nouvelle Aire
	protégée en création CAZ, l'ONG conservation International dévient le gestionnaire officiel des
	la NAP CAZ.
	Cette présentation est composée par les deux parties suivantes :
	-Partie 1 : Bilan de dix ans de mise en place des contrats de TGRNR dans la commune de
	Didy : quel enseignement et expériences au vu du processus de mise en place de la NAP
	CAZ.
	-Partie 2 : Rôle des TGRNR dans l'articulation des politiques de conservation et de
	valorisation des forêts : cas concret à Didy dans le cadre de l'intégration des contrats
	GELOSE dans le SAPM
	projets de
	développement durable
	A partir du 2 août 2013, les 17 contrats GELOSE à objectif de conservation par la valorisation
	de la commune de Didy appuyés par le projet COGESFOR rentrent dans une nouvelle phase de
	prolongation de 10 ans. L'arrêté régional 04 REG /ALMAN/SG/DDR/EF en date du 26 avril
	2013 confirme l'application du SAFR [Schéma d'Aménagement forestier Régional Alaotra -
	Mangoro], comme référentiel de base de gestion du massif forestier d'Ambohilero. Il est retenu
	lors de l'atelier régional de validation en novembre 2011 que le SAFR constitue un schéma
	d'aménagement de rang 2. C'est-à-dire que ce document donne plus d'indication sur
	l'aménagement et le zonage forestier du secteur Didy par typologie des acteurs d'une part et
	rend opérationnel le PAG CAZ d'autre part.
	Le SAFR a été conçu dans un contexte technique et législatif complexe. Le Directeur Général
	des forêts n'a pas oublié de rappeler cette situation durant l'atelier sus mentionné. Il a réitéré

). Dans ce contexte, l'arrêté ministériel n° 45-328 du 14 décembre 2011 portant délégation de gestion de la nouvelle Aire protégée confit à l'ONG Conservation International le rôle de gestionnaire officiel de la nouvelle aire protégée du Corridor Ankeniheny-Zahamena jusqu'au 31 décembre 2014.

Cette présentation vise à ouvrir une discussion sur «le rôle des TGRNR dans l'articulation des politiques de conservation et de valorisation des forêts » sur la base d'une revue historique et analytique des enjeux de l'intégration des contrats GELOSE dans la NAP CAZ.

Mots clés : conservation, valorisation, articulation des politiques

2 Introduction

Madagascar, la Grande île de l'Océan Indien, est réputé internationalement pour sa méga biodiversité par le taux élevé d'endémicité des faunes et flores

[Falloux et Talbot, 1992]

. C'est également un pays où se confrontent différentes visions de la gestion durable, l'une tournée plutôt vers le développement et la recherche de l'autonomie des acteurs locaux par une mise en valeur durable de leurs ressources naturelles, l'autre mettant en priorité des objectifs de conservation et cherchant à limiter l'utilisation des ressources naturelles par les populations dans et autour des parcs nationaux -dont la superficie s'est fortement accrue dans les dernières années. Le paradoxe est que, souvent, les mêmes instruments de gestion de l'environnement sont mobilisés par les opérateurs, qu'ils soient acteurs de la conservation ou de

3 Partie 1 : Dix ans de mise en place des contrats de TGRNR GELOSE et GCF dans la commune de Didy : quel enseignement et expériences au vu du processus de mise en place de la NAP CAZ ? D

  'après les sources historiques, les premiers arrivants dans la forêt d'Ambohilero et dans la plaine de Didy étaient des chasseurs Betsimisaraka venant de l'Est pendant la période de XV ème siècle. Des migrants Bezanozano venant du Nord de Moramanga se sont ensuite installés dans la plaine et dans une partie de la forêt vers 1700. d'un arrêté d'interdiction de la délivrance de permis de type gré à gré en 2000 pour arrêter ce type d'exploitation forestière. Actuellement, plusieurs villages comme Sahafasenina abritent les descendants des bucherons.1995 -2004 : début de la réalisation des études sur la commune de Didy par des équipes pluri disciplinaires

	-Problème d'exploitation de béryl dans le site de Beahitra
	-Exploitation forestière destructrice par la société Malaisienne Latitude Timber à
	Antsevabe en 2004,
	Entre 1983 et 2002 : après la réouverture de la piste reliant Didy -Ambatondrazaka, 11
	exploitants forestiers se succédaient dans le massif forestier d'Ambohilero jusqu'en 2001
	[ONESF, 2010].
	2002 -2005 : première intervention de Conservation international et FFEM à Didy. Début du
	processus de mise en place des contrats de TGRNR
	2003 : CI / MIRAY a sous traité la mise en place des contrats de TGRNR GCF à l'ONG Adidy.
	FFEM a commencé les études techniques relatives à la mise en place des contrats GELOSE :

Entre 1700 et 1780, un grand nombre de conflit et d'alliance inter-clan et inter-ethnique a été enregistré d'où l'apparition des villages fortifiés de Nosy Didy. Selon le recensement, une vingtaine de lignages gèrent coutumièrement le massif forestier d'Ambohilero et dispose le droit d'usage et d'accès exclusif

[START_REF] Charbonnier | Limites et dynamiques coutumières dans la forêt classée d'Ambohilero, à l'intérieur de la cuvette de Didy[END_REF]

. D'après la tradition orale de la commune de Didy, le premier KIJANA forestier aurait été créé par les lignages ZAFINDRAVOLA. Jusqu'à maintenant, et malgré la mise en place du système de gestion de type « moderne » à développer dans le paragraphe en dessous, la gestion coutumière sous l'égide du Tangalamena [Chef de clan] reste toujours vivace est accepté par la population locale.

Le processus de mise en place des contrats de transfert de gestion de type GCF à objectif de conservation sans possibilité de valorisation économique et GELOSE à objectif de conservation par la valorisation de la ressource a commence officiellement à partir de 2002 par l'intervention des deux projets d'appui entre autre: l'ONG Conservation international et FFEM. En 2013, la commune rurale de Didy compte 25 contrats de transfert de gestion dont 8 de type GCF et 17 de types GELOSE dont 11 situés dans le nord du massif forestier d'Ambohilero et 7 à l'ouest du marais de Didy. Les 12 contrats GELOSE pratiquent par la valorisation raisonnée de la ressource forestière dont la filière bois d'oeuvre et huile essentielle.

Chronologiquement, l'historique de la mise en place des contrats de transfert de gestion dans la commune de Didy peut être récapitulé comme suit : Avant 1962 : la gestion forestière a été marquée par la domination du système coutumier et lignager.

1962 à 1983 : Le premier statut juridique du massif forestier d'Ambohilero date de 1962 par l'adoption de l'arrêté n° 2382 /MAP / FOR, portant classement de la forêt par le Ministère de l'agriculture et du paysannat. La forêt fut exploitée dès 1957 malgré le problème d'évacuation du bois occasionné par l'enclavement. La monographie de Didy révèle que les bucherons Betsimisaraka et Sihanaka s'installèrent dans le campement forestier pour fuir l'impôt ou karatra isan-dahy imposé par l'administration coloniale. L'ouverture de la piste Didy -Ambatondrazaka en 1983 a provoqué l'arrivée massive de l'exploitation forestière. Il faut attendre la promulgation diagnostic socio -économique -Inventaire forestier -Formation des enquêteurs locauximplication des médiateurs environnentaux agréée par l'ONE [application du décret 2000 028] Organisation d'un atelier de cadrage local de la méthodologie de mise en place des contrats de TGRNR à Didy avec la participation de CI/MIRAY, FFEM, équipe CIREF Ambatondrazaka. Ceci a aboutit aux deux conclusions suivantes :

-restructurer les associations demanderesse de TGRNR effectuée par l'ONG Adidy. Il faut que les propriétaires coutumiers se constituent en VOI. -découpage physique du massif forestier d'Ambohilero pour deux types de contrats de TGRNR : Nord : 8 contrats GELOSE appuyés par FFEM / SUD : 8 contrats GCF avec Beririnina au centre pour site de Pilote de GELOSE.

2003 : officialisation des contrats GCF pour une durée de 3 ans 2005 : officialisation du premier contrat GELOSE à objectif de conservation par la valorisation du VOI Beririnina pour une durée de 3 ans suivi de 7 autres contrats à la même année.

2013 : les 17 contrats GELOSE appuyés par le projet COGESFOR ont été renouvelés pour une période de 10 ans (2013 -2023).

Tableau 1: Les structures locales de gestion

	2009 -2013 Mise en place du SIEBO Antsevabe	PAG CAZ + PGESS +
		Mise en place de la coopérative des	Lancement PACT de conservation
		VOI MITSINJO
		Extension de la gestion de la filière vers
		la production d'huile essentielle
		certifiée BIO par ECOCERT,
		Opérationnalisation du système de
		contrôle forestier décentralisé
	4 Partie 2 :
		FFEM	Conservation International
		CCED [comité communal pour	Mise en place de l'union des VOI sous
		l'environnement le développement]	contrat GCF FTMAD
		régie par un arrêté communal,	Mise en place de la Fédération des VOI
		Mise en place des polisin'ala,	[GELOSE + GCF]
		Mise en place du Dina be communal	Mise en place des VNA et appui matériels
		Mise en place de la barrière de contrôle	Mise en place de KOLOHARENA
	2005 -2009	forestier d'Antsevabe, Dotation matériel des VOI pour l'exploitation raisonnée de bois d'oeuvre	Appui à la mise en place de la NAP CAZ Début du processus de mise en place de la NAP CAZ : réalisation de la consultation
		Mise en place de l'Union des VOI sous	publique relative à la mise en place de la
		contrat GELOSE SAHANALA	NAP
		Appui à l'obtention de permis de coupe,	Promulgation de l'arrêté de protection
		Mise en place du système de contrôle	temporaire
		forestier décentralisé et de la fiscalité	Elaboration des outils techniques de gestion :

Rôle des TGRNR dans l'articulation des politiques de conservation et de valorisation des forêts : cas concret à Didy dans le cadre de l'intégration des contrats GELOSE dans le SAPM

  La mise en place du SAPM a été basée sur une déclaration politique d'augmenter jusqu'à six million d'hectare la superficie des espaces protégées à Madagascar. Sur la base de l'expérience du projet COGESFOR appuyée par l'administration forestière régionale depuis 2002 dans le massif forestier d'Ambohilero, cette partie développe les recommandations sur les règles requises en matière d'exploitation forestière sous gestion contractuelle dans une zone ciblée par la mise en place du SAPM.

	-Mise en place des règles minimales d'exploitation et d'aménagement dans le site à
	transférer avec objectif de valorisation des produits,
	-Mise en place des procédures d'exploitation claire et
	-Opérationnalisation d'un système de contrôle forestier décentralisé accompagné avec la
	fiscalité pour assurer la pérennité et l'auto financement du contrôle.
	4.1

Se référant l'article 9 du décret n° 2005 -848 portant sur la mise en place d'une AP, « AP principalement selon le principe de l'utilisation durable des écosystèmes naturelles, en particulier pour des buts scientifiques, récréatifs et de subsistance, mais aussi économique. La protection et le maintien à long terme de la diversité biologique et des autres valeurs naturelles du site sont des objectifs essentiels de cette catégorie » Ce statut de Reserve de Ressources Naturelles permet la réalisation des activités suivantes:

-Activités spirituelles, -Activités scientifiques, -Activités éducatives récréatives et écotourisme, -Activités d'exploitation durable.

Dans ce sens, la NAP n'exclu pas la possibilité de réalisation d'une exploitation durable. Mais il faut baliser cette approche sur une base technique et organisationnelle claire et concertée avec les acteurs. Au travers les expériences du projet COGESFOR dans la commune de Didy, les propositions des conditions d'efficacités de l'exploitation dans site ciblé par le SAPM sont basées sur les trois aspects suivants :

Règles minimales d'exploitation et d'aménagement dans le site de transfert de gestion ciblé par le SAPM

  'aspect de valorisation doit être indiqué clairement dans l'objectif de gestion de la communauté gestionnaire.-Le site objet de la gestion contractuelle doit être délimité contradictoirement c'est-à-dire en présence des riverains. La carte et les limites seront affichées publiquement au bureau de la commune de rattachement de la ressource au moins pendant 30 jours. Le maire délivre un certificat d'affichage en cas d'absence d'une éventuelle opposition par un tiers. Encadré 1 : article 54 de la loi GELOSE Article 54 : Les communautés de base agréées, bénéficiaires du transfert de gestion dans le cadre de la présente loi auront droit à certains avantages pour la commercialisation et la valorisation des ressources renouvelables et des produits dérivés. Les avantages concédés aux communautés de base agréées, sur la base de certificats d'origine des ressources ou produits dérivés, seront de caractère essentiellement économique utilisant en particulier les outils de la parafiscalité. Ces avantages seront institués par voie législative. Ils permettront aux communautés de base agréées d'assurer par une meilleure valorisation une gestion viable et durable à long terme des ressources dont la gestion leur est concédée et la conservation globale de la biodiversité des ressources de leur terroir. Ils viseront par ailleurs à mettre en place une incitation économique effective de nature à déterminer les communautés de base non encore agréées à demander le transfert de gestion et le bénéfice de l'agrément. Ces avantages seront institués de façon différentielle selon chacune des ressources concernées et leur mode de gestion. Dans un souci de saine gestion économique et d'adaptation continue aux conditions de l'économie de marché, ils seront ajustables par voie réglementaire. -Le zonage de chaque site de TGRNR répond au principe de 1/3 de valorisation et de droit d'usage et 2/3 de conservation [NDC]. Pour une surface forestière de 41 858 ha sous contrat GELOSE du massif forestier d'Ambohilero, la zone de valorisation est limitée 6 856 ha soit 5 % d'Ambohilero et 2 % de la NAP CAZ, 19 749 ha de zone de conservation et 15 241 ha de droit d'usage.

Des règles minimales d'exploitation et d'aménagement doivent être appliquées pour assoir la gestion durable des ressources forestières entre autre les aspects cités en dessous :

-la valorisation durable des filières porteuses doit être effectuée dans un cadre légale et réglementaire autorisant l'exploitation. Exemple : pour le cas des contrats de transfert de gestion de Didy, l'article 54 de la loi GELOSE [Cf encadré] autorise l'exploitation. L

3 Le contrôle forestier décentralisé [CFD] et la fiscalité sur les produits forestiers objet de la valorisation économique

  pour réduire les pertes d'exploitation et augmenter le rendement matière, -Enregistrement systématique du numéro des souches, du nombre des produits et de la date de coupe dans un cahier de chantier à trois volets. Les souches sont utilisées pour le contrôle. Une est conservée par le VOI, -Réception des produits sur la place de dépôt signalée préalablement à l'administration forestière. La réception implique un agent communal, un agent forestier et un polisin'ala. Un procès-verbal est dressé à la fin de la réception, -Opération d'étiquetage des produits par le VOI, de poinçonnage au marteau forestier par un agent de l'administration forestière et avec un marteau numéroteur pour la commune et d'écriture du code de traçabilité nationale, -Enregistrement systématique de toutes les données d'exploitation dans le système d'information bois d'oeuvre (SIEBO) tenu par un agent de l'administration forestière à Antsevabe (barrière de contrôle forestier) pour pouvoir délivrer une autorisation de transport, -Délivrance des dossiers administratifs nécessaires au transport des produits soit (i) autorisation de transport, (ii) fiche d'apurement de stock et (iii) laissez passer, -Paiement des ristournes communales et régionales et redevances d'exploitation forestière.Le CFD est un mécanisme de suivi, surveillance et contrôle d'un périmètre de site en gestion contractuelle. Il vise à décharger l'administration de tutelle de certaines tâches qui peuvent être réalisées localement, selon l'article 1 de la loi GELOSE « en vue de permettre la participation effective des populations rurales à la conservation durable des ressources naturelles renouvelables, il peut être confié à la communauté de base, dans les conditions prévues par la présente loi, la gestion de certaines de ces ressources comprises dans les limites de leur terroir ». Pour le cas de l'exploitation raisonnée de bois d'oeuvre des VOI, le contrôle et le suivi de l'exploitation au niveau du chantier jusqu'à la commercialisation est le coeur des activités des acteurs désignés. L'enjeu de l'opération est de garantir au maximum la légalité de l'exploitation, assurer le respect du plan d'aménagement plus particulièrement, le principe du quota et la rotation de la coupe et éviter la commercialisation frauduleuse des produits illicites. La caisse CFD permet d'assurer la pérennité du contrôle forestier local avec ou sans appui d'un partenaire technique et financier. Le flux des informations peut être synthétisé comme suit :

4.

Figure 1 : Flux des informations sur le contrôle forestier décentralisé 5 Conclusion Le

  cas de conservation par la valorisation des ressources naturelles renouvelables des VOI sous contrats GELOSE du massif forestier d'Ambohilero est un exemple concret de la possibilité de concilier le système d'aire protégée de catégorie VI avec l'aspect de gestion forestière communautaire. Même si l'exemple développé dans cette présentation se limite sur le cas de l'exploitation forestière, l'expérience peut être appliquée dans d'autre filière porteuse. En 10 ans d'intervention dans la commune rurale de Didy, le projet se permet de conclure que « la gestion durable de forêt est basée sur la valorisation des richesses jusqu'alors monopolisées par des exploitants souvent étrangers ». L'administration forestière au travers son service technique déconcentré assurera la pérennisation et la duplication des résultats dans les autres sites. La forêt d'Ambohilero, actuellement ciblée par la mise en place de la NAP CAZ. C'est à l'administration et à la communauté de s'approprier en poursuivant les efforts accomplis par le projet COGESFOR ». On n'a jamais démontré que conservation par la valorisation et aire protégée doivent être appliquées dans deux massifs distincts.

	Mission de surveillance	Contrôle forestier des agents
	des VOI		de l'administration
	Elaboration du compte rendu à l'administration	Application du Dina en cas d'infraction	En cas de poursuite
	forestière et la commune
			P.V.
			(

par les OPJ) TRANSACTION (AF) POURSUITE JUDICIAIRE Elaboration ou Acte de transaction Déferrement au parquet Exécution Non Exécution Attestation d'exécution Reprise poursuite judiciaire Clôture du dossier AUDIENCE JUGEMENT Clôture Interjection d'appel

  Institut de Géographie Université de Neuchâtel. Pour l'obtention du grade de docteur ès Sciences Humaines. 270 p. Loi n° 96 025 du 30 septembre 1996 relative à la Gestion Locale des Ressources Naturelles Renouvelables ou GELOSE -Loi n° 94 -007 du 26 avril 1995 relative aux pouvoirs des Collectivités Territoriales Décentralisées (CTD). -Décret n° 98-782 du 16 septembre 1998, relatif au régime de l'exploitation forestière à Madagascar. -Loi n° 97-017 du 8 aout 1997 portant révision de la législation forestière Malagasy -Décret n° 97-1200 du 2 octobre 1997 portant adoption de la politique forestière malagasy -Décret n° 98-782 du 16 septembre 1998 relatif au régime d'exploitation forestière -Arrêté n°12 702/2000 portant instruction de dossier de demande de délivrance de permis d'exploitation de permis de coupe à titre onéreux -Arrêté ministériel n°12.702/2000 en 2000 portant suspension d'instruction de dossier de demande, de délivrance de permis d'exploitation et de permis de coupe a titre onéreux -Arrêté n° 18 633 du 17 octobre 2008 portant mise en protection temporaire globale des sites visés par l'arrêté n° 17914 du 18 octobre 2006, -Arrêté n° 45 328 du 14 décembre 2011 portant délégation de gestion de la nouvelle Aire protégée en création dénommée CAZ, la forêt d'Ambohilero entre provisoirement dans le régime d'une AP

	Textes forestiers
	-


T Triki
email: taha.triki@imag.fr

Y Ledru
email: yves.ledru@imag.fr

L Du Bousquet
email: lydie.du-bousquet@imag.fr

F Dadeau

J Botella
email: julien.botella@smartesting.com

Model-based filtering of combinatorial test suites

Tobias is a combinatorial test generation tool which can efficiently generate a large number of test cases by unfolding a test pattern and computing all combinations of parameters. In this paper, we first propose a model-based testing approach where Tobias test cases are first run on an executable UML/OCL specification. This animation of test cases on a model allows to filter out invalid test sequences produced by blind enumeration, typically the ones which violate the pre-conditions of operations, and to provide an oracle for the valid ones. We then introduce recent extensions of the Tobias tool which support an incremental unfolding and filtering process, and its associated toolset. This allows to address explosive test patterns featuring a large number of invalid test cases, and only a small number of valid ones. For instance, these new constructs could mandate test cases to satisfy a given predicate at some point or to follow a given behavior. The early detection of invalid test cases improves the calculation time of the whole generation and execution process, and helps fighting combinatorial explosion.

Introduction

Combinatorial testing is an efficient way to produce large test suites. In its basic form, combinatorial testing identifies sets of relevant values for each parameter of a function call, and the production of the test suite simply generates all combinations of the values of the parameters to instantiate the function call. JMLUnit [START_REF] Cheon | A simple and practical approach to unit testing: The JML and JUnit way[END_REF] is a simple and efficient tool based on this technique, which uses JML assertions as the test oracle. Extended forms of combinatorial testing allow to sequence sets of operations, each operation being associated to a set of relevant parameters values. This produces more elaborate test cases, which are appropriate to test systems with internal memory whose behaviour depends on previous interactions. Tobias [START_REF] Maury | Using Tobias for the automatic generation of VDM test cases[END_REF][START_REF] Ledru | Filtering TOBIAS combinatorial test suites[END_REF][START_REF] Ledru | Mastering combinatorial explosion with the Tobias-2 test generator[END_REF] is one of these combinatorial generators. It was used successfully on several case studies [START_REF] Du Bousquet | Reusing a JML specification dedicated to verification for testing, and vice-versa: case studies[END_REF][START_REF] Dupuy-Chessa | Test of the ICARE platform fusion mechanism[END_REF][START_REF] Ferro | Generation of test programs for the assertion-based verification of TLM models[END_REF] and has inspired recent combinatorial testing tools, such as the combinatorial facility of the Overture toolset for VDM++ [START_REF] Lausdahl | Connecting UML and VDM++ with open tool support[END_REF] or jSynoPSys [START_REF] Dadeau | jSynoPSys -a scenario-based testing tool based on the symbolic animation of B machines[END_REF].

Tobias takes as input a test pattern and performs its combinatorial unfolding into a possibly large set of test cases. Each test case usually corresponds to a sequence of test inputs. An additional oracle technology is needed to decide on successful or failed test executions. In the past, we have mainly used the run-time evaluation of JML assertions as a test oracle [START_REF] Du Bousquet | Reusing a JML specification dedicated to verification for testing, and vice-versa: case studies[END_REF]. But the tool can be used in other contexts than Java/JML. In this paper, we adopt a modelbased testing approach where tests are first played on a UML/OCL specification of the system under test. The animation of a sequence of operations on the UML/OCL specification is performed by the Test Designer tool of Smartesting 4and brings two kinds of answers. First, it reports whether the sequence is valid, i.e. each of its calls satisfies the pre-condition of the corresponding operation and is able to produce an output which verifies the post-condition. Then, it provides the list of intermediate states and operation results after each operation call. This information can be used as test oracle to compare with the actual states and results of the system under test. It must be noted that the model is deterministic, which forces all accepted implementations to produce the same results and intermediate states (if observable). In summary, the model is used (a) to discard invalid sequences, and (b) to provide an oracle for valid ones.

Combinatorial testing naturally leads to combinatorial explosion. This is initially perceived as a strength of such tools: large numbers of tests are produced from a test pattern. This helps to systematically test a system by the exhaustive exploration of all combinations of selected values. The latest version of Tobias has been designed to generate up to 1 million abstract test cases. It is actually only limited by the size of the file system where the generated tests are stored. Unfortunately, the translation of these test cases into a target technology such as JUnit, the compilation of the resulting file and its execution usually require too much computing resources and, in practice, the size of the test suite must be limited between 10 000 and 100 000 test cases.

Several techniques can be adopted to limit combinatorial explosion. The most classical one is the use of pairwise testing techniques [START_REF] Cohen | The combinatorial design approach to automatic test generation[END_REF] which does not cover all combinations of parameter values but simply covers all pairs of parameter values. This technique is very efficient to reduce a large combinatorial test suite to a much smaller number of test cases, but it relies on the hypothesis that faults result from a combination of two parameters. Therefore it may miss faults resulting from a combination of three or more parameters. The technique can be generalized to cover all n-tuples of parameters but it may always miss combinations of n + 1 parameters. Another approach is the use of test suite reduction techniques [START_REF] Harrold | A methodology for controlling the size of a test suite[END_REF] which select a subset of the test suite featuring the same code coverage as the original test suite. This technique has several limitations. First, it requires to play the full test suite in order to collect coverage information. Also, empirical studies have shown that test suite reduction may compromise fault detection [START_REF] Rothermel | An empirical study of the effects of minimization on the fault detection capabilities of test suites[END_REF].

In this paper, we consider the case where combinatorial test suites lead to a large proportion of invalid test cases, i.e. test cases which will not be accepted by the specification. These invalid test cases must be discarded from the test suite because the specification is unable to provide an oracle for these tests. Discarding these invalid test cases leads to a safe reduction of the test suite. We present a tool which incrementally unfolds a test pattern and discards invalid test cases. The tool is based on an evolution of the Tobias tool where several new constructs have been added to the base language.

Section 2 introduces an illustrative case study. Then Section 3 presents the basic constructs of Tobias, using the case study. Section 4 presents additional constructs which help filter combinatorial test suites. Section 5 presents the toolset which incrementally unfolds the test patterns and filters the resulting test suite. Section 6 reports on several experiments carried with this tool set. Section 7 gives an overview of the research literature related to our work. Finally, Section 8 draws the conclusions of this work. We consider the example of a smart card application, representing an electronic purse (e-purse). This purse manages the balance of money stored in the purse, and two pin codes, one for the banker and one for the card holder. Similarly to smart cards, the e-purse has a life cycle (Fig. 1), starting with a Personalization phase, in which the values of the banker and holder pin codes are set. Then a Use phase makes it possible to perform standard operations such as holder authentication (by checking his pin), crediting, debiting, etc. When the holder fails to authenticate three consecutive times, the card is invalidated. Unblocking the card is done by a banker's authentication. Three successive failures in the bank authentication attempts make the card return to the Personalization phase. Each sequence of operations is performed within sessions, which are initiated through different terminals. This example has originally been designed to illustrate access control mechanisms, and it is used a basis for test generation for access control 5 . It was already used to illustrate test suite reduction with Tobias [START_REF] Dadeau | Directed random reduction of combinatorial test suites[END_REF]. The original example was specified in JML. We have translated this specification into a UML/OCL model for the Smartesting Test Designer tool.

In Test Designer (TD), information about the behaviour of operations is captured in assertions associated to the operations. In the perspective of animation, these assertions must characterize a deterministic behaviour. An example of the pre-and post-conditions of the checkPin(int) operation is given Fig. 2. Post-conditions represent the code to be animated by TD if the pre-condition is verified. TD uses an imperative variant of OCL6 , inspired by the B language [START_REF] Abrial | The B Book -Assigning Programs to Meanings[END_REF]. The variables appearing in the right hand side of a = sign are implicitly taken in their pre-state (usually denoted in OCL by @pre). In the model, the conditional branches are tagged with special comments. For example if the pin code is equal to the right one (self.hpc_), the tag @AIM:HOLDER_AUTHENTICATED will be activated and saved by the animator. After animation of an operation call, TD provides the list of all activated tags. The set of activated tags after an execution represents a behaviour of an operation. For example, the set: B1 = {@AIM:HOLDER_IS_NOT_AUTHENTICATED,@AIM:MAX_NUMBER_OF_TRIES_REACHED} is a behaviour of the checkPin operation leading to INVALID mode.

Basic Tobias test patterns

To generate test cases, Tobias unfolds a test pattern (also called "test schema"). The textual Tobias input language (TSLT) contains several types of constructs allowing the definition of complex system scenarios. The key concept in the Tobias input language is the group concept which defines a set of values or sequences of instructions. The group concept is subject to combinatorial unfolding. Some other concepts can be applied to instructions like iteration or choice. To illustrate these constructs, let us consider the following pattern:

group EPurseSchema1 [us=true, type=instruction] { @IUT; @Personalize; @AuthenticateHolder; @Transaction{1,3} EPurseSchema1 is a group of instructions (type = instruction), and the flag us indicates whether the group will be unfolded (=true) or not. This group is a sequence of 4 other groups: IUT, Personalize, AuthenticateHolder and Transaction. This last group will be repeated one to three times in the sequence. The IUT group defines a new instance of class EPurse. Then, the Personalize group opens a new ADMIN session, sets the banker and the holder PIN codes, and finally closes the session. The AuthenticateHolder group authenticates the holder, and finally the Transaction group allows to do transactions. We use groups of values in some operation calls. For instance, the parameter of the setBpc method has 2 possible values.

The iteration construct {m,n} repeats an instruction, or a sequence of instructions, from m to n times or exactly m times. For example, in group Au-thenticateHolder, the checkPin operation is iterated 1 to 4 times (to check all possible sequences of correct/incorrect user authentication.

The Transaction group illustrates the choice construct. It consists of an exclusive choice between the two operation calls Debit or Credit. Each of them can be instantiated by three different amounts.

The EPurseSchema1 pattern is unfolded into 30 960 test cases :

1 * (2*2) * (2 1 +2 2 +2 3 +2 4 ) * ((3 * 2) 1 +(3 * 2) 2 +(3 * 2) 3
). Only 2776 test cases are valid ones (i.e. satisfy the pre-conditions). In Fig. 3, examples of test cases unfolded from EPurseSchema1 are given, TC3 is valid, contrary to TC26835 (which executes 4 consecutive calls to the checkPin operation with the wrong Pin code) and TC30960 (which executes a debit operation but never credits).

If we put the maximum iteration bound of Transaction to 10, it would result into 8 707 129 200 test cases and would cause combinatorial explosion. In the next sections, we will see how the new Tobias constructs make it possible to take such explosive test patterns into account.

New Tobias constructs

Here, we introduce three new constructs for the Tobias input language. These constructs support new techniques for filtering test cases. This allows to control the size of the produced test suite, and incrementally pilot the combinatorial unfolding process. These constructs are inspired by the jSynoPSys scenario language [START_REF] Dadeau | jSynoPSys -a scenario-based testing tool based on the symbolic animation of B machines[END_REF] and are syntactically and semantically adjusted to meet our needs.

The State predicate construct inserts an OCL predicate in the test sequence.

The predicate expresses that a property is expected to hold at this stage of the test sequence. Tests whose animations do not satisfy this OCL predicate should be discarded from the test suite. It allows the tester to select a subset of the unfolded test suite featuring a given property at execution time. For example, not all AuthenticateHolder animations succeed. Therefore, we define a state predicate to select the tests which succeed the authentication. The pattern is defined as follows:

group EPurseSchema5 [us=true, type=instruction] { @IUT; @Personalize; @AuthenticateHolder❀({ep} , self.isHoldAuth_ = true); @Transaction; } AuthenticateHolder performs checkPin one to four times. Then the pattern selects those sequences which end up with a successful authentication. The TSLT construct takes the form ❀(set of targets , OCL predicate), where the set of targets identifies the objects which correspond to self in the OCL predicate.

Here the set of targets is the singleton including ep.

The behaviours construct is another way to filter tests. It applies to an operation and keeps the tests whose animation covers a given behaviour, expressed as a set of tags. For example, in the previous pattern (EPurseSchema5), instead of using a state predicate to keep tests that succeed the holder authentication, we select the authentication sequences whose last call to checkPin covers the tag @AIM:HOLDER_AUTHENTICATED.

group EPurseSchema6 [us=true, type=instruction] { @IUT; @Personalize; @AuthenticateHolder2; @Transaction; } group AuthenticateHolder2 { ep.beginSession(Terminal.PDA); ep.checkPin(@UserPinValue){0,3}; ep.checkPin(@UserPinValue)/w{set(@AIM:HOLDER_AUTHENTICATED)}; }

After the last call to checkPin, we put the symbol /w and we define a set of tags that must be activated after the operation execution. Here, when the pin code is correct, the tag @AIM:HOLDER AUTHENTICATED is covered in the post-condition of checkPin (see Sect. 2).

The Filtering key is called after an instruction. It allows to accept a set of succeeded tests at some position and to discard the others. Then it will select some of the succeeded tests. TSLT group EPurseSchema7 [us=true, type=instruction] { @Prologue_ONE; @Transactions; } group Prologue [us=true, type=instruction] { @IUT;@Personalize; @AuthenticateHolder2; } 5 The incremental unfolding and filtering process

Standard unfolding and filtering process

Before introducing the mechanism of incremental unfolding, we begin by presenting the process of generation, animation and filtering of test cases by coupling the Tobias and Test Designer tools (Fig. 4). The starting point is a schema file including a test pattern written in TSLT. Three steps are automatically involved to produce the test evaluation results:

1. The schema file is unfolded by the Tobias tool which generates one or several test suite files written in the XML output language of the tool (outob file).

For each group marked in TSLT as us=true, Tobias produces an outob file. This file contains all abstract test cases generated by the combinatorial unfolding of the corresponding group. 2. The outob files are translated into JUnit test suites including all necessary information to animate test cases. Each JUnit test case interacts with the API of TD to animate the model. We take advantage of the JUnit framework and the Java API of TD to animate the tests in a popular and familar tool for engineers, and to benefit from the JUnit structure of test suites. 3. JUnit executes the test suites. Each test case is animated on the TD model through the TD API. The animation process allows to identify and filter out invalid test cases, i.e. the ones which:

include some operation call that violates its precondition, -include some operation call that violates its postcondition, -do not fulfill some state predicate or include some operation call that fails to activate its associated behaviours.

The animation of test cases proceeds sequentially. If an instruction fails because of one of these four reasons, the animation of the test stops and the test case is declared as failed and discarded from the test suite. The valid ones are saved to a repository.

Incremental unfolding and filtering process

Algorithm The standard process requires to completely unfold the test patterns and to animate each test case of each test suite. At this stage, we did not take advantage of filtering keys ( ONE, ALL, n, n%). These filtering keys can be applied on the resulting test suite to select the relevant test cases. In this section, we will see that the early application of filtering keys may lead to significant optimisations of (a) the unfolding process and (b) the animation of the test suite.

The incremental process is defined for the unfolding of a single pattern p. It can be generalized to unfold multiple patterns. Its algorithm is given in Fig. 5 and performs the following steps:

-At each iteration, pattern p is divided into a prefix, located before the first filtering key, and a postfix, located after it. -The standard unfolding and filtering process of Sect. 5.1 is applied to the prefix. It results into a group of valid unfolded prefixes. -A subset of this group is selected according to the filtering key.

-This subset of valid unfolded prefixes is concatenated with the postfix to form the new value of p. -The process iterates until all filtering keys are processed in the pattern.

-A last unfolding is applied to the resulting pattern stored in p. Example To illustrate this incremental process, consider the following pattern:

group EPurseSchema9 [us=true, type=instruction] { @IUT; @Personalize; @AuthenticateHolder❀({ep} , self.isHoldAuth_ = true)_ONE; @Transactions;} Before calling @Transactions, we would like to choose just one (_ONE) sequence of operations that succeeds holder authentication. The prefix of this pattern is:

group EPurseSchema9pre [us=true, type=instruction] { @IUT; @Personalize; @AuthenticateHolder❀({ep} , self.isHoldAuth_ = true); } This prefix is then unfolded using the standard process. Since there is no remaining filtering key, the whole pattern will be unfolded to generate the final test cases. This unfolding leads to 6 test cases, where only 3 are valid. The final number of valid test cases may depend on the prefix that will be chosen randomly. These test cases will be animated to discard the invalid ones, and then produce the filtered test suite. This process is clearly optimized since only 126 test cases were completely unfolded, instead of 720 in the standard process. In the next section, we present experimental results on more complex examples.

Some experimental results

Let us consider the following example:

group EPurseExample [us=true, type=instruction] {@IUT; @Personalize; @AuthenticateHolder❀({ep} , self.isHoldAuth_ = true);@Transactions{4};}

The EPurseExample is unfolded into 155 520 test cases. Our tools succeed to achieve steps 1 and 2 (translation into TSLT and production of an outob file).

Unfortunately, the translation of the outob XML file into a JUnit file crashes due to a lack of memory (we used up to 1.5Gb of RAM). If this had succeeded, we presume that the compilation of the JUnit file would also crash. These technical problems can be overcome by decomposing our files into smaller ones, but still the whole process would take time and computing resources. Other group definitions can rapidly reach over 1 million test cases which may require untractable time and memory resources. We redefine the pattern by introducing filtering keys:

group EPurseExampleUsingKeys [us=true, type=instruction] { @IUT; @Personalize; @AuthenticateHolder❀({ep} , self.isHoldAuth_ = true); @Transactions_ALL; @Transactions_ALL; @Transactions_ALL; @Transactions; } This pattern will produce the same valid test cases as the previous one, since we used the _ALL key. Using the incremental process, we need four iterations to remove the three filtering keys and unfold the resulting pattern. The pattern is completely unfolded and animated in 175 seconds as given in Fig. 6. As a result our 155 520 test cases only include 6496 valid ones. To identify these, our incremental process needs four iterations but only unfolds and plays 16512 test cases. In this case, it performed the selection process using 10% of the resources needed for the standard one, and kept the test suites small enough to avoid tool crashes.

Support for a brute force approach. Let us consider another explosive pattern, based on Fig. 1. The aim of this pattern is to find test sequences where the purse goes back to Personalisation mode, before being set in Use mode. The only way to reach this goal is to start from P erso mode, go into U se and Invalid modes, before getting back to P erso and finally to U se. These major steps are captured in the state predicates of the following pattern:

group EPurseSchema18op [us=true, type=instruction] { @IUT; @ALLOps{4}❀({ep}, self.mode_ = Mode::USE); @ALLOps{5}❀({ep}, self.mode_ = Mode::INVALID); @ALLOps{5}❀({ep}, self.mode_ = Mode::PERSO); @ALLOps{4}❀({ep}, self.mode_ = Mode::USE); }

In order to change states, we adopt a brute force approach where a single group has been defined for all operations offered by the card. Group ALLOps can be unfolded in 19 elements.

group ALLOps { ep.beginSession(@TerminalValue) | ep.endSession() | ep.setBpc(@BankPinValue) | ep.setHpc(@UserDebitValue) | ep.authBank(@BankPinValue) | ep.checkPin(@UserDebitValue) | ep.credit(@Amounts) | ep.debit(@Amounts); } EPurseSchema18op repeats all operations 4 times, until it reaches the U se mode. Finding that it requires 4 iterations can result from a trial and error process, or from a careful study of the specification. Since we adopt a brute force approach, let us consider that the engineer has attempted to reach the U se mode in one to three steps, without success, and finally found that four steps were sufficient (session opening, setting the Holder and Bank codes, and session close). Similarly he found that 5 steps are the minimum to reach state Invalid (session opening, three unsuccessful attempts to checkPin and session close), and to then reach state P erso (session opening, three unsuccessful attempts to authBank and session close). As a result, to find a valid sequence reaching the U se mode and returning to the same mode after visiting the other modes, we need to call at least 18 operations (4+5+5+4). EPurseSchema18op represents 19 18 test cases (about 10 23 test cases), and thus cannot be directly unfolded. Because of the brute force approach, and because we inserted filtering predicates, a large number of these test cases will be invalid. This enables us to call the incremental process. We redefine EPurseSchema18op using the filtering key ALL to keep all valid prefixes.

group EPurseSchema18opWFilteringKey [us=true, type=instruction] { @IUT; @ALLOps_ALL; @ALLOps_ALL; @ALLOps_ALL; @ALLOps❀({ep}, self.mode_ = Mode::USE)_ALL; @ALLOps_ALL; @ALLOps_ALL; @ALLOps_ALL; @ALLOps_ALL; @ALLOps❀({ep}, self.mode_ = Mode::INVALID)_ALL; @ALLOps_ALL; @ALLOps_ALL; @ALLOps_ALL; @ALLOps_ALL; @ALLOps❀({ep}, self.mode_ = Mode::PERSO)_ALL; @ALLOps_ALL; @ALLOps_ALL; @ALLOps_ALL; @ALLOps❀({ep}, self.mode_ = Mode::USE); } EPurseSchema18opWFilteringKey is unfolded incrementally in 18 iterations. Fig. 7 shows the number of unfolded and accepted tests at each iteration. Steps 9 and 14 show how filtering predicates dramatically decrease the number of accepted tests. Fig. 7 shows that the number of test cases animated at each step remains small enough to be handled with reasonable time and computing resources, and to avoid tool crashes. As a result, we unfolded and animated a total of 85424 test cases for the 18 iterations in less than 17 minutes, instead of 19 18 in the standard process. We finally found all 640 valid test cases hidden into this huge amount of potential test cases. This second example shows that this incremental technique is efficient to find complex test cases hidden in a huge search space. The key to success is to make sure that the use of filtering keys will effectively reduce or limit the number of test cases at each iteration. Therefore, one should prefer a specification and a test pattern which help identify invalid test cases as soon as possible.

Improvements with respect to our previous work. In the past [START_REF] Ledru | Filtering TOBIAS combinatorial test suites[END_REF][START_REF] Ledru | Mastering combinatorial explosion with the Tobias-2 test generator[END_REF] In [START_REF] Ledru | Mastering combinatorial explosion with the Tobias-2 test generator[END_REF] we filtered the elements of the test suite whose text did not fulfill a given predicate. This predicate is freely chosen by the test engineer and does not prevent to filter out useful test cases. For example, one could filter out all test cases whose length was longer than a given threshold. In [START_REF] Dadeau | Directed random reduction of combinatorial test suites[END_REF][START_REF] Ledru | Mastering combinatorial explosion with the Tobias-2 test generator[END_REF], we investigated the use of random selection techniques. These techniques are by essence unable to distinguish between valid and invalid test cases, but they are able to reduce the number of test cases to an arbitrary number whatever be the size of the initial test suite. Compared to these selection techniques, our incremental process does not discard valid test cases, but makes the assumption that the number of valid test cases is small enough to remain tractable.

Related work

In [START_REF] Jagannath | Reducing the costs of boundedexhaustive testing[END_REF], authors propose to study test reduction in the context of boundedexhaustive testing, which could be described as a variation of combinatorial testing. Three techniques are proposed to reduce test generation, execution time and diagnosis. In particular, the Sparse Test Generation skips some tests at the execution to reduce the time to the first failing test. Unlike ours, this approach does not rely on a model to perform test generation and reduction. Our approach allows filtering large combinatorial test suites by animating them on an UML/OCL model. It eliminates tests which don't verify the pre and post conditions of operations and/or given predicates or states. Generating tests or simply checking their correctness, is a classical approach when a model is available (principle of the "model-based testing" approaches). For instance, in [START_REF] Grieskamp | Interaction coverage meets path coverage by SMT constraint solving[END_REF], authors generate automatically a combinatorial test suite, that satisfies both the specification and coverage criteria (among which pairwise coverage of parameter values). The generation engine is based on a constraint solver and the specification is expressed in Spec#. In [START_REF] Belhaouari | A constraint logic programming approach to automated testing[END_REF], authors also propose to automate test case generation with a constraint solver, but the specification is expressed as contracts extended with state machines. For both, the objective of the work is to generate a test suite which fulfills a coverage criterion on a model. In our approach, the test schema gives a supplementary selection criterion for test generation. In [START_REF] Constant | Automatic test generation from interprocedural specifications[END_REF], specification is expressed as IOLTS and generation is done with respect to a test purpose, for conformance testing. In some way, our test schema can be compared to a sort of test purpose, but contrary to this work where only one test is generated for each test purpose, we aim at generating all the test cases satisfying the test purpose.

The problem of test suite reduction is to provide a shorter test suite while maintaining the fault detection power. The approach presented in [START_REF] Heimdahl | On the effect of test-suite reduction on automatically generated model-based tests[END_REF] generates test suites from a model and traps properties corresponding to structural coverage criteria. An algorithm is then executed on the resulting test suite to generate a reduced test suite having the same coverage than the original one. The original and the reduced test suites are animated on a faulty model to compare their fault localization capabilities. In [START_REF] Fraser | Redundancy based test-suite reduction[END_REF], authors propose an approach where test cases created thanks to model-checker are transformed such that redundancy within the test-suite is avoided, and the overall size is reduced. Our approach differs from test suite reduction techniques in two points. First, we don't need to execute all tests of the original test suite to perform the reduction, and second, we consider that all valid test cases are equivalent when performing reduction with the filtering keys. YETI 7 is a random test generation tool which generates test cases from program bytecode. The number of generated test cases is limited by the available time. The report shows in a real time GUI the bugs found sofar, the coverage percentage according to a classical coverage criteria, the number of system calls and the number of variables used in the system to carry out the test generation and execution. Compared to our toolset, our approach performs the generation of tests from a UML/OCL model and not from a program. The choice of the methods under test, the length of the call sequences and the parameter values is not done randomly as in the YETI tool but according to a careful test schema defined by the user. Contrary to our tool, the notion of filtering against specific states or behaviors and the incremental unfolding do not exist in the YETI tool whose purpose is to maximize bugs detection and structural coverage.

Conclusion and perspectives

In this paper, we address the problem of filtering a large combinatorial test suite with respect to a UML/OCL Model. The whole approach relies on three main steps. First the set of tests to generate has to be defined in terms of a test pattern, expressed in a textual language called TSLT. Second, this schema is unfolded to produce abstract test cases that are animated within Smartesting Test Designer tool. This animation allows to identify and remove invalid test cases. The process of unfolding and filtering can be done incrementally so that potential combinatorial explosion can be mastered. Several examples have been presented. They show that the incremental process is able to generate all valid test cases scattered in a huge search space, provided that the number of valid test cases remains small enough. This paper has presented several new constructs which help the test engineer to express more precise test patterns and to filter out invalid test cases at early stages of the unfolding process. From a methodological point of view, this requires to augment the test pattern with state predicates, behaviour selectors, and filtering keys, which keep the incremental process within acceptable bounds. This approach has been defined in the context of the ANR TASCCC Project. We intend to apply it soon to the Global Platform case study provided by Gemalto, a last-generation smart card operating system8 . This model presents 3 billions of possible atomic instantiated operation calls, due to combination of operations parameters values. A large proportion of these latters represent erroneous situations that should not be considered.

Fig. 1 .

 1 Fig. 1. The main modes of the bank card and the main operations

Fig. 2 .

 2 Fig. 2. Pre and post-condition for checkPin(int) operation

Fig. 4 .

 4 Fig. 4. The process of generation and filtering test cases (standard process)

algorithmFig. 5 .

 5 Incremental_Generation_And_Execution_Process (p): while( p contains at least one filtering key ) Let (prefix _1stKey ; postfix) match p in validPrefixes := apply_Standard_Process(prefix); validPrefixesSubset := Select_Subset_Of_ Valid_Prefixes_According_To(1stKey); p := (validPrefixesSubset ; postfix); end while result := apply_Standard_Process(p); end The incremental unfolding algorithm

  provides four filtering keys ( ONE, ALL, n, %n) to keep one, all, n or n% of the valid prologues. If we want to accept all of them we use ALL, just one we use ONE and n (resp. %n) randomly selects n (resp. n% of the) test cases amongst the valid ones. For example consider EPurseSchema7. The prologue group leads the purse to a state where the holder is authenticated. If the test engineer simply wants to keep one of these, he can add keyword _ONE after the prologue :

  Results of EPurseSchema18opWFilteringKey unfoldingexecution time is based on a simple idea: if the prefix of a test case fails, then all test cases sharing the same prefix will fail. In[START_REF] Ledru | Filtering TOBIAS combinatorial test suites[END_REF], we have proposed an intelligent test driver which remembers the failed prefixes, and avoids to execute a test case starting with a prefix which previously failed. This idea is close to the one presented in this paper. Still, there are significant advances in the new technique proposed here. First, the original technique required to produce the full test suite. Every test was examined to check if it included a failing prefix. Our new incremental process does not generate the full test suite, it incrementally builds and filters the prefixes by alternating between unfolding and animation activities. Because we avoid the full unfolding of the test suite, we are able to consider test patterns corresponding to huge numbers of test cases (1918 in the last example). Another contribution of this paper is the definition of new constructs for test patterns (state predicates, behaviours, filtering keys), which help invalidate earlier the useless test cases in the unfolding process. Selection at generation time is another technique, where one selects a subset of the test suite based on some criterion. This selection takes place during the unfolding process and does not require to execute or animate test cases.

	Iteration Nb of tests	Nb of tests	Iteration Nb of tests	Nb of tests
		unfolded	accepted		unfolded	accepted
	1	19	3	10	1064	72
	2	57	7	11	1368	184
	3	133	29	12	3496	376
	4	551	24	13	7144	1160
	5	456	40	14	22040	64
	6	760	104	15	1216	80
	7	1976	312	16	1520	224
	8	5928	1136	17	4256	624
	9	21584	56	18	11856	640
		Fig. 7.
						, we have
	proposed two techniques to master combinatorial explosion with Tobias: test
	filtering at execution time, and test selection at generation time. Filtering at

http://smartesting.com

the original code of the application (in B and Java/JML) is available at http://membres-liglab.imag.fr/haddad/exemple site/index.html

The example presented in this paper follows the standard OCL syntax.

Tool website : http://www.yetitest.org/

http://www.globalplatform.org/specifications.asp

Acknowledgment This research is supported by the ANR TASCCC Project under grant ANR-09-SEGI-014.


Franck Lebeau
email: flebeau@femto-st.fr

Bruno Legeard
email: blegeard@femto-st.fr

Fabien Peureux
email: fpeureux@femto-st.fr

Alexandre Vernotte
email: avernott@femto-st.fr

Model-Based Vulnerability Testing for Web Applications

Keywords: Vulnerability testing, Model-Based Testing, Web applications, DVWA example

This paper deals with an original approach to automate Model-Based Vulnerability Testing (MBVT) for Web applications. Today, Model-Based Testing techniques are mostly used to address functional features. The adaptation of such techniques for vulnerability testing defines novel issues in this research domain. In this paper, we describe the principles of our approach, which is based on a mixed modelling of the application under test: the specification indeed captures some behavioral aspects of the Web application, and includes vulnerability test purposes to drive the test generation algorithm. Finally, this MBVT approach is illustrated with the widely-used DVWA example.

I. INTRODUCTION

The continued growth of Internet usage as well as the development of Web applications foreground the challenges of It security, particularly in terms of data confidentiality, data integrity and service availability. Thus, as stated in the annual barometer concerns of Information Technology Managers 1 , for 72% of them, computer security and data protection are their primary concerns. This growth of risk arises from the mozaic of technologies used in current Web applications (eg HTML5), which increases the risk of security breaches. This situation has led to significant growth in application-level vulnerabilities, with thousands of vulnerabilities detected and disclosed annually in public databases such as the MITRE CVE -Common Vulnerabilities and Exposures 2 . The most common vulnerabilities found on these databases especially emphasize the lack of resistance to code injection of the kind SQL Injection or Cross-Site Scripting (XSS), which have many variants. They appear in the top list of current web applications attacks. Application-level vulnerability testing is first performed by developers, but they often lack the sufficient in-depth knowledge in recent vulnerabilities and related exploits. This kind of tests can also be achieved by companies specialized in security testing, in pen-testing (for penetration testing) as instance. These companies monitor the constant discovery of such vulnerabilities, as well as the constant evolution of attack 1 Barometer CIO 2012, survey from the CSC institute, the 01 Informatique magazine and the BFM radio http://assets1.csc.com/fr/downloads/Barometre CIO 2012 Tout se transforme OK.pdf 2 Web site of MITRE CVE database -http://cve.mitre.org techniques. But they mainly use manual approaches, making the dissemination of their techniques very difficult, and the impact of this knowledge very low.

The work presented in this paper aims to automate vulnerability testing of Web applications, in order to extend the testing capability of these applications, increase the detection of such vulnerabilities and improve the overall level of security. The approach studied, based on model-based test generation techniques, aims to capture vulnerability test patterns in order to automate their implementation on Web applications.

The original contributions of this paper are:

• The consideration of the application's functional behaviour to generate vulnerability test cases, which allows for a more thorough exploration and testing of the Web application;

• The capture of Vulnerability Test Patterns as test purposes used to drive the test generation engine through models;

• The modelling activity dedicated to vulnerability testing that combines modelling of the system under test and modelling of the environment activities.

In the remainder of this paper, we first present our approach following the example of vulnerability testing of Cross-Site Scripting (XSS). We provide modelling material and test purposes in order to show how our test generation tool chain computes vulnerability test cases, that are executable on the target application. This presentation then relies on an experiment conducted on a Web application named DVWA -Damn Vulnerable Web Application -which is a demonstration application featuring typical vulnerabilities. Finally, we position this work in the state of the art and offer a conclusion and perspectives.

II. MODEL-BASED VULNERABILITY TESTING

We propose to revisit and adapt the traditional approach of Model-Based Testing (MBT) in order to generate vulnerability test cases for Web applications. This adapted approach is called Model-Based Vulnerability Testing (MBVT). In this section, we firstly describe the specificities of the MBVT approach. Secondly, we introduce the running example, named DVWA, used in the rest of the paper to illustrate the MBVT approach, and finally, we define the scope of the experiments conducted on this example.

A. Principles of the MBVT approach

MBT [START_REF] Utting | Practical Model-Based Testing -A tools approach[END_REF] is an increasingly widely-used approach that has gained much interest in recent years, from academic as well as industrial domain, especially by increasing and mastering test coverage, including support for certification, and by providing the degree of automation needed for shortening the testing execution time. MBT refers to a particular approach of software testing techniques in which both test cases and expected results are automatically derived from a high-level model of the System Under Test (SUT). This high-level model, which defines the input of the MBT process, specifies the behaviours of the functions offered by the SUT, independently of how these functions have been implemented. The generated test cases from such models allow to validate the behavioural aspects of the SUT by comparing back-to-back the results observed on the SUT with those specified by the model. MBT aims thus to ensure that the final product conforms to the initial functional requirements. It promises higher quality and conformance to the respective functional requirements, at a reduced cost, through increased coverage (especially about stimuli combination) and increased automation of the testing process [START_REF] Dias-Neto | A Picture from the Model-Based Testing Area: Concepts, Techniques, and Challenges[END_REF]. However, if this technique is used to cover the functional requirements specified in the behavioural model of the SUT, it is also limited to this scope, since what is not modeled will not be tested.

The use of MBT techniques to vulnerability testing requires to adapt both the modelling approach and the test generation computation. Within the traditional MBT process, which allows to generate functional test cases, positive test cases 3are computed to validate the SUT in regards to its functional requirements. Within vulnerability testing approach, negative test cases 4 have to be produced: typically, attack scenarios to obtain data from the SUT in an unauthorized manner. The proposed process, to perform vulnerability testing, is depicted in Figure 1. This process is composed of the four following activities:

① the Test Purposes activity consists in formalizing test purposes from vulnerability test patterns that the generated test cases have to cover;

② the Modelling activity aims to define a model that captures the behavioural aspects of the SUT in order to generate consistent (from a functional point of view) sequences of stimuli;

③ the Test Generation and Adaptation activity consists in automatically producing abstract test cases from the artefacts defined during the two previous activities;

④ the Concretization, Test Execution and Observation activity aims to (i) translate the generated abstract test cases into executable scripts, (ii) to execute these scripts on the SUT, (iii) to observe the SUT responses and to compare them to the expected results in order to assign the test verdict and automate the detection of vulnerabilities.

All these MBVT activities are supported by a dedicated toolchain, which is based on an existing MBT software named CertifyIt [START_REF] Bouquet | A test generation solution to automate software testing[END_REF] provided by the company Smartesting 5 .

This software is a test generator that takes as input a test model, written with a subset of UML (called UML4MBT [START_REF] Bouquet | A subset of precise UML for model-based testing[END_REF]), which captures the behaviour of the SUT. More concretely, a UML4MBT model consists of (i) UML class diagrams to represent the static view of the system (with classes, associations, enumerations, class attributes and operations), (ii) UML Object diagrams to list the concrete objects used to compute test cases and to define the initial state of the SUT, and (iii) state diagrams (annotated with OCL constraints) to specify the dynamic view of the SUT. Such UML4MBT models have a precise and unambiguous meaning, so that the of those models can be understood and computed by the CertifyIt technology. OCL expressions indeed provide the expected level of formalization necessary for MBT modelling. This precise meaning makes it possible to simulate the execution of the models and to automatically generate test cases by applying predefined coverage strategies. Each generated test case is typically an abstract sequence of high-level actions from the UML4MBT models. These generated test sequences contain the sequence of stimuli to be executed, but also the expected results (to perform the observation activity), obtained by resolving the associated OCL constraints.

Section III describes, in a detail manner, each of these activities and illustrate them using a running example, which is introduced in the next subsection.

B. Presentation of the DVWA example

In order to evaluate the effectiveness and efficiency of our approach, we have applied it on a Web application called DVWA 6 . The objective of this open-source Web application test bed, based on PHP/MySQL, is to provide an aid for security professionals, web developers and teachers/students to learn, improve, and test their skills in vulnerability discovery. It can also be used to test web security testing tools, like vulnerability scanners for instance.

DVWA embeds several vulnerabilities, notably vulnerabilities of the kind SQL Injection and Blind SQL Injection, and Reflected and Stored XSS. These vulnerabilities are commonly used to attack current Web applications 7 . Each vulnerability has a dedicated menu item leading to a dedicated page. DVWA also embeds three security levels: low, medium, and high. Each level carries different security protections: the lowest level has no protection at all, the medium level is a refined version but is still quite vulnerable, and the highest level is a properly secured version. Users can choose which level they want to work with by specifying it through the application. It is also possible to view and compare the source code of each security level.

C. Perimeter and objectives of experimentations

Our approach allows testing an application among the four types of attack mentioned earlier (Blind and Not Blind SQL Injection, Reflected/Stored XSS). To ease the understanding, we focus this presentation on the Reflected XSS attack (RXSS). It is one of the major breach because it is highly used and because its exploitation leads to severe risks (such as identity spoofing). An RXSS attack targets end-users. This kind of attack happens when a user input field is used by the server to produce a response sent back to a end-user. A pirate injects malicious data (such as a script, typically written in JavaScript, which will be executed by an end-user browser) in the Web application through a user input field. Lack of user input validations leads to unsecured applications. An XSS attack is either Reflected (the response containing malicious data is immediately produced and sent back to the end-user) or Stored (the malicious data is saved in the application's database, and retrieved later, in another context). Our presentation deals with vulnerabilities of the kind Reflected XSS. For each security level, our objective is to apply our MBVT approach in order to compute and execute test cases allowing discovery of RXSS vulnerabilities.

III. DETAILS OF OUR APPROACH

In this section, we detail each main activity of the MBVT process. For each activity, we present its objectives as well as its behaviours, and we use the DVWA example to illustrate our statements.

A. Formalizing Vulnerability Test Patterns into Test Purposes

Vulnerability Test Patterns (vTP) are the initial artefacts of our approach. A vTP expresses the testing needs and procedures allowing the identification of a particular breach in a Web application. There is as much vTP as types of application-level breaches. The ITEA2 Diamonds research project has already studied vTP, and provide a first definition as well as a first listing of vTP 8 . The characteristics of a Vulnerability Test Pattern are: its name, its description, its testing objectives (precising the addressed testing objectives), its prerequisites (precising the conditions and knowledges 7 These vulnerabilities appears in the top three most frequently used types of attack listed by the OWASP project -Open Web Application Security Project -cf www.owasp.org. 8 required for a right execution), its procedure (precising its modus operandi), its observations and its oracle (precising which information have to be prone in order to identify the presence of an application-level breach), its variants (precising some alternatives regarding the means in use, or the malicious data, or what is observed), its known issues (precising any limitation or problem (eg., technical) limiting its usage), its affiliated vTP (listing its correlated vTP), its references (to public resources dealing with application-level vulnerability issues, such as CVE, CWE, OWASP, CAPEC, ...). Figure 2 presents the Vulnerability Test Pattern of Reflected XSS attack.

For this vTP, variants of malicious data are defined during the modelling activity, variants of the procedure are defined during the adaptation and execution activity. The initial procedure is defined in a test purpose. A test purpose is a high level expression that formalizes a test intention linked to a testing objective to drive the automated test generation on the behavioural model. In the MBVT context, we propose to use test purposes to formalize vTP. We propose test purposes as a mean to drive the automated test generation. The test purpose language we are presenting is called Smartesting Test Purpose Language [START_REF] Botella | Model-based Testing of Cryptographic Components Lessons Learned from Experience[END_REF]. This is a textual language based on regular expressions [START_REF] Julliand | Generating security tests in addition to functional tests[END_REF], allowing the formalization of vulnerability test intention in terms of states to be reach and operations to be called. The language relies on combining keywords, to produce expressions that are both powerful and easy to read. Basically, a test purpose is a sequence of important stages to reach (last three lines in Figure 3). A stage is a set of operations or behaviour to use, or/and a state to reach. Transforming the sequence of stages into a complete test case, based on the model behaviour and constraints, is left to the MBT technology (more details comes in the section III-C). Furthermore, at the beginning of a test purpose, the test engineer can define iterators (three first lines in Figure 3). Iterators are used in stages, in order to introduce context variations. Each combination of possible values of iterators produces a specific test case. 2, applied on the DVWA case study. This schema precises that for all sensible web pages, for all malicious data enabling the detection of RXSS breach, and for all security levels of DVWA, it is required to do the followings: (i) use any operation to activate the sensible page with the required security level, (ii) inject the malicious data in all the user inputs of the page, (iii) check if the page is sensible to the RXSS attack. The three keywords ALL * are enumerations of values, defined by the security test engineer, allowing him/her to master the final amount of test cases.

We use a second test purpose, similar to the presented one, enabling to precisely target which user input fields have to be injected. This test purpose gives ways of control to the security engineer. Modifications are: (i) one added iterator targeting sensible fields, and (ii) the use of the operation injectField instead of the operation injectAllFields.

B. Modelling

The modelling activity produces a model based, on one hand, on the functional specifications of the application, and on the other hand on the test purposes which will be applied on it (keywords used in test purposes have to be modelled). We present in the following the used UML diagrams (classes, objects, state diagrams), and their respective usages in the context of our MBVT approach.

Class diagrams specify the static aspect of the model, by defining the abstract objects of the SUT. Class diagrams of our approach share many similarities with traditional MBT. Classes model business objects (notably, the SUT class models the system under test, and defines the points of control and observation). Associations model relations between business objects. Enumerations model sets of abstract values, and literals model each value. Class attributes model evolving characteristics of business objects. Class operations model points of control and observation of the SUT (we found here navigations between pages). Nevertheless, our MBVT approach differs from the traditional MBT by (see Figure 4):

• two additional classes (page and field) and their relations, which respectively model the general structure of the application and the user input fields potentially used to inject malicious data;

• some additional operations, coming from the test purposes, which model means to exercise and observe the attack

• one additional enumeration which model malicious data injected in user input fields. The UML object diagram models the initial state of the SUT, by instantiating class diagram elements. Thus, instances model business entities available at the initial state of the SUT, and links model relations between these entities. In our MBVT approach, the object diagram model the Web pages of the application and the user input fields of these pages. Note that: (i) the additional class User models the potential users of the application; (ii) class attributes message and security level respectively model application feedbacks and security level; (iii) the five first operations model the necessary and sufficient functional subset of the application allowing the access to the tested pages with the relevant level of security; (iv) operations injectAllFields and injectField, which are keywords coming from test purposes, model the injection of malicious data on all or part of the user input fields of Web pages; (v) operation checkMessage models the observation of the message attribute; operation checkRXSSAttack models the observation of the attack, and serves as oracle.

Example (DVWA):

Moreover, regarding the static aspect of the model, some enumeration literals model malicious data variants: RXSS DUMMY is a basic variant, RXSS COOKIE1 and RXSS COOKIE2 are two variants allowing to retrieve private user information, and RXSS WAF EVASION models a variant allowing to bypass some web application firewall techniques (see section III-D for their translation into concrete values).

Figure 6 presents the state diagram, which models the behaviour of DVWA. It defines precedences between pages: identification is required before reaching any other page of the application. Finally, Figure 7 presents the initial state of the DVWA model. It specifies: (i) one user, with its credentials, and (ii) the pages and user input fields of DVWA. The second phase produces the abstract test cases from the test targets. This phase is left to the test case generator. An abstract test case is a sequence of steps, where a step corresponds to a completely valued operation call. An operation call represents either a stimulation or an observation of the SUT. Each test target produces one test case (i) verifying the sequence of intermediate objectives and (ii) verifying the model constraints. Note that an intermediate objective (and hence, a test purpose stage) can be transformed into several steps. Figure 8 presents a test cases obtained from the test purpose of Figure 3. The five first steps of this test case correspond to the first stage of the test purpose.

Finally, the third phase exports the abstract test cases into the execution environment. In our case, it consist on (i) creating a JUnit test suite, where each abstract test case is exported as a JUnit test case, and (ii) creating an interface. This interface defines the prototype of each operation of the SUT. The implementation of these operations is in charge of the test automation engineer.

Example (DVWA):

We are using two test purposes and have defined four malicious data, in order to test one page with one user input field. Each test purpose produces 12 test targets, where each test target produces exactly one abstract test case, for a total amount of 24 abstract test cases. Figure 8 presents one of the generated abstract test cases. It has to be interpreted this way: (i) it logs in the application with valid credentials; (ii) it sets the security level; (iii) it loads the targeted Web page; (iv) it verifies the correct execution of the functional part of the test case (using the checkMessage observation); (v) it injects the malicious datum; (vi) it verifies if there exists an application-level breach or not (using the checkRXSSAttack observation). This last step assigns the verdict of the test case. Regarding the test purpose focusing on precise user input fields, test cases only differ at step #6, where the injectField operation replaces the injectAllFields operation.

D. Adaptation and test execution

During the modelling activity, each page, user input field, malicious datum, user credentials, etc. ... in summary, all data used by the application, are modelled in a abstract way. Hence, the test suite can't be executed as it is. The gap between abstract keywords used in abstract test cases and the real API of the SUT must be filled. To ease the understanding of our approach, we only present an adaptation of the kind 1↔1, but tables with multiple values are also used for a mapping of the kind 1↔*. Stimuli must also be adapted. When exporting the abstract test cases, the MBT tool provides an interface defining the signature of each operation. The test automation engineer is in charge to implement the automated execution of each operation of this interface. Because we are testing Web applications, we have studied two ways of automation:

• at the GUI level: we stimulate and observe the application via the client-side GUI of the application. Even if this technique is time consuming, it could be necessary when the client-side part of the application embeds JavaScript scripts. For this technique, we use the Selenium framework.

• at the HTTP level: we stimulate and observe the application via HTTP messages send to (and received from) the server-side application. This technique is extremely fast and can be used to bypass HTML and JavaScript limitations. For this technique, we are using the Apache HTTPClient Java library.

The last but not the least activity of the MBVT is to execute the adapted test cases in order to produce a verdict. We introduce a new terminology fitting the characteristics of a test execution:

• Attack-pass: the complete execution of the test reveals that the owns a breach, unlike in MBT where a complete execution of a test indicates a valid implementation;

• Attack-fail: the failure of the execution of the last step reveals that the application is robust to the attack, unlike MBT where such a failure indicates a invalid implementation;

• Inconclusive: in certain circumstances, it is not sure that a breach is discovered (eg., due to technical issues). An abnormal event happens, but no breach has been observed.

Example (DVWA):

The model defines four malicious data dedicated to Reflected XSS attacks. These values are defined in an abstract way, and must be adapted. Each of them is mapped to a concrete value: RXSS DUMMY ↔ <> RXSS COOKIE1 ↔ <script>alert(document.cookie)</script> RXSS COOKIE2 ↔ <img src="foo" onerror="javascript:alert(document.cookie)"/> RXSS WAF EVASION ↔ <scr<script>ipt>alert(document.cookie)</script> Operations of the SUT can be adapted in two ways: using Selenium or HTTPClient. However, we mainly use the HTTP-based approach (HTTPClient), because this techniques dramatically saves time on DVWA, for the same results. Based on the execution of the test suite, 50% of the test cases have been identified as Attack-pass: the two first malicious data with a low security level, the third malicious datum with the low and medium security level, and the fourth malicious datum with the medium security level. These results fit our manual experiments on DVWA. This concordance gives a first validation of our approach with regards to the addressed subset of vulnerabilities, and the DVWA context.

IV. STATE OF THE ART

The tool landscape in web application security testing is structured in two main classes of techniques: In practice these techniques are complementary, addressing different types of vulnerabilities. For example, SAST techniques are good to detect buffer overflow and other badly formatted string, but not so good to detect XSS or CSRF vulnerabilities. So, in this section, we focus on DAST techniques and provide a state of the art of emerging model-based security testing techniques.

Fuzzing techniques relate to the massive injection of invalid or atypical data (for example by randomly corrupting an XML file) generally by using a randomized approach [START_REF] Takanen | Fuzzing for Software Security Testing and Quality Assurance[END_REF]. Test execution results can therefore expose various invalid behaviours such as crash effects, failing built-in code assertions or memory leaks.

Web application vulnerability scanners aim to detect vulnerabilities by injecting attack vectors. These tools generally include three main components [START_REF] Bau | State of the Art: Automated Black-Box Web Application Vulnerability Testing[END_REF]: a crawler module to follow web links and URLs in the web application in order to retrieve injection points, an injection module which analyses web pages, input points to inject attack vectors (such as code injection), and an analysis module to determine possible vulnerabilities based on the system response after attack vector injection. As shown in a recent comprehensive study [START_REF]Web site on Price and Feature Comparison of Web Application Scanners[END_REF], corroborated by research papers [START_REF] Doupé | Why Johnny can't pentest: an analysis of black-box web vulnerability scanners[END_REF], [START_REF] Finifter | Exploring the relationship between web application development tools and security[END_REF] and confirmed by our own experience with tools such as IBM AppScan 9 , these tools suffer from two major weaknesses that highly decrease their practical usefulness:

• Limitations in application discovery As black-box web vulnerability scanners ignore any request that can change the state of the web application, they miss large parts of the application. Therefore, these tools test generally a small part of the web application due to the ignorance of the application behavioural "intelligence". Due to the growing complexity of the web applications, they have trouble dealing with specific issues such as infinite web sites with random URLbased session IDs or automated form submission.

• Generation of many false positive results The already-mentioned benchmark shows that a common drawback of these tools is the generation of false positives at a very important rate either for Reflected XSS, SQL injection or Remote File Inclusion vulnerabilities. The reason is that these tools use brute force mechanisms to fuzz the input data in order to trigger and establish a verdict by comparison to a reference execution trace. Therefore, they lack precision to assign the verdict, as they do not compute the topology of the web application to precisely know where to observe. These strong limitations of existing web vulnerability scanners lead to the key objectives of model-based vulnerability testing techniques: better accuracy in vulnerability detection, both by better covering the application (by capturing the behavioural intelligence) and by increasing the precision of the verdict assignment.

Model-based security testing are emerging techniques aiming to leverage model-based approaches for security testing [START_REF] Schieferdecker | Model-based security testing[END_REF]. This includes:

• Model-based test generation from security protocol, access-control or security-oriented models Various types of models of security aspects of the system under test have been considered as input to generate security test. For example, [START_REF] Dadeau | Mutation-Based Test Generation from Security Protocols in HLPSL[END_REF] proposes a method using security protocol mutation to infer security test cases. [START_REF] Jürjens | Model-based Security Testing Using UMLsec: A Case Study[END_REF] develops a model-based security test generation approach from security models in UMLSec. [START_REF] Buchler | Semi-Automatic Security Testing of Web Applications from a Secure Model[END_REF] presents a methodology to exploit a model describing a Web application at the browser level to guide a penetration tester in finding attacks based on logical vulnerabilities.

• Model-based fuzzing This approach applies fuzzing operator in conjunction with models; For example, [START_REF] Schneider | Model-based behavioural fuzzing[END_REF] proposes an approach that generates invalid message sequences instead of invalid input data by applying behavioural fuzzing operators to valid message sequences in form of UML sequence diagrams.

• Model-based test generation from weakness or attack models In these types of approaches, test cases are generated using threat, vulnerability or attacker models, which reflects the common steps needed to perform an attack, and the required associated data. For example, [START_REF] Wang | A threat model driven approach for security testing[END_REF], threats to security policies are modeled with UML sequence diagrams, allowing to extract event sequences that should not occur during the system execution.

Our approach allows to generate vulnerability tests from a model that mixes functional behavioural features of the system under test and aspects that model the possible attacks, which is modelling aspects of the environment of the system. Moreover, contrary to functional MBT, the test generation process is driven by the vulnerability test patterns, so that the behavioral model is restricted to the only elements that are needed to compute the vulnerability test cases.

V. CONCLUSION AND FUTURE WORKS

Web application vulnerabilities fall into two categories: Technical vulnerabilities include cross-site scripting, injection flaws and buffer overflows. Logical vulnerabilities relate to the logic of the application to get it to do things it was never intended to do. They often are the result of faulty application logic. Logical vulnerabilities are specific to the functionality of particular web applications, and, thus, they are extremely difficult to characterize and identify. For example, an important security breach have been discovered and disclosed in 2012 in the Paypal payment module of Magento10 eCommerce framework, due to the capability to falsify the payment amount after concluding the deal [START_REF]NBS System -Vulnerability in Magento's implementation of PayPal[END_REF]. This paper proposes a Model-Based Vulnerability Testing approach from a behavioral model and test patterns, which aims to address both technical and logical vulnerabilities. Technical vulnerabilities are managed by the composition of a navigational behavioral model and related test patterns; and logical vulnerabilities may be address through more complete modeling and adequate patterns. The main drawback of modelbased vulnerability testing echoes the one of MBT in general: the needed effort to design models, test purposes, and adapter. We are following several research directions to reduce this effort, which consist in identifying the reusability potential of the three artifacts from one project to another: test purposes can be made generic to their affiliated vulnerability type, model parts can be made generic to a web development framework (like Magento for e-commerce solutions) and also automatically generated, at least partially, using crawling techniques, and the adapter of those model parts can also be made generic to the associated framework. Therefore, our future work leads in two main research directions: (1) extending the method by covering more vulnerability classes, both technical (such as CSRF, file disclosure and file injection) and logical (such as the integrity of data over applications business processes). We will also study [START_REF] Dias-Neto | A Picture from the Model-Based Testing Area: Concepts, Techniques, and Challenges[END_REF] how the various MBVT artifacts may be made generic and reusable from one project to another project. In this context, we will focus on eCommerce applications, and more particularly eCommerce applications build on the top of the Magento framework. Indeed, eCommerce applications built with Magento have good properties because they rely to custom development and use of add-ons, both being wellknown to introduce security vulnerabilities.

Fig. 1 .

 1 Fig. 1. Model-Based Vulnerability Test process

Fig. 3 .

 3 Fig. 3. test Purpose formalizing the vTP of Figure 2 on DVWA

Fig. 5 .

 5 Fig. 5. Class diagram DVWA

Figure 5

 5 presents the class model of the DVWA example (Page and Field classes are not shown).

Fig. 4 .Fig. 7 .

 47 Fig. 4. Class diagram of the SUT structure, for our MBVT approach

Fig. 8 .

 8 Fig. 8. Abstract test case example

We call "positive test" a test case that checks whether a sequence of stimuli produces the expected effects with regards to the specifications. When a positive test is in success, it demonstrates that the tested scenario is implemented correctly.

By "negative test case" we define a test case targeting an unexpected use of the SUT. When a negative test case succeeds, it highlights a problem in the SUT.

http://www.smartesting.com

Damn Vulnerable Web Application -http://www.dvwa.co.uk/

See www.ibm.com/software/awdtools/appscan/

http://www.magentocommerce.com/

ACKNOWLEDGMENT

This work is supported by the French FSN project DAST (dast.deptinfo-st.univ-fcomte.fr) and the European ITEA2 project (http://www.itea2-diamonds.org).