Spécification et Validation d'un Contrôleur de Performances Sportives

Mohammed Al Achhab, Ahmed Hammad et Hassan Mountassir LIFC-Laboratoire d'Informatique de l'Université de Franche-Comté 16, route de Gray 25030 Besançon Cedex Email : {alachhab, hammad, mountass}@lifc.univ-fcomte.fr Abstract-Ce papier a pour objectif de montrer l'intérêt d'utiliser les méthodes formelles pour spécifier et valider un système médical, nous utilisons les automates hiérarchiques pour modéliser ces systèmes. La sémantique utilisée est celle d'une structure de Kripke où les états sont valués par des propositions atomiques. Cette structure peut être de grande taille en nombre d'états. Par nature, les systèmes hiérarchiques sont définis de manière hiérarchique par un ensemble de sous systèmes en éclatant à chaque fois un ou plusieurs états en un ensemble d'automates. Dans cet article, nous proposons de vérifier des proporiétés, seulement sur ces sous-systèmes. Pour pallier au problème de l'explosion combinatoire et la vérification de propriétés, nous considérons que les sous systèmes concernés par la propriété à vérifier et en déduire sa vérification sur le système global. Les résultats sont illustrés sur l'exemple d'un contrôleur de performances sportives.

I. MOTIVATIONS ET PROBLÉMATIQUE

Au cours de la dernière décennie, le développement de logiciels n'a pas cessée de croitree dans tous les domaines. En effet l'introduction de composantes informatiques s'avère de plus en plus importante dans les secteurs comme les systèmes de gestion pour l'aviation, les réseaux de téléecommunication, les banques, les systèmes de transport, les protocoles de paiement électronique et bien d'autres secteurs. L'être humain est et va de plus en plus être confronté à des exigences croissantes quant au bon fonctionnement de ces systèmes, et plus particulièrement pour les systèmes informatiques critiques. Nous qualifions de système critique, tout système dont les défaillances peuvent avoir des conséquences dramatiques et catastrophiques en termes humains ou économiques. Les systèmes de contrôle et les outils médicaux sont les systèmes critiques les plus répandus. Un exemple malheureux de système médical est la machine de radiation T HERAC25 [START_REF] Leveson | An investigation of the therac-25 accidents[END_REF], développée par la compagnie AECL 1 . Cette machine, utilisée entre 1985 et 1987 pour le traitement du cancer, permettait de détruire les tumeurs en émettant des radiations sur celles-ci sans affecter l'organe touché par la tumeur. Cependant, une anomalie dans son fonctionnement a entraîné la mort de 6 patients ; en effet, une erreur dans la programmation du logiciel conduisait dans certaines situations à utiliser erronément la machine dans un mode Rayon-X au lieu du mode faisceau d'électrons, ce qui envoyait 125 fois plus de radiations que dans la dose prescrite par le médecin. Ainsi, il est important de spécifier avec précision ces systèmes et par la suite 1 Atomic Energy of Canada Limited vérifier les propriétés exigées par l'utilisateur, afin d'assurer un développement fiable de tels systèmes, de réduire le coût de maintenance et de minimiser le risque de pertes économiques et humaines.

Notre travail s'articule autour de la spécification et la vérification de systèmes hiérarchique réactifs issus des travaux sur les StateCharts [START_REF] Harel | Statecharts : A Visual Formalism for Complex Systems[END_REF] et Unified Modeling Language (U M L) [START_REF] Booch | The Unified Modeling Language user guide[END_REF]. Nous utilisons les automates hiérarchiques [START_REF] Mikk | Hierarchical Automata as Model for Statecharts[END_REF] pour modéliser les systèmes hiérarchiques réactifs. Cette modélisation possède, en outre, des concepts tels que le raffinement d'états, des transitions qui ont plusieurs états de départ et plusieurs états d'arrivée (Interlevel Transitions), la priorité entre les transitions et l'exécution simultanée des transitions. Ces concepts rendent difficile l'utilisation directe de méthodes formelles.

Diverses méthodes et techniques ont été introduites afin d'effectuer la vérification de propriétés par model-checking sur les modèles hiérarchiques [START_REF] Latella | Automatic verification of a behavioural subset of uml statechart diagrams using the spin modelchecker[END_REF], [START_REF] Al'achhab | Vérification de systèmes hiérarchiques par raffinement[END_REF], [START_REF] Bhaduri | Model checking of statechart models : Survey and research directions[END_REF]. Dans [START_REF] Mikk | Implementing Statecharts in Promela/SPIN[END_REF], les auteurs montrent comment les StateCharts peuvent être traduits en P ROM ELA (le langage de spécification qu'utilise SP IN [START_REF] Holzmann | The model checker SPIN[END_REF]) en utilisant les automates hiérarchiques comme format intermédiaire. Les techniques de vérification utilisées sont algorithmiques et sont basées souvent sur la détection de cycles pour montrer la satisfaction ou non d'une propriété. Les propriétés sont exprimées à l'aide d'une logique comme la LT L (Linear Temporal Logic) [START_REF] Manna | The temporal logic of reactive and concurrent systems[END_REF]. Le principal problème réside dans la complexité des procédures de décision et l'explosion combinatoire du nombre d'états.

Dans ce papier, nous proposons d'utiliser la vérification par modules (ou modulaire) sur notre exemple. Cette méthode est utilisée pour vérifier les systèmes de grande taille. Il consiste à découper le modèle de système en un ensemble de modules et de vérifier si une propriété est satisfaite sur chaque module. La vérification de chaque module se fait d'une manière séparée et indépendante [START_REF] Masson | Modular verification for a class of PLTL properties[END_REF]. Le choix des propriétés à vérifier et la méthode de découpage sont deux points très importants, parce que ce n'est pas toujours vrai que : si une propriété est vérifiée sur tout les modules alors elle est satisfaite sur le modèle global du système. Cela découle de la manière de découper le modèle global en modules. Par nature, les automates hiérarchiques sont définis par des sous automates hiérarchiques.

Nous proposons des schémas de propriétés vérifiées sur chaque module du système et qui le sont sur le système global. Les modules du systèmes sont appelés sous structure de Kripke, notée SSK. Chaque sous structure de Kripke représente un aplatissement d'une partie de système représenté par un ensemble des automates associés à un état. La vérification des propriétés sera donc effectuée sur les sous structures de Kripke associées aux états raffinés par ces automates. Si les SSK vérifient la propriété ' alors la structure de Kripke globale, associée à l'automate hiérarchique global, la vérifie également. Cette méthode est appelée la vérification modulaire ou par parties.

La suite de ce papier est organisée en quatre sections. Dans la section deux, nous présentons les concepts de base : automate séquentiel et automate hiérarchique. Dans la section trois, nous présentons la sémantique d'automate hiérarchique sous forme de structure de Kripke. Dans la section quatre, nous présentons la démarche de vérification modulaire : définition de la partie à vérifier et schémas de propriétés. Dans la section cinq, nous traçons quelques perspectives à ce travail. Nous illustrons nos propos par un exemple de contrôleur de performances des sportives. On note χ l'application qui lie un état raffiné avec les états de l'automate fils. Nous définissons χ + comme la fermeture transitive non-réflexive, χ * comme la fermeture transitive réflexive de χ.

Proposition 1: Le décor de l'état fils implique celui de son ascendant : ∀s ∈ χ(s) =⇒ (L(s ) =⇒ L(s)).

Définition 2: (sous-automate hiérarchique) Soit AH = F, E, γ un automate hiérarchique, la restriction de la fonction de composition γ aux états d'un automate A ∈ F nous permet de définir le sous-automate hiérarchique

AH A = F A , E A , γ A telle que : F A = F \{A i |S Ai ∩ χ * (S A ) = ∅}, E A = E et γ A = γ|χ * (S A ) (On considère A comme l'automate racine de AH A ).

B. Exemple d'un contrôleur de performances sportives

Nous donnons un exemple de contrôleur de performances sportives des cyclistes, c'est un appareil d'entraînement basé sur un cardiofréquencemètre. Cet appareil permet d'enregistrer principalement les fréquences cardiaques d'un cycliste pendent ces entraînements. Il se compose d'un récepteur des signaux Ce système est conçu principalement pour enregistrer la fréquence cardiaque, la vitesse et la mesure de la pente. L'objectif est d'améliorer les performances des cyclistes en analysant ces données.

Au départ, le contrôleur est désactivé, dans cet état, il peut être soit en veuille, soit en maintenance. Dans l'état actif, l'athlète peut choisir soit le mode enregistrement des signaux, soit le mode consultation. Chaque attribut enregistré est composé de (vitesse, fréquence cardiaque et la mesure de pente). Dans le mode consultation, le cycliste peut choisir soit les statistiques, soit affichage des attributs.

La figure 1 représente un modèle simplifié, décrit par un automate hiérarchique.

L'automate hiérarchique AH = F, E, γ est composé de huit automates séquentiels Pour faciliter la lisibilité de SK nous avons dessiné qu'une partie des transitions définies par les règles de progrès et de composition, aussi nous avons donné que les noms des états des configurations.

F = {A 0 , A 1 , A 2 , A 3 , A 4 , A 5 , A 6 , A 7 } qui sont liés entre eux avec la fonction de composition γ = {s 0 -→ {A 1 }∧s 1 -→ {A 2 }∧ s 4 -→ {A 3 } ∧ s 5 -→ {A 4 } ∧ s 6 -→ {A 5 , A 6 , A 7 } ∪ {s -→ ∅|s ∈ {s 2 ,
-→ s 1 , s 4 Const -→ s 5 , s 6 M iseAjr -→ s 7 sont définies comme suit : -s 0 Start -→ s 1 def = s 0 {s 2 },Start,∅ -→ s 1 ; -s 4 Const -→ s 5 def = s 4 {s8},Const,∅ -→ s 5 ; -s 6 M iseAjr -→ s 7 def = s 6 {(s 1 2,s 1 4,s 1 6)},M iseAjr,∅ -→ s 7 .
-→ s ) ⇒ ¬activable (C|e) (t))) γ(s) = {A 1 , . . . A m } = ∅ A 1 :: C e -→ C 1 Am :: C e -→ C m A :: C e -→ {{s} ∪ C 1 ∪ • • • ∪ C m } -Règle

III. VÉRIFICATION DE PROPRIÉTÉS

Dans ce papier, nous nous intéressons à la vérification de propriétés exprimées en LT L sur les systèmes hiérarchiques. Pour faire face au problème d'explosion combinatoire dû à la complexité de ces systèmes, nous présentons une approche de vérification par modules pour éviter l'aplatissement de tout l'automate hiérarchique. Cette méthode est utilisée pour vérifier les systèmes de grande taille. Il consiste à découper le modèle de système en un ensemble de modules et de vérifier si une propriété est satisfaite sur chaque module. La vérification d'une propriété sur chaque module se fait d'une manière séparée et indépendante.

Le choix des propriétés à vérifier et la méthode de découpage sont deux points très importants, parce que ce n'est pas toujours vrai que : si une propriété ϕ est vérifiée sur tous les modules alors elle l'est sur le modèle global du système. Cela découle de la manière de découper le modèle global du système en modules.

Par nature, les automates hiérarchiques sont définis par des partitions des espaces d'états du système. C'est à dire, chaque état peut être décomposé en un un ensemble d'automates, cette décomposition définit un module. Nous appelons cette partie de système une sous structure de Kripke, notée SSK. Chaque sous structure de Kripke représente un aplatissement des automates fils associés à un état décomposé.

Un certain nombre de propriétés LT L ont pour particularité d'être satisfaites globalement lorsqu'elles sont satisfaites sur tous les modules du système. Ainsi, il faut s'assurer qu'une propriété est vérifiable modulairement avant de la vérifier de manière modulaire.

La vérification d'une propriété ϕ sera donc effectuée sur les sous structures de Kripke. Si les SSK vérifient la propriété ϕ alors la structure de Kripke globale, associée à l'automate hiérarchique, la vérifie également. Cette méthode est appelée la vérification modulaire ou par parties. Formellement, pour tout état s raffiné, si SSK s |= ϕ alors SK |= ϕ.

Avant de définir les schémas de propriétés qui peuvent être vérifiées d'une manière modulaire, nous commençons par définir l'ensemble des sous structures de Kripke associées à un automate hiérarchique.

A. L'ensemble des modules de AH

Soient AH = F, E, γ un automate hiérarchique. Soit SK = Conf, C 0 , -→ K , E, LK la structure de Kripke associée à AH. Soit S r l'ensemble des états raffinés (c'est à dire : un état s ∈ S r si γ(s) = ∅). Nous associons à chaque état s de S r une sous structure de Kripke, notée SSK s , de la structure de Kripke globale SK.

La sous structure de Kripke SSK s représente l'aplatissement des automates fils de l'état s ∈ S r et les transitions sortantes de s appartenant aux automates ancêtres de s.

Définition 6: (Sous strucure de Kripke) Soit s un état de S r , la sous structure de Kripke SSK s = Conf s , C 0s , -→ Ks , E, LK associée à l'état s est définie comme suit :

- -

σ(i) |= p si et seulement si p ∈ LK(C i ), -σ(i) |= ¬ϕ si et seulement si il n'est pas vrai que σ(i) |= ϕ, -σ(i) |= ϕ 1 ∧ϕ 2 si et seulement si σ(i) |= ϕ 1 ∧σ(i) |= ϕ 1 , -σ(i) |= ϕ si et seulement si σ(i + 1) |= ϕ, -σ(i) |= ϕ 1 Uϕ 2 si et seulement si ∃k.(k ≥ i ∧ σ(k) |= ϕ 2 ∧ ∀j.(i ≤ j < k ⇒ σ(j) |= ϕ 1 )
). Les autres opérateurs temporels se redéfinissent comme suit : ♦ϕ peut être redéfini par true U ϕ, ϕ peut être redéfini par ¬♦¬ϕ, ϕ 1 ⇒ ϕ 2 redéfini par ¬ϕ 1 ∨ ϕ 2 .

2) Schémas de propriétés: Soient AH = F, E, γ un automate hiérarchique, SK la structure de Kripke associée à AH, S r l'ensemble des états raffinés et M l'ensembe des modules de AH. Soient s un état de S r , p et q deux propositions exprimées sur AP .

Dans le théorème suivant, nous énonçons des schémas de propriétés vérifiables modulairement.

Théorème 3.1: Soit ϕ une formule LT L de type p, (p ⇒ ♦q) et (p ⇒ p U q). Si toutes les sous structures de Kripke SSK de M satisfont ϕ alors SK satisfait ϕ.

Preuve du théorème 3.

toute SSK ∈ M, si SSK |= (p ⇒ ♦q) alors SK |= (p ⇒ ♦q).
Nous avons SSK |= (p ⇒ ♦q), alors ∀σ ∈ Σ(SSK) et 2 Pour plus de détails sur la logique LT L, voir [START_REF] Manna | The temporal logic of reactive and concurrent systems[END_REF], [START_REF] Pnueli | The temporal semantics of concurrent programs[END_REF] ∀i.(i ≥ 0 ∧ σ(i) |= p ∧ σ(j) j>i |= ♦q). Pour chaque SSK s , toutes les transitions sortantes de l'état s (transitions prioritaires) sont dans SSK s , donc chaque chemin d'exécution de SSK s est un morceau de chemin de SK, alors les configurations satisfont q seront dans le chemin d'exécution de SK. Donc, si chaque SSK vérifie (p ⇒ ♦q), alors SK la vérifie également.

IV. CONCLUSION ET PERSPECTIVES

Dans ce papier nous nous sommes intéressés à la vérification de systèmes hiérarchiques, qui proviennent du domaine médical, en l'occurence un contrôleur de performances sportives. Pour faire face au problème d'explosion combinatoire dû à la complexité de ces systèmes, nous présentons une approche de vérification par modules (sous-structures) pour éviter l'aplatissement de tout l'automate hiérarchique. Cette méthode est utilisée pour vérifier les systèmes de grande taille. Il consiste à découper le modèle de système en un ensemble de modules et de vérifier si une propriété est satisfaite sur chaque module. La vérification d'une propriété sur chaque module se fait d'une manière séparée et indépendante.

Nous travaillons actuellement pour étendre ces schémas de propriétés car notre objectif est d'exploiter la notion d'hiérarchie pour utiliser le moins possible la technique du modelchecking ou éventuellement l'utiliser sur des sous modèles de taille raisonnable.

  A. Automate hiérarchique Un automate hiérarchique, noté AH, est un ensemble d'automates qui sont liés entre eux par une fonction de composition. La fonction de composition fait le lien entre un état s d'un automate séquentiel (état père) et un ensemble d'automates (automates fils). Définition 1: (automate hiérarchique) AH est défini par le 3-uplet F, E, γ , où : F = {A 1 , . . . A n } est un ensemble d'automates ayant un ensemble d'états distincts, E = ∪ A∈F Σ A est un alphabet fini de noms d'actions et γ : A∈F S A -→ 2 F est une fonction de composition sur F tel que : dans l'ensemble F il y a un seul automate racine A racine , chaque automate A ∈ F \{A racine } a un état père et la fonction de composition ne doit pas contenir de cycles : ∀S ⊆ A∈F S A .∃s ∈ S.S ∩ A∈γ(s) S A = ∅.

Fig. 1 .

 1 Fig. 1. Exemple de AH

Cas 3 :

 3 Pour toute SSK ∈ M, si SSK |= (p ⇒ p U q) alors SK |= (p ⇒ p U q). SSK |= (p ⇒ p U q) alors ∀σ.(σ ∈ Σ(SSK) ⇒ σ |= (p ⇒ p U q)). Par définition de la LT L ∀i.(i ≥ 0 ∧ σ(i) |= p) et ∃k.(k ≥ i ∧ σ(k) |= q ∧ ∀j.(i ≤ j < k ⇒ σ(j) |= p)). Pour chaque SSK s ,toutes les transitions sortantes de l'état s sont dans SSK s , donc chaque chemin d'exécution de SSK s est un morceau de chemin SK. D'après la proposition 1, les états fils des états raffinés dans σ(i) vérifiont aussi p. Donc, si les SSK satisfont (p ⇒ p U q), alors nous concluons que la propriété est vérifiée sur SK. Nous donnons quelques exemples de propriétés vérifiables modulairement et par le système global. Dans le cas 2, "Au départ, le contrôleur est inactif, il devient actif plus tard". Dans le cas 3, "Le contrôleur continue à enregistrer les performances d'un sportif pour qu'elles soient consultées ultérieurement".

  s 3 , s 7 , s 8 , s 9 , s 10 , s 11 , s 12 , s 13 , s 14 , s 15 , s 16 }}}. Nous avons χ(s 0 ) = {s 2 , s 3 }.II. SÉMANTIQUE DES AUTOMATES HIÉRARCHIQUESDans cette section, nous décrivons la sémantique de l'automate hiérarchique définie comme une structure de Kripke. Cette présentation nous permet de vérifier les systèmes hiérarchiques à nombre fini d'états par model-checking. Une structure de Kripke est définie par un ensemble de configurations reliées par une relation de transition. Nous commençons par définir la notion de configuration, étiquetage des transitions dans AH et transition activable. (configuration) Soit S t = ∪ A∈F S A l'ensemble des états de AH = F, E, γ et soit C un ensemble d'états dans S t . C est une configuration si : -l'automate racine participe par un seul état à la configuration C : ∃!s.(s ∈ S A racine ∧ s ∈ C) et -la fermeture en bas : pour chaque état s dans C si s est raffiné par un automate A, alors, A participe aussi par un seul état à C : ∀s, A.(s ∈ C ∧ A ∈ γ(s) ⇒ ∃!s .(s ∈ S A ∧ s ∈ C)) Dans l'automate hiérarchique de la figure 1, les ensembles (s 0 , s 2 ), (s 0 , s 3 ), (s 1 , s 5 , s 9 ), (s 1 , s 4 , s 6 , s 11 , s 13 , s 15 ), (s 1 , s 4 , s 7 ) et (s 1 , s 4 , s 8 ) sont des configurations. (s 0 , s 2 ) est la configuration initiale. On note Conf A l'ensemble des configurations de l'automate hiérarchique AH A où A est l'automate racine de AH A .B. L'étiquetage des transitions dans un automate hiérarchiquePour représenter les diagrammes StateCharts à l'aide des automates hiérarchiques, Mikk et al[START_REF] Mikk | Hierarchical Automata as Model for Statecharts[END_REF] ont ajouté deux gardes, sr(source restriction) et td(target determinator) aux transitions d'automates séquentiels. L'objectif est de préserver les informations des transitions qui ont plusieurs états de départ et plusieurs états d'arrivée (Interlevel T ransitions). F est défini par le triplet (sr, a, td) tel que : source(t) = s est la source de la transition, but(t) = s est l'état d'arrivée de la transition t, action(t) = a est l'action de t, sr est employée pour déterminer dans quelles configurations t est activable, et td est employée pour déterminer les états d'arrivée de la transition t. Dans la figure 1, les transitions s 0

	A. Configuration
	Une configuration d'un automate hiérarchique permet de
	décrire l'état global de celui-ci à un instant précis.
	Définition 3: Start

Soit AH = F, E, γ un automate hiérarchique. L'étiquetage d'une transition t def = s -→ s dans un automate A ∈

  Soient s et s deux états d'un automate A ∈ F et t → s une transition dans A. Si s est raffiné par un ou plusieurs automates et sr = ∅, alors, t est activable de n'importe quel état des automates fils de s. Si s est raffiné par un ou plusieurs automates et td = ∅, alors, les états d'arrivée de t sont les états initiaux des automates fils de s . Enreg -→ s 4 sont activables à partire de tout les états des automates fils. 1) Ensemble de transitions sans conflit: Soit AH = F, E, γ un automate hiérarchique, A un automate dans F , C une configuration dans Conf A et a une action dans E. On dit que la transition t → s de l'automate A est activable à partir de la configuration C, notée activable (C|t) , si l'état s est dans la configuration C et C est une configuration dans sr ou sr = ∅. Soient t 1 et t 2 deux transitions activables à partir de C|e. On dit que t 2 est prioritaire par rapport à t 1 si : (source(t 1 ) ∈ χ + (source(t 2 ))). Définition 4: (ensemble de transitions activables sans conflit) Soit ET (C|e) l'ensemble des transitions étiquetées par l'ensemble des actions e ⊆ E activables à partir de la configuration C. On appelle trs ⊆ ET (C|e) l'ensemble maximal des transitions sans conflit activables à partir de C|e si : (1) ∀A ∈ F.(|trs∩ -→ A | ≤ 1) (chaque automate participe au plus avec une seule transition) (2) ∀t ∈ ET (C|e) .(t ∈ trs) s'il n'y a pas de transition t ∈ ET (C|e) avec une priorité élevée. Dans la figure 1, si la configuration actuelle est {s 1 , s 5 , s 9 } et l'ensemble des actions à exécuter est {Stop, Enreg, Stat}), alors l'ensemble des transitions activables est {(s 1 (structure de Kripke) La sémantique de AH est une structure de Kripke SK = Conf, C 0 , -→

				def = s	sr, a, td
					Stop -→
				s 0 ), (s 5 transitions sans conflit est {(s 1 Enreg -→ s 4 ), (s 9 Stat -→ s 10 )} et l'ensemble maximal des Stop -→ s 0 )}.
				2) Structure de Kripke:
	s	sr,a,td	def =	Définition 5: {s} = C ∩ S A ∀t.(t ∈-→ A .(t = (s sr,a,td

-Dans l'exemple, les transitions s 1 Stopt -→ s 0 et s 5 -K , E, LK où : -Conf est l'ensemble des configurations de AH, -C 0 est la configuration initiale, -E est l'ensemble d'actions, -LK : Conf -→ 2 AP telle que LK(C) = ∪ si∈C L(s i ), --→ K ⊆ Conf ×2 E ×Conf est la relation des transitions de SK. Une transition t ∈-→ K est un ensemble de transitions sans conflit définie par les règles suivantes : -Règle de progrès : Cette règle s'applique à un automate A si un de ses états s est dans la configuration C et si l'une des transitions partante de s est activables alors une de ces transitions a lieu. {s} = C ∩ S A ∃t ∈-→ A .(activable (C|e) (t)) ∧ t = (s sr,a,td -→ s ) A :: C e -→ ({s } ∪ td) -Règle de composition : Cette règle explique comment un automate délègue sa transition à ses automates fils : elle s'applique à un automate A ayant un état s dans la configuration C tel que toutes les transitions partantes de s ne sont pas activables et l'état s est raffiné par un ou plusieurs automates. Les automates fils peuvent exécuter leurs transitions.

  de bégaiement : Cette règle est appliquée à un automate A ayant un état s dans la configuration C mais toutes les transitions partantes de s ne sont pas activables et s n'est pas raffiné par un autre automate. . . . . La séquence de configurations σ = C 0 , C 1 , . . . C i . . . définie un chemin d'exécution de SK. On note Σ(SK) l'ensemble des chemin d'exécution de SK. La structure de Kripke SK associée à l'automate hiérarchique AH de la figure1 est représentée dans la figure 2.

								{s} = C ∩ S A
									Basic(s)
			∀t ∈-→ A .(t = (s	sr,a,td -→ s )) ⇒ ¬activable (C|e) (t)
	A :: C Une exécution de SK est une séquence finie ou infinie de e -→ {s} configurations et de noms d'actions de la forme : C 0 e 1 -→ C 1 e 2 -→ • • • e i -→ C i e i+1 Stop S0, S3 In -→ Start Out
		S0,S2				S1,S4,S6,S11,S13,S15
	Stop	Stop	Stop	Stop	Stop	EnV			EnFC	EnPente
					S1,S4,S6,S12,S13,S15	S1,S4,S6,S11,S14,S15	S1,S4,S6,S11,S13,S16
		Enreg			EnPente	EnFC		EnV	EnPente	EnFC	EnV
							S1,S4,S6,S12,S14,S15	S1,S4,S6,S11,S14,S16
	Suivt	Pres	Enreg						S1,S4,S6,S12,S13,S16
	S1,S5,S9					EnFC	S1,S4,S6,S12,S14,S16 EnFC	EnV
	Stat	Aff							MiseAjr
					Const				AttSign
	S1,S5,S10							S1,S4,S7
									Enrg
									S1,S4,S8
									S9
					Fig. 2. SK associée à AH

  Conf s est un sous ensemble de configurations de SK, telle que : C est une configuration dans Conf s si C est une configuration des automates fils de s ou C est une configuration cible d'une transition sortante de s ; -C 0s est la configuration initiale tels que tous les états initiaux des automates fils de s appartiennent à C 0s ; -E 2 est l'ensemble d'actions ; -LK 2 : Conf s -→ 2 AP V est la fonction de décor des configurations ; --→ Ks ⊆-→ K2 est la relation de transitions de SSK s . -→ Ks est un sous ensemble de la relation -→ K2 . t C j est une transition dans -→ Ks si et seulementsi : t ∈-→ K2 , C i ∈ Conf s et C j ∈ Conf s .Les sous structures de Kripke SSK s1 et SSK s4 associées aux états s 1 et s 4 de l'automate hiérarchique AH de la figure1sont représentées dans la figure3. Fig. 3. Les sous structures de Kripke SSKs 1 et SSKs 4La sous structure de Kripke SSK s 1 se compose de trois configurations et quatre transitions. Les transitions étiquetées par l'actions Stop sont des transitions de l'automate ancêtre A 0 , sortantes de l'état s 1 .Définition 7: (L'ensemble des modules de AH) Soient AH = F, E, γ un automate hiérarchique. A racine l'automate racine de AH. Soit S r l'ensemble des états raffinés. Nous appellons M l'ensemble des modules de AH si :-l'automate racine appartient à M, -pour chaque état s de S r il existe une sous structure de Kripke SSK s associée à s dans M. L'ensembe des modules de l'automate hiérarchique de la figure1est défini par six sous structure de Kripke : SSK racine , SSK s 0 , SSK s 1 , SSK s 4 , SSK s 5 et SSK s 6 . SSK s1 et SSK s4 sont représentées dans la figure 3, les autres sous structure de Kripke sont représentées dans la figure 4. Nous proposons dans cette section quatre patterns de propriétés qui peuvent être vérifiées d'une manière modulaire. Nous commençons par rappeler la définition de la logique LT L. 1) Logique temporelle linéaire: Soit p une proposition atomique de l'ensemble AP . Une formule temporelle ϕ de LT L 2 est définie par la grammaire suivante : ϕ ::= p|¬ϕ|ϕ ∧ ϕ| ϕ|ϕUϕ Soient ϕ, ϕ 1 , ϕ 2 des formules temporelles. Soit σ = C 0 , C 1 , . . . C i , . . . un chemin d'exécution d'une structure de Kripke SK. Nous définissons que "ϕ est satisfaite à la configuration C i i≥0 de l'exécution σ", noté σ(i) |= ϕ, comme suit :

	def = C i -→ Const a Enreg Actif,Enregistrement,Signaux Const Actif,Consultation Stop SSK(S1) Actif,Enregistrement,Aff_Ecran Stop Stop Actif,Enregistrement,Enregist MiseAjr Enrg Stop SSK(S4) Start S1,S4,S6,S11,S13,S15 EnV EnFC S1,S4,S6,S12,S13,S15 S1,S4,S6,S11,S13,S16 S1,S4,S6,S11,S14,S15 EnFC EnV EnPente EnFC S1,S4,S6,S12,S14,S15 S1,S4,S6,S11,S14,S16 S1,S4,S6,S12,S13,S16 EnV EnFC EnV S1,S4,S6,S12,S14,S16 EnPente Stop MiseAjr S1,S4,S7 Enrg AttSign Aff Stop S0,S2 Pres Desactif,Veuil Suivt S1,S5,S9 S1,S5,S10 Stat EnPente Enreg Stop Stop Const Out In S0, S3 Stop Enreg SSK S0 SSK racine SSK S5 SSK S6 Actif,Enregistrement Actif,Consultation Desactif,Veuil B. Schémas de propriétés
	S1,S4,S8
	Fig. 4. Les sous structures de Kripke de l'automate hiérarchique de la figure
	1

  Pour toute SSK ∈ M, si SSK |= p alors SK |= p. SK est définie par l'ensemble des configurations de SSK, c'est à dire, dans SK il n'y a pas une configuration C qui n'appartient pas à une sous structure de Kripke de M. Nous avons SSK |= p, d'après la sémantique de la LT L toutes les configurations de SSK satisfont p. Comme SK est définie par l'ensemble des configurations de SSK alors SK |= p.

	1 :
	Cas 1 :
	Cas 2 :
	Pour


Sékou Diakité

Jean-Marc Nicod

Laurent Philippe

Comparison of Batch Scheduling for Identical Multi-Tasks Jobs on Heterogeneous Platforms

Keywords: Batch scheduling, grid computing, heterogeneous platform, on-line scheduling, steady state scheduling, genetic algorithm

In this paper we consider the scheduling of a batch of the same job on a heterogeneous execution platform. A job is represented by a directed acyclic graph without forks (intree) but with typed tasks. The execution resources are distributed and each resource can carry out a set of task types. The objective function is to minimize the makespan of the batch execution. Three algorithms are studied in this context: an online algorithm, a genetic algorithm and a steady-state algorithm. The contribution of this paper is on the experimental analysis of these algorithms and on their adaptation to the context. We show that their performances depend on the size of the batch and on the characteristics of the execution platform.

I. INTRODUCTION

In this paper we are interested in scheduling one batch of identical jobs on a heterogeneous computing grid. Each job of the batch is an application described by a Directed Acyclic Graph (DAG) without forks (intree) and executed independently from the others jobs. The originality of the work is that each host is able to perform only a subset of the application tasks but several hosts are able to carry out the same task. An example is a work-flow to process a set of data in several steps -each step could be a filter applied to an image-on a grid where the softwares installed on the hosts differs -only some filters are available on a host. Our objective is to minimize the makespan of the batch execution, but, as there is no direct optimal solution to the problem, we evaluate different solutions by simulating them.

In this context, the main contribution of this paper is the comparison of three scheduling techniques for medium sized batches: a simple on-line scheduler, a steady-state scheduling technique and a standard heuristic based algorithm, designed for DAG scheduling. We also show that the platform architecture may affect the performances of the schedule.

The organization of the paper as follow. The second section gives a formal definition of the context and of the scheduling problem. The third section is dedicated to the related works. Then, in the forth section, we select three algorithms and we explain how we adapt them to our context. The algorithms comparison is done experimentally, so the simulation implementation is described in the fifth section. The results and the comments on the different scheduling techniques are given in the sixth section, before the conclusion.

LIFC/ INRIA GRAAL, 16 route de Gray 25000 Besanc ¸on, France, [diakite,nicod,philippe]@lifc.univ-fcomte.fr

II. CONTEXT DEFINITION

The platform is composed by a set of processors which communicate through network links. It is represented by an undirected graph: P F = (P, L), where the vertices are the n processors p i (p i ∈ P : i ∈ [1..n], n = |P |) and the edges are the network links l i between these processors.

On this platform, we execute one batch of identical jobs. A batch B of length m is defined as a set of m identical instances J j of the job J such as B = {J j : j ∈ [1..m]}. The job J is composed of several tasks with dependency constraints and is represented by a DAG: J = (T, D) where the vertices T are the tasks T k and the edges D are the dependency constraints between the tasks. Note that there will be several instances of task T k belonging to different instances J j of job J.

Tasks cannot be executed on every processor. Each processor P i implements a limited set of functions (libraries) to carry out the tasks. We define the set of function F i as the set of tasks T k that the processor P i is able to perform. Let F be the set of all the functions used by the job J thus ∪ i F i = F where i ∈ [1..N ]. The time T needed to execute a task T k on different processors P i is not uniform: T (T k , P i ) = T (T k , P ′ i ). The targeted applications on the grid are very time consuming. For this reason, we make the assumption that the bandwidth of P F allows us to neglect the communication time for all the computation steps of each instance J i of the job J.

According to the α|β|γ [START_REF] Graham | Optimization and approximation in deterministic sequencing and scheduling: a survey[END_REF] classification of scheduling problems, this problem is defined by U r |batch of intrees|C max : the platform is heterogeneous thus the execution times are unrelated and we optimize the makespan C max of a batch of intree. Finding an optimal schedule for a batch of jobs on a heterogeneous platform with limited resources is known to be an NP-complete problem, so there is no direct method. Two solutions may be used: either use a heuristic to compute a suboptimal schedule or use the results of an optimal solution to a problem close to ours.

III. RELATED WORKS

Three approaches match this context. Steady-state techniques achieve an optimal use of the resources for an infinite number of identical jobs [START_REF] Beaumont | Assessing the impact and limits of steady-state scheduling for mixed task and data parallelism on heterogeneous platforms[END_REF]. The resulting schedule is composed of an initialization stage before entering in steady-state where it becomes optimal. This result will tend towards optimality when the size of the batch increases, as the weight of the initialization stage decreases in the global schedule. When the size of the batch is too small, the initialization stage overhead leads however to an inefficient schedule. So, the question is "from what batch size steady-state scheduling becomes interesting?".

Classical solutions to optimize the makespan of a set of tasks relay on heuristics such as Earliest Finish Time [START_REF] Topcuouglu | Performance-effective and lowcomplexity task scheduling for heterogeneous computing[END_REF] or Critical Path [START_REF] Kwok | Dynamic critical-path scheduling: An effective technique for allocating task graphs to multi-processors[END_REF]. These heuristics approaches compute a schedule off-line with the assumption that no other jobs will be run on the platform. These techniques schedule the whole set of tasks, so they do not suffer from the initialization problem. However, if the number of tasks scales up, the computation time becomes too long due to the complexity of the algorithm.

On-line oriented techniques generate the schedule during the jobs execution. They take the state of the system into account to assign new tasks to processors. These techniques are very easy to implement and give rather good results. They give however no guarantee on the optimality of the schedule.

Other works exist on scheduling multiple DAGs. Most of them describe real-time schedulers for periodic tasks [START_REF] Li | Hierarchical scheduling and allocation of multirate systems on heterogeneous multiprocessors[END_REF], [START_REF] Qin | A dynamic and reliability-driven scheduling algorithm for parallel real-time jobs executing on heterogeneous clusters[END_REF]. Real-time schedulers are not adapted to our context because their objectives is to ensure that the tasks deadlines are met. Iverson and Özgüner [START_REF] Iverson | Dynamic, competitive scheduling of multiple dags in a distributed heterogeneous environment[END_REF] use a different technique where multiple DAGs compete for the available computational resources. In the paper, schedulers have limited informations on processors and no informations on future jobs to schedule. This is not the case in our context where a centralized entity schedules all the jobs.

IV. SELECTED SOLUTIONS

In this section we present the selected algorithms and their adaptation to the context characteristics. represents one of the three possible approaches and provide good results in our context. The first algorithm is a static scheduling algorithms for graphs of aperiodic tasks on a heterogeneous platform. It allows us to evaluate the performances of an algorithm designed for a set of tasks to schedule middle size batches of jobs. The second algorithm is a simple listbased on-line scheduling algorithm that we use to obtain a reference makespan. The third algorithm is a steady-state oriented scheduling algorithm. This algorithm uses a linear program to optimize the number of jobs executed per time unit in steady-state, and produces an optimal schedule [START_REF] Beaumont | Assessing the impact and limits of steady-state scheduling for mixed task and data parallelism on heterogeneous platforms[END_REF]. It allows us to evaluate the performance of an optimal steadystate algorithm, designed for an unlimited number of jobs, in the context of middle sized batch.

A. GATS

Genetic Algorithm for Task Scheduling (GATS) is a genetic algorithm that produces 7% to 10% shorter schedule than classical scheduling techniques for aperiodic tasks on a heterogeneous platform [START_REF] Daoud | Gats 1.0: A novel ga-based scheduling algorithm for task scheduling on heterogeneous processor nets[END_REF]. It uses the genetic metaheuristic to enhance the schedule obtained by a list-based scheduling heuristic. The first step is to create an initial population: the first individual represents the result of a list-based schedule which favors the tasks on the critical path of J. Then one individual per processor represents a random schedule where all the tasks are affected to the given processor and the remain of the population represents random schedules. GATS individuals do not represent total schedules but only processors-tasks associations. A decoding step translates each individual to a schedule that respects all the dependencies. The decoded schedule is used to compute the fitness f of an individual as: f = 1/Makespan(schedule). The representation without time informations allows fast computations of mutations and cross-overs since tasks are directly movable from one slot to another. Once the initial population is created, GATS performs a loop that computes the fitnesses of the individuals, a rank-based selection, mutations and cross-overs until the termination criteria are met. The termination criterion used is a fixed number of loops. The computed schedule is at least equal to the initial list-based solution.

The original GATS algorithm is not designed to schedule multiple instances of the same job. One simple method to make GATS able to solve this problem is to schedule all the job instances as a single job. This method increases however the time and the physical memory necessary for GATS to compute the schedule. So we use a hybrid method that schedules the tasks in successive intervals of x jobs and appends the set schedules.

B. On-line Scheduling with knowledge

Algorithm 1 onlineScheduler(processors, job, count) job ← job multiply(job, count) while not isEmpty(job) do f ree ← update f ree list(job, f ree) T best ← remove f irst(f ree) P best ← smallest EF T (processors, T best ) send(T best , P best ) if isEmpty(f ree) then W ait f or a task to be f ree end if W ait f or a processor to be idle end while

The algorithm 1 is a simple implementation of an on-line scheduler. When the on-line scheduler is asked to execute count jobs, it creates a single job (job) that groups the count jobs to be scheduled. The algorithm manages a f ree tasks list that contains tasks with no dependency. At each loop of the algorithm, the first task of the list is selected to be scheduled. This algorithm does not use a heuristic to select the task to schedule contrary to other list based scheduling algorithms [START_REF] Topcuouglu | Performance-effective and lowcomplexity task scheduling for heterogeneous computing[END_REF], [START_REF] Wu | Segmented min-min: A static mapping algorithm for meta-tasks on heterogeneous computing systems[END_REF]. This mechanism shortens the traversal time of a job. T best is used to select the best processor (P best ) using the Earliest Finish Time (EFT) heuristic [START_REF] Topcuouglu | Performance-effective and lowcomplexity task scheduling for heterogeneous computing[END_REF]. The selected task is sent to the selected processor then the algorithm waits for, at least, one free task and one idle processor, until all the jobs are carried out.

C. Steady-state scheduling

The steady-state scheduling technique uses a linear program to compute an optimal schedule when the system enters a steady-state. The objective function of the linear program is to maximize the number of jobs computed per time unit. The constraints of the linear program force the solution to respect the computation abilities of each processor. These constraints also ensure that jobs are fully computed.

The solution of this linear program gives the ratio of time spent by each processor for each task of the jobs and the proportion of time spent by each network link to send task results for each inter-tasks dependencies. As the execution context is a steady-state, the proportion can be computed as a rational number. This solution is translated into a weighted sum of allocation, where an allocation represents the traversal of a job in the platform (task/processor associations). The steadystate scheduling computes a period in which the allocations are interleaved according to their weight. The steady-state stage is the concatenation of the adequate number of these periods to compute the number of desired jobs.

The scheduling needs an initialization stage before entering in steady-state and a termination stage to finish after the last period. The initialization stage computes every task needed to enter into the steady-state stage. In the original algorithm, the initialization is not optimized. The master computes itself every tasks without parallelism facility. As the initialization, the termination stage is performed by the master in a sequential way. Its role is to terminate every task staying in the platform after the last steady-state period.

V. SIMULATION

Building a mathematical model of the algorithms is not realistic due to the complexity of the problem. Their implementation on a grid cannot give reproducible results. So we use a grid simulator to evaluate the three algorithms.

The simulator was implemented above SimGrid and its MSG API [START_REF] Casanova | Simgrid: A toolkit for the simulation of application scheduling[END_REF], [START_REF] Casanova | Scheduling distributed applications: the simgrid simulation framework[END_REF]. it is based on the master/slave paradigm. Algorithms are implemented in the master node and dispatch tasks to slave nodes according to the scheduling decisions.

Figure I shows the platforms and figure 2 shows the jobs used in the simulation discussed in the next section. For instance, in the platform P F 0 , the processor p 1 needs 10 time units to perform a task A (p 1 (A) = 10).

The processor and algorithms performances are expressed in time units as there are obtained by simulation and not by experiments. These results may be applied to different time units: seconds, minutes, etc. Table II gives the simulations results for small (50), medium (100) and big (500) batches. The capacity (Cap.) is a lower bound of the time needed to execute one job: the size of the period the steady-state algorithm divided by the number of jobs produced during the period. Since the schedule computed by the steady-state algorithm is optimal, this value is a lower bound for the time needed to execute one job. The results given in table II are obtained using the following expression: performance = capacity × batch size/makespan. So, this value represents the ratio of their makespan and the lower bound.

TABLE I: Simulation platforms

A A B C D A B C D A A B C D B C D A (J1) (J2) (J3) B C D A B A C D A A B C D A B C D A (J4) A B (J5) A B C D (J6) A B A A (J7)

A. Performances

GATS is the best algorithm for small and medium batches with an average performance of 0.99. On-line scheduling and the steady-state scheduling are the seconds with an average performance of 0.93. For big batches (500 jobs), the steadystate algorithm gives the best results, on-line scheduler is the second and GATS has very poor performances.

The on-line algorithm is always good and stable around 0.94 with a minimum value of 0.86 and the two others are less reliable as, in some cases, they have very bad performances with 0.46 for steady-state and 0.22 for GATS. Each of these two algorithms has however its own domain of stability: GATS in small and medium sizes and steady-state in larger sizes.

Another result not shown by this table, is that our adaptations on the algorithms -parallelizing the initialization and termination stages of the steady-state algorithm and using limited buffer size in the on-line algorithm -generate significant performances improvements. For instance, for on-line algorithm, the mean result for small batches is improved by 16% and, for steady-state algorithm, it has been improved by 52%.

0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 000 000 111 111 0 0 1 1 0 1 0 0 0 1
0 0 0 0 0 0 0 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 1 1 1 1 1

B. Batch size

The main drawbacks of the steady-state scheduler are its initialization and termination stages. Figure 3a shows an experiment where the steady-state period takes 1000 time units (one period) to execute 37 jobs. The initialization executes 148 partial jobs (740 tasks) and the termination cleans up 148 partial jobs (592 tasks). In this experiment, the steadystate algorithm makes up its handicap for a batch of 500 jobs where it becomes better than the two other algorithms. However, figure 3b shows that this is not always true. In this experiment the steady-state period takes 1000 time units to execute 110 jobs, the initialization and the termination executes 110 partial jobs and the scheduling is not able to make up its handicap even for 1000 jobs. The difference between these two experiments is in the parallelism of the initialization and the termination stage. In (a) a high level of parallelism is possible as tasks of types A, B, C and D are scheduled in initialization and termination while, in (b), the initialization stage manages only tasks of type A and termination tasks of type B.

GATS is very sensitive to the batch size, for small and medium batches (50 and 100) GATS has an average performance of 0.99 but it falls to 0.61 for big batches (500). One of the reasons of this performance loss may be the scheduling intervals presented in IV-A: GATS does not enhance the whole schedule but just partial schedule intervals of 200 tasks. Note that some of the results, on P F 0 for example, are not affected by this, so intervals are note the only reason. We propose another explanation in the next section.

The on-line scheduler performances does not change with the batch size. This is not surprising as the algorithm takes jobs one after another and thus does not depend on the batch size.

C. Platform / Job

We can observe that the performances depend on the platform characteristics. On platform P F 0 , where no parallelism is possible for a task type, the three algorithms perform well. On platform P F 1 , the three algorithms choose where to schedule A, B, C tasks as several processors can execute them. This leads to poor performances for GATS on batches bigger than 500 because the search space is too large. For the steady-state scheduler, the number of jobs per steady-state period becomes larger leading to longer initialization and termination stages and so to bad performances.

The on-line scheduler performs well in general as shown on figure 4a. The only identified drawback is that the algorithm does not take the graph dependencies into account. For instance, in the case of the platform P F 2 (fig. 4b), the first processor is the fastest at producing A tasks and the only one able to carry out B tasks. For a set of jobs composed of two tasks of type A and B with B depending on A, the online scheduler first balances the load of A tasks between all Fig. 4b: Simulation with platform P F 2 and job J 5 processors, as they are the only free tasks. Then, when tasks B are freed, the first processor has to finish the execution of all its A tasks before executing B tasks. This leads to a performance loss as shown on figure 4b or on table II when scheduling 50 jobs J 5 on P F 1 .

As explained in the previous subsection the steady-state algorithm may suffer from its initialization and termination stages. These two stages closely depend on the period size and on the number of jobs in the period. The period depends on the platform and the job. For example, on table II, scheduling job J 5 on platform P F 1 leads to a period of 1000 time units for 110 jobs. On the opposite scheduling job J 5 on platform P F 0 leads to a period of 10 time units for 1 job. The steady-state algorithm performs poorly when the platform/job association leads to large number of jobs in a period, in particular for small to medium batches. This is shown by the results of job J 5 : on platform P F 0 the schedule is always optimal, whereas, on P F 1 , the performances increase with the batch size to make up the delay generated by the initialization and termination stages.

As a genetic algorithm, GATS explores the possible schedules space to find a good schedule. This space grows when processors are able to execute different types of tasks and when the jobs contain tasks of the same type like in the experiments involving platform P F 1 or P F 5 (Table II). In such big spaces, GATS is not able to converge to a good schedule and its performances fall when the size of the batch increases, as shown in figure 4a. This is also significant on table II when scheduling jobs on platform P F 1 compared to platform P F 0 .

D. Computation time of the scheduling stage

The table III jobs using the three different algorithms. We can note that the steady-state scheduler is the fastest. The on-line scheduler is also very fast, but, on real experiments we must take care as it does not provide any guaranties on real time use. GATS is very slow, this is acceptable to schedule a batch, but the computation overhead is too important to launch an execution on the fly.

VII. CONCLUSION AND FUTURE WORKS

In this paper, we have presented a performance comparison with three scheduling algorithms for bounded batches of jobs on heterogeneous platforms. On-line scheduling is a good algorithm, but it does not reach optimal performances when the size of the batches increases. Steady-state suffers from its initialization and termination stages. it could be improved by parallelizing these two stages. Another point to look at is the steady-state period, the number of jobs to perform in the initialization and the termination is directly linked to the number of jobs per steady-state period. Futures works should try to find a balance between the period jobs count and the number of jobs to schedule. GATS obtains excellent performances for small batches but degrades with the batch size. Future work should investigate the performances degradation and find solutions to avoid them. The computation time needed to obtain the schedule from GATS cannot be improved by a great magnitude, code optimization will reduce it, but the inner time complexity of GATS forces it to be computation intensive.

Future studies will generalize the problem by introducing communication costs and DAG with forks. The forks on DAG will increase the complexity of the steady-state scheduling, future experiments should tell us if it is significant. Fault tolerance is also an issue of interest : off-line algorithms (steadystate and GATS) will probably suffer from the unpredictable platform behavior while the on-line scheduler should not need any adaptations as it is based on dynamic informations.

Fig. 1 :

 1 Fig. 1: Overlapping of Interval i and Interval i+1 .

Fig. 2 :

 2 Fig. 2: Simulation jobs

Fig. 3b :

 3b Fig.3b: Simulation with platform P F 1 and job J 5

TABLE II :

 II Performance of On-line, Steady-state and GATS against platform capacity.

	Time unit	000 111 00 00 11 11 0 1 00 00 11 11 00 11 0 0 1 1 00 00 11 11 0 0 1 1 00 11 0 1 00 00 11 11 000 000 111 111 0 0 1 1 00 00 11 11 0 0 1 1 00 11 0 1 00 11 0 1 0 0 1 1 0 1 0 0 1 1 00 0 0 0 1 1 1 00 00 11 11 00 00 00 11 11 11 00 11 11 0 0 1 1 00 00 11 11 0 0 0 0 1 1 1 0 0 1 1 1 000 000 111 111 00 00 11 11 00 00 11 11 0 1 00 00 11 11 0 1 0 0 1 1 0 0 1 1 00 11 00 00 11 11 00 00 11 11 00 00 11 11 0 0 1 1 00 00 11 11 0 0 0 1 1 1 000 111 0 0 1 1 00 11 0 0 1 1 00 11 0 0 1 1 0 1 00 00 11 11 0 1 00 00 00 11 11 11 0 0 0 1 1 1 00 00 00 11 11 11 0 0 0 0 1 1 1 1 00 00 00 00 00 11 11 11 11 11 0 0 0 0 0 0 Batch size 1 1 1 1 1 1 10 50 100 150 200 250 300 400 500 600 700 800 900 1000 0 20000 40000 60000 80000 100000 120000 140000 160000 200000 180000 Capacity x batch size On-line scheduler Steady-state scheduler GATS
		Fig. 3a: Simulation with platform P F 1 and job J 4
		000 111 0 0 1 1 00 11 00 00 11 11 00 00 00 11 11 11 000 000 111 111 00 11 00 11 0 0 1 1 0 0 0 1 1 1	0 0 0 1 1 1 0 0 0 1 1 1 00 0 0 0 0 1 1 1 1 00 00 11 11 11 00 0 0 0 0 1 1 1 1 00 00 00 00 11 11 11 11 00 00 00 00 00 11 11 11 11 11 00 00 00 11 11 11 11 0 0 0 0 1 1 1 1 00 00 00 00 00 00 11 11 11 11 11 11 00 0 0 0 0 0 0 1 1 1 1 1 1 00 00 00 00 00 00 00 11 11 11 11 11 11 11 00 00 00 00 00 00 00 11 11 11 11 11 11 11 00 00 00 00 00 00 00 00 11 11 11 11 11 11 11 11 00 00 00 00 00 11 11 11 11 11 11 00 00 00 00 00 00 00 00 11 11 11 11 11 11 11 11	0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1

  shows the average time needed on an Intel Core 2 Duo running at 1.6 GHz to compute the schedule of 1000

	On-line scheduler	Steady-state scheduler	GATS
	35.04s	0.08s	1799.68s

TABLE III :

 III Average time spent by the micro-processor to compute the schedule of 1000 jobs.


J Julliand
email: julliand@lifc.univ-fcomte.fr

P.-A Masson
email: masson@lifc.univ-fcomte.fr

R Tissot
email: tissot@lifc.univ-fcomte.fr

Generating Tests from B Specifications and Test Purposes ⋆

Keywords: Model-Based Testing, Test Purpose, IAS Case Study

This paper is about generating tests from test purposes, in addition to structural tests. We present a method that re-uses a behavioural model and an abstract test concretization layer developed for structural testing, and relies on additional test purposes. We propose, in the B framework, a process of test generation that uses the symbolic animation mechanisms of LTG (Leirios Test Generator) based on constraint solving, and guided by the test purposes. We build for that a B animable model that is the synchronized product of a behavioural B abstract model and a test purpose described as a labelled transition system. We prove the correctness of this method, and illustrate it by means of the IAS case study. IAS is a smart-card application dedicated to the operations of Identification, Authentication and electronic Signature.

Introduction

B models are well suited for producing tests of an implementation by means of a model based testing approach [START_REF] Utting | Practical Model-Based Testing -A tools approach[END_REF]. This approach proceeds by writing a formal behavioural model (M) of the expected functionalities of a system. This model is an abstraction of any real implementation, and is supposed to provide a reliable view of the implementation under test (IUT). By applying selection criteria, a test generation tool can automatically extract tests from the model. These tests are particular "executions" of the model. They are sequences of operation calls of the model, with the values of their parameters and their results as predicted by the model. The tests are abstract since they have the same level of abstraction as the model. They are concretized to execute them on the IUT by a concretization layer (CL). Comparing the results returned by the IUT with the ones predicted by the model allows delivering a verdict of the tests.

Structural testing uses static (syntactic) selection criteria, essentially providing control flow and data coverage of the model. The tests exercise the functionalities of the system by directly activating and covering the corresponding operations. Industrial studies have proven the efficiency of the method to detect faults in an implementation (see for example [START_REF] Farchi | Using a model-based test generator to test for standard conformance[END_REF][START_REF] Bernard | Generation of test sequences from formal specifications: GSM 11-11 standard case study[END_REF]). Writing M and CL is an important effort, but the cost is justified by the possibility to automatically compute a great number of smart test cases. Nevertheless, static selection criteria appear to be insufficient to exercise the IUT in tortuous situations. We think for example of some elaborate scenarios of attack of systems requiring strong security guarantees. Our objective is to benefit from M and CL to compute some additional tests that use a particular scenario as a selection criterion.

The scenario can be described by means of a test purpose (TP), which we consider as a dynamic (semantic) selection criteria that orchestrates the successive calls of the operations of the model. The tests extracted from the model by means of a test purpose are sequences of operation calls corresponding to the scenario.

The context of this work is the test generation from B models. We use LTG [START_REF] Jaffuel | LEIRIOS Test Generator: Automated test generation from B models[END_REF], the test generator from Leirios1 , to automatically extract abstract tests from the model. LTG uses a constraint solver for computing the tests. LTG produces structural tests by applying a static criterion to cover all the paths of the control structure of every operation. Moreover, it is possible to assist the generation of tests by providing LTG with sequences of operation calls that describe the shape of the expected tests.

Our main contribution in this paper is to define in the B framework a process that uses LTG for generating abstract tests, with a dynamic selection criterion provided in the shape of a sequence of operations to LTG.

We give in Sec. 2 some preliminary definitions to our work. We present in Sec. 3 our process for computing and executing tests from a B model and a test purpose. Section 4 describes how to combine a behavioural model and a test purpose to obtain a B model for the test generation. We present the IAS case study and our experimentation in Sec. 5. We conclude and compare our proposition to related works in Sec. 6.

Preliminaries

This section gives the background of the paper. First, we give in Sect. 2.1 general notions about B abstract machines. We define the notions of B trace and B execution. We also define the restrictions due to the targeted application class and to the context of test generation. Section 2.2 defines a test purpose as a special kind of labelled transition system. It also presents the notions of TP trace and TP execution associated to the test purpose. The notion of trace is used to guide the test generation tool LTG that computes several executions for each trace.

B Abstract Machines

First introduced by J.-R. Abrial [START_REF] Abrial | The B Book: Assigning Programs to Meanings[END_REF], a B abstract machine defines an open specification of a system by a set of operations. Intuitively, an operation has a precondition and modifies the internal state variables by a generalized substitution. An operation is provided with a list of parameters and can return results.

We address a particular class of specifications of reactive systems. Our specifications are defensive, i.e. we assume that an operation terminates if it is invoked with well typed parameters. That means that we consider environments that respect a contract: they always call the operations with well typed parameter values. We also assume that any operation returns a status word that codifies a report of its execution. Therefore in the remainder of the paper, operations are defined as in Def. 1.

For defining a B abstract machine, we need to remind the reader of the notions of B predicates and B generalized substitutions. B predicates on a set of variables x are denoted by P (x), R(x), I(x), T (x), . . . In the remainder of this paper, the predicate I(x) denotes an invariant and T (p) denotes a typing predicate on the parameter variables p. When there is no ambiguity on x, we simply denote the predicates by P , R, I, . . . We denote by S the B generalized substitutions and by E, F , . . . the B expressions. Given a substitution S and a post-condition R we are able to compute the weakest precondition P , such that if P is satisfied, then R is satisfied after the execution of S. The weakest precondition, defined in [START_REF] Abrial | The B Book: Assigning Programs to Meanings[END_REF], is denoted by [S]R. We denote by S R the expression ¬[S]¬R, intuitively meaning that if S R is satisfied, then a computation of S exists terminating in a state satisfying R. Given a B substitution S, a particular predicate denoted by prd x (S) defines the relation between the values of the state variables x before the execution of S and the values of the state variable x ′ after the execution of S. prd x (S) is the pre-post predicate of S. It is defined in Def. 2. A B abstract machine is defined as in Def. 3. Definition 1 (Operation). Let S i be a substitution. Let sw i be a status word and p i be a list of parameter names. Let T i (p i ) be a typing predicate on p i . An operation named op i is defined as

sw i ← op i (p i ) = PRE T i (p i ) THEN S i END.
Definition 2 (prd x ). Let S be a substitution. The predicate prd x (S) is defined as prd x (S) = S (x = x ′ ).

Definition 3 (B Abstract Machine). A B abstract machine M is a tuple x, I, Init, OP where x is a set of state variables, -I is an invariant predicate over x, -Init is a substitution called initialization, -OP is a set of operation definitions as in Def. 1.

We denote as X M (where X ∈ {x, I, Init, OP }) a component of the B model M. If there is no ambiguity on the model that is considered, we simply denote it by X. A model M defines a set A M of operation names and a set Pred M of B predicates over the state variables x of M.

The test cases are finite executions. We first define the notion of B trace of a B abstract machine in Def. 4. Intuitively, a B trace is a finite sequence of operation names starting after the initialization.

Definition 4 (B Trace). Let M = x, I, Init, OP be a B abstract machine. A trace is a finite sequence τ M = Init; op 1 ; op 2 ; . . . ; op n where op i is the name of an operation (∈ A M ) defined in OP as in Def. 1.

Several executions can be associated to a B trace because, for any operation op i , there are possibly several parameter values v i of p i that satisfy the typing predicate T i (p i ). As can be seen in Def. 5, an execution is an instance of a B trace with parameter values for every operation call that satisfy the precondition T i (p i ).

Definition 5 (B Execution). Let M = x, I, Init, OP be a B abstract machine. Let τ M = Init; op 1 ; op 2 ; . . . ; op n be a trace of M. σ M = (op 1 (v 1 ), w 1 ); (op 2 (v 2 ), w 2 ); . . . ; (op n (v n ), w n ) is an execution associated to τ M , denoted by σ M ∈ Exec B (M, τ M ), if there is a sequence of state variable values u 0 ; u 1 ; u 2 ; . . . ; u n , a sequence of status words w 1 ; w 2 ; . . . ; w n and a sequence of parameter values v 1 ; v 2 ; . . . ; v n such that

-[x ′ := u 0 ]prd x (Init), -for any i ∈ 1..n: [p i := v i ]T i (p i ) ∧ [x, x ′ , sw i , p i := u i-1 , u i , w i , v i ]prd x (S i ).
Since we assume our specifications to be defensive, there is at least one execution associated to a B trace if T i (p i ) is a satisfiable typing predicate. Thanks to that, we assume that the executions respect the contract, i.e. the environment (simulated by the test generator) always calls the operations with well-typed parameter values. In other words, the typing precondition is interpreted as a guard in B event systems, in such a way that the test generator chooses parameter values that satisfy the guard, i. e. the typing predicate T i (p i ). Moreover, the operation call op i (v i ) from the state u i-1 gives the new state variable values u i and returns the status word w i . u i-1 , u i , w i and v i satisfy the pre-post predicate of S i .

Test Purpose

We have defined in [START_REF] Julliand | Generating security tests in addition to functional tests[END_REF] a language for describing test purposes, that combines operation calls and target state descriptions. Its semantics is given as a labelled transition system as in Def. 6. A test purpose TP is bound to a B abstract machine M that is the specification of the system under test. We say that TP is defined on M. We give a unique name to any transition in a set T = {t 1 , t 2 , . . . , t n }. The binding between TP and M is such that the transitions of TP are labelled by the names of the operations of M in A M , and a state predicate of Pred M on the variables x of M is associated to any state of TP.

Definition 6 (Test Purpose). A test purpose on a model

M is a tuple Q, q 0 , T, λ, Q f where Q is a finite set of states, q 0 ∈ Q is the initial state, Q f ⊆ Q is the set of terminating states, T ∈ T → Q × A M × Q is a finite set of
named and labelled transitions denoted by t i -→ q i-1 opi → q i , and λ ∈ Q → Pred M is a total function that associates a state predicate, denoted by λ(q i ), to every state.

A test purpose TP defines a set of finite traces that represents a set of symbolic test cases. We call each trace a TP trace (see Def. 7). A TP trace is that of a finite sequence of transitions that must be well formed w.r.t. the transition relation of TP. These symbolic test cases must be instantiated as test cases (non symbolic), called TP executions (see Def. 8) by a symbolic animator from a behavioural model M and some coverage criteria. In Def. 8, an execution is a finite sequence of pairs made of an operation call provided with the values of its parameters, and the expected status word value returned by the operation call.

The executions are easy to compute by a test generator when the TP traces are sequences of operations whose names have all been instantiated. Backtracking may be necessary to satisfy the constraints set by the predicates for the states to reach, and the enabling conditions of the operations.

Definition 7 (TP Trace). A finite sequence of transitions τ TP = t 1 ; t 2 ; . . . ; t n is a trace of a test purpose TP if there are

q i ∈ Q and op i ∈ A M , 0 < i ≤ n, such that for any i ∈ 1..n, t i -→ q i-1 opi → q i ∈ T and q n ∈ Q f .
Given a trace τ TP , there are zero or many executions of τ TP on the B abstract machine on which TP is defined.

Definition 8 (TP Execution). Let M = x, I, Init, OP be a B abstract machine. Let τ TP = t 1 ; t 2 ; . . . ; t n be a trace of a test purpose

TP = Q, q 0 , T, λ, Q f defined on M. σ TP = (t 1 (v 1 ), w 1 ); (t 2 (v 2 ), w 2 ); . . . ; (t n (v n ), w n
) is an execution associated to τ TP , denoted by σ TP ∈ Exec TP (M, τ TP ), if there are a sequence of state values of TP q 0 ; q 1 ; q 2 ; . . . ; q n , a sequence of state variable values of M u 0 ; u 1 ; u 2 ; . . . ; u n , a sequence of status words values w 1 ; w 2 ; . . . ; w n and a sequence of parameter values v 1 ; v 2 ; . . . ; v n such that:

-[x ′ := u 0 ]prd x (Init), -for any i ∈ 1..n: t i -→ q i-1 opi → q i ∈ T , -for any i ∈ 1..n: [p i := v i ]T i (p i ) ∧ [x, x ′ , sw i , p i := u i-1 , u i , w i , v i ]prd x (S i ) ∧ [x := u i ]λ(q i ).
As for the B executions, several TP executions can be associated to a TP trace for the same reasons. But in the TP executions, every operation call op i (v i ) must moreover lead to a state that satisfies the target state predicate λ(q i ) which is associated to the target state q i of the test purpose. For that, in Def. 8, we have added the following condition for any i: [x := u i ]λ(q i ). Consequently, it is also possible that no execution is associated to a TP trace if there is no sequence u 1 ; u 2 ; . . . ; u n of state variable values that satisfy the sequence λ(q 1 ), λ(q 2 ), . . . , λ(q n ) of target state properties.

Process of Property Based Testing

Our process for generating tests uses a test purpose as selection criterion and a B behavioural model as oracle. The complete process is described by Fig. 1. The left part of Fig. 1 shows how the set of abstract test cases is first computed, whereas the right part shows how these tests are finally executed on the IUT and the verdict is delivered.

Computing the abstract test cases is obtained by a symbolic animation of the TP traces on a B machine M TP that is the synchronized product between the B model M and the test purpose TP. The synchronized product between M and TP is computed according to the expression in B that is given in Sec. 4. The result is a B machine M TP whose executions are the possible executions from M that conform to TP. Besides, TP is unfolded as a finite set of TP traces (see Def. 7) τ TP , i.e. as sequences of transition names (each one labelled with an unparameterized operation call) defined according to TP, but without the target states. This set computes all the TP traces whose last state is terminating, and whose length is lower or equal to a maximum length defined by the tester.

We use LTG, the test generator from Leirios, to instantiate the TP traces. LTG proceeds by symbolic animation. Notice that any other tool with similar capabilities could be used for that purpose. The principle is to "guess" values for the parameters of the operations that make it possible to execute the sequence of operations as described by a particular trace τ TP of the test purpose. In other words, TP executions are computed from τ TP and M TP . The parameter values are computed in LTG by a constraint solver, that finds some values that make the sequences of operations of τ TP reach the target states given in the TP. No execution is computed when the target states are impossible to reach. The status words are also computed as expected by M TP for these parameters. Additionally, from one TP trace τ TP , LTG will try to compute a different TP execution for each of the behaviours of the last operation of τ TP : every branch of an operation described as a control structure (such as a conditional structure) is called a behaviour of the operation.

The tests computed by this procedure have the abstraction level of the model M of the system. They can not be executed as such on the IUT. They have to be concretized by the concretization layer CL which converts the instantiated operation calls of the TP execution into a script executable on the IUT. This computes a set of concrete tests. These concrete tests can then be executed on the IUT, from which the output values (the status words) are observed. The concretization layer also gives the correspondence between the status words from the IUT and the ones from the model. This allows delivering the verdict of the test by comparing the values really returned by the IUT with the ones predicted by the model.

Combining a Model and a Test Purpose for Security Test Generation

In Fig. 2, we define how to express in B the synchronized product M TP of a behavioural model M described as a B abstract machine, and a test purpose TP on M. M TP includes the abstract machine M so that it can read the state variables x of M, and it can synchronize any transition t of TP with a call to an operation of M labelled by t. The variable Cq represents the current state reached by the last transition executed in the test purpose TP. The initial state is q 0 . For any transition t i (such that T (t i ) = q i-1 opi → q i ), we define an operation also called t i in M TP . Its parameter values must satisfy the typing predicate T i (p i ) of the operation op i that is called. This operation is enabled if the current state is q i-1 and if there are state variable values x ′ and a status word value sw ′ i after t i that satisfy the pre-post predicate of the body of the operation op i and the target state predicate of the test purpose λ(q i ). When these conditions hold, the operation t i calls the operation of the test purpose op i and places the system in the target state q i of the test purpose.

Theorem 1 establishes the soundness of the method. For a TP trace τ TP = t 1 ; t 2 ; . . . ; t n (see Def. 7), any B execution (see Def. 5) of the B composed abstract machine M TP for the B trace τ M TP = Init M TP ; t 1 ; t 2 ; . . . ; t n is a TP execution (see Def. 8) of τ TP on the abstract machine M. Theorem 2 establishes the method completeness.

Theorem 1 (Soundness). Let M TP be the B composition of a B model M and a test purpose TP on M as in Fig. 2, and let τ TP be a TP trace then,

Exec B (M TP , Init M TP ; τ TP ) ⊆ Exec TP (M, τ TP ).
Proof. The proof relies on the fact that, the difference between the B executions of the model M and the TP executions of M, is that, the target predicate λ(q i ) holds in every target state q i of the TP execution. This condition is also satisfied in the B execution of M TP since we add this condition in the guard of its operations t i (see Fig. 2). Moreover, it is obvious that the B executions of M TP and the TP executions of M compute the same sequence of states as TP, and execute the same sequence of operation calls as M. The proof is straightforward. Our implementation with LTG computes the B execution of M TP with the semantics given in Def. 5. It is sound, but not complete because the constraint solving algorithm is time limited.

(pi) = PRE Ti(pi) THEN SELECT Cq = qi-1 ∧ ∃(x ′ , sw ′ i ) • (prdx(Si) ∧ [x := x ′ ]λ(qi)) THEN swi ← opi(pi) || Cq := qi END END; . . . END

Case Study

IAS case study

This work was done in the framework of the RNTL POSE project, that brings together industrial (GEMALTO, LEIRIOS, SILICOMP/AQL) and academic (LIFC/INRIA CASSIS project, LIG) partners. The problem is the validation of a system conformity to its security policy, especially for smart cards.

Experiments have been made with a real size industrial application, the IAS platform. Prior to the project, a behavioural model in B had been written by the LIFC and Leirios, from which structural tests had been computed and executed on an IAS implementation by Gemalto. We have extended these tests with security ones.

IAS is a standard for Smart Cards developed as a common platform for e-Administration in France, and specified in [START_REF] Gixel | Common IAS Platform for eAdministration[END_REF] by GIXEL. IAS provides services to the other applications running on the card. IAS conforms to the ISO 7816 standard.

The file system of IAS is illustrated with an example in Fig. 3. Files in IAS are either Elementary Files (EF), or Directory Files (DF), e.g. file 01 and file 02 in Fig. 3. The file system is organized as a tree structure whose root is designed as MF (Master File).

The Security Data Objects (SDO) are objects of an application that contain highly sensitive data such as PIN codes (e.g. pin2 in Fig. 3) or cryptographic keys, that can be used to restrict the access to some of the application data. The access to an object by an operation in IAS is protected by security rules based on security attributes. The access rules can possibly be expressed as a conjunction of elementary access conditions, such as Never (which is the rule by default, stating that the command can never access the object), Always (the command can always access the object), or User (user authentication: the user must be authenticated by means of a PIN code).

Let us present the variables of the model that we use in an example of a test purpose given in Sec. 5.2. Let X ID be a set of X identifiers, where X is either DF, PIN, OBJ or SDO. The variable current DF (∈ DF ID) stores the current selected DF. The variable pin2 dfParent (∈ PIN ID → DF ID) associates to a PIN the DF where it is located. The variable rule 2 obj (∈ SDO ID ∪ {always, never} ↔ OBJ ID) associates to a SDO the object that it protects. If the object is always (resp. never) accessible, then the SDO is replaced by the value always (resp. never). The variable pin authenticated 2 df (∈ PIN ID ↔ DF ID) associates to a PIN the DF where the PIN is authenticated.

Consider for example the data structure shown in Fig. 3. pin2 → file 01 ∈ pin2 dfParent means that the PIN object pin2 is located in the DF file 01. pin2 → file 02 ∈ rule 2 obj means that the access to the DF file 02 is protected by a user authentication over the SDO pin2. If pin2 → file 02 ∈ pin authenticated 2 df, then the access to the DF file 02 is authorized, otherwise it is forbidden.

For creating objects, the commands are CREATE FILE DF, PUT DATA OBJ PIN - CREATE, ... For navigating, they are SELECT FILE DF PARENT, SELECT FILE DF - CHILD, ... For setting the values of attributes, they are RESET RETRY COUNTER, CHANGE REFERENCE DATA, VERIFY, ... For changing the life cycle state of objects, they are DEACTIVATE FILE, ACTIVATE FILE, TERMINATE FILE,...

Test Purpose Example

Here, we exhibit one of the test purposes written for the experimentation of our approach. The property to be tested is "to access an object protected by a PIN code, the PIN must be authenticated ". We associate with this property a test purpose that causes the loss of the PIN authentication in all possible ways, and then tries to access the object. This test purpose is instantiated on the example of Fig. 3, for which we imagine that the access to the DF file 02 is protected by an authentication over the PIN pin2. The tester can describe this test purpose by regular expressions, as illustrated in Fig. 4. They are easily translated into the automaton shown in Fig. 5. The state properties in the states s 1 to s 7 are defined as B predicates over the state variables of the B model M, as in Fig. 4. The transitions from the state s 0 to the state s 4 aim at building the data structure surrounded by a dashed line in Fig. 3. The first transition creates a new DF (file 01). The second creates a PIN object (pin2) into the DF file 01, and gains an authentication over it. The third transition creates the DF file 02 into the DF file 01. The fourth transition resets the current DF to file 01, in order to start the core of the test. As a result, the DF file 02 is protected by the PIN pin2 (located in the DF file 01) for all possible access commands. The PIN pin2 is authenticated.

The following transitions translate the regular expression in Fig. 4, and show the core testing stage, describing the testing of the security property in three steps. First, the transitions between s 4 and s 5 describe all the possible ways for losing the authentication (for instance, a failure of the VERIFY command or a reset of the retry counter) over the PIN pin2. The transition from s 5 to s 6 selects the DF file 02. Finally, the transitions between s 6 and s 7 describe the application of the access commands inside the DF file 02 to test the access conditions. The state s 7 is the terminating state.

Experimentation and results

In this part, we give the results of an experimentation done with the B model of IAS which is 15500 lines long. The complete IAS commands have been modelled as a set of 60 B operations.

We first discuss what knowledge of the model is required to write the test purposes, and then we present our experimental results. Designing test purposes The description language is based upon regular expressions, which makes it easy to use. But designing a test purpose requires some knowledge of the model. The tester must know the names of the different operations of the model, and of the state variables and constants to describe the states to reach. Moreover, he must choose the right behavioural level for the description of the test purposes, to ensure good performances of the test generation. For example, inserting a state to reach between two operation calls allows reducing the search space, but requires searching which conditions ensure the execution of the second operation without reducing its reachable behaviours.

Experimentations We have experimented with three different test purposes, which gave a total of 183 tests that have been run on the IAS implementation. The test purpose example shown in Fig. 5 gave 30 test TP traces, which have produced 35 TP executions. This is because sometimes there are several possible behaviours to cover in the last operation of the TP trace.

The two other test purposes were for testing possible bad interpretations of the access conditions due to a mechanism of short references to the security objects, and the effects of life cycle changes on the authentication of a PIN. In these various test campaigns, we have successfully instantiated every TP trace, except when they contained unreachable states (w.r.t. the constraints on the operations sequencing). Furthermore, we have begun an experimentation to test the POSIX compliance of a file system. We have already generated 250 test sequences (from 5 test purposes) for this case study. By now, these sequences are able to test non-trivial executions of the system with basic operations.

Experimental results

The tests that we have generated are not redundant w.r.t. the tests computed with static coverage criteria like behaviour coverage. This is because the test purposes force the test generator to reach some given states or to apply some operation sequences, which would not have been necessarily reached or covered otherwise. These tests address some situations which have been identified as potential vulnerabilities, and which were not addressed by the previously generated structural tests.

We illustrate the difference between tests based on a test purpose and structural tests through the example of the aforementioned property: the access to DF file 02 is protected by PIN code pin2. The automaton associated to the TP that we have considered for this property is shown in Fig. 5. Let us imagine the same kind of automaton, but for a structural test related to this property. Structural testing will exercise the property in two ways: by gaining an authentication over pin2 and successfully accessing file 02, or by not gaining the authentication and thus failing to access file 02. The automata for these two cases are respectively given in Fig. 6 and Fig. 7. In these two automata, the initialization stage is (almost) identical to the automaton for the TP, because we want to compare the tests based on the same data structure. In comparison to Fig. 5, the only difference is about the VERIFY command that is given with its expected result (denoted by the subscript OK) in Fig. 6, and absent from Fig. 7.

Then the core testing stage only consists of trying to access file 02, which is always refused, as denoted by the subscript ¬OK in Fig. 7, and always allowed in Fig. 6 (in Fig. 5, the expected result of every access command should be ¬OK).

The value-added of the tests from the TP is to force the coupling between a successful authentication and (later) an access denial. In other words, two operation behaviours are coupled in the same execution, whereas they were not tested together with structural testing.

Another advantage of using test purposes is that they are issued from a potential vulnerability, to which the tests computed can be linked. This traceability is more difficult to obtain for structural tests.

Conclusion and Future work

We have presented in the B framework a method for generating tests from test purposes in a behavioural model based testing context. The tests generated are additional w.r.t. the structural ones [START_REF] Bernard | Generation of test sequences from formal specifications: GSM 11-11 standard case study[END_REF][START_REF] Satpathy | ProTest: An automatic test environment for B specifications[END_REF]. The method has been validated on a real-size industrial application. The method makes use of already existing material, written for model based structural testing: the behavioural model and the concretization layer. Additionally, test purposes are written to describe how to test behavioural properties.

The method easily ensures the traceability of the tests generated to the original test purpose, since the tests are computed from them. Also, with the traceability mechanism for functional test generation that we use, we know which operation behaviours have been covered.

Many other works use test purposes as selection criteria to extract tests from a model. The test purposes are described by temporal properties in a temporal logic, input output Labelled (Symbolic) Transition Systems ioLTS (ioSTS), or use cases.

By exploiting its ability to produce counter-examples, a model-checker can be used to compute tests from temporal properties [START_REF] Amman | Using a model checker to test safety properties[END_REF]. These techniques are restricted to finite systems. The TGV approach [CJMR07, JJ05], uses explicit test purposes to extract tests from specifications, both given as ioLTS or ioSTS [START_REF] Jeannet | Symbolic test selection based on approximate analysis[END_REF]. Our approach also addresses infinite systems, like ioSTS. ioSTS are specifications where the data are integers and booleans, whereas the B models define more complex set data structures. So, our approach is based on set constraint solving techniques whereas ioSTS use integer abstract interpretation and constraint solving techniques.

In [START_REF] Satpathy | Synthesis of scenario based test cases from B models[END_REF], the authors present a test case generation algorithm from B event systems and use cases by refinement. There are three main differences with our approach. Our method reuse abstract B machines and a concretization layer CL dedicated to the functional test generation. Therefore we do not refine the test cases. Moreover, our test purposes are more expressive use cases that contain target state information.

Also, as a difference with the above cited approaches, we have showed in a previous work [MJP + 07] how the test purposes can be automatically computed, by modelling some test needs as syntactic transformation rules that transform behavioural properties.

We are currently working at identifying and writing such transformation rules, based on the IAS case study. This work needs to be developed by studying many other case studies (for instance, the mini-challenge that proposes to design and verify a POSIX compliant flash-based system [START_REF] Joshi | A mini challenge: build a verifiable filesystem[END_REF]) in order to produce rules sufficiently generic to be applicable to a variety of examples.

Rules could also be automatically deduced from the syntactic expression of a property, as suggested by [START_REF] Bouquet | Safety property driven test generation from JML specifications[END_REF] for properties expressed in JTPL, a temporal logic for JML.

Fig. 1 .

 1 Fig. 1. Process for Generating and Executing Tests from a B model and a Test Purpose

Fig. 2 .

 2 Fig. 2. Combination of a model M and a test purpose TP on M

Fig. 3 .

 3 Fig. 3. A sample IAS tree structure

.

  Fig. 4. Example of a test purpose -execution step

Fig. 5 .

 5 Fig. 5. Example of a test purpose

Fig. 7 .

 7 Fig. 7. Structural testing for an access denial

  The simplest (and shortest) way not to gain the authentication is by not calling the VERIFY command: this is what LTG does for this example.

	s 0	CREATE FILE DF	s 1	PUT DATA OBJ PIN CREATE • VERIFY OK	s 2
		CREATE FILE DF OK
			DELETE FILE OK
	s 4	ACTIVATE FILE OK	s 3	CREATE FILE DF
		PUT DATA OBJ PIN CREATE OK
		DEACTIVATE FILE OK
		TERMINATE FILE DF OK
		Fig. 6. Structural testing for an authorized access
	s 0	CREATE FILE DF	s 1	PUT DATA OBJ PIN CREATE		s 2
		CREATE FILE DF ¬OK
		DELETE FILE ¬OK
	s 4	ACTIVATE FILE ¬OK	s 3	CREATE FILE DF
		PUT DATA OBJ PIN CREATE ¬OK
		DEACTIVATE FILE ¬OK
		TERMINATE FILE DF ¬OK

http://www.leirios.com

⋆ Research partially funded by the French National Research Agency ANR (POSE ANR-05-RNTL-01001) and the Région Franche-Comté.