P A Bisgambiglia
email: bisgambiglia@univ-corse.fr

E De Gentili

J F Santucci
email: santucci@univ-corse.fr

DEVS-FLOU : ENVIRONNEMENT DE MODELISATION BASEE SUR LE PARADIGME DES EVENEMENTS DISCRETS ET SUR LA THEORIE DES ENSEMBLES FLOUS

Keywords: Environnement de multi-modélisation, DEVS, Théorie des ensembles flous, systèmes complexes

L'objectif de cet article est de présenter une approche générique de multi-modélisation et de simulation de systèmes complexes. Afin de prendre en compte des paramètres flous ou mal connus, nous nous proposons de définir une approche permettant l'ajout d'une technique basée sur la théorie des ensembles flous, dans un environnement de multi-modélisation JDEVS basé sur le formalisme unificateur DEVS.

INTRODUCTION

L'objectif de cet article est de proposer une approche générique de multi-modélisation et de simulation de systèmes complexes. La représentation des systèmes est réalisée à partir d'un ensemble de modèles. Un modèle décrit en utilisant un formalisme spécifique, est en général mieux adapté pour décrire et simuler une partie d'un système. La composition de différents types de modèles, ou de différentes techniques et leurs abstractions à différents niveaux est donc indispensable pour pouvoir étudier un système dans son ensemble. Une telle association de modèles est appelée multi-modèles.

L'étude de systèmes complexes, nécessite donc l'intégration de plusieurs techniques au sein d'un modèle. Pour prendre en compte des paramètres flous ou mal connu, nous nous proposons de définir une approche permettant l'ajout d'une technique basée sur la théorie des ensembles flous, dans l'environnement de multi-modélisation JDEVS développé dans notre laboratoire. Ceux-ci afin de traiter l'incertitude de tels paramètres. L'environnement JDEVS s'appuie sur le formalisme unificateur DEVS (Discrete EVent System specification) introduit par le Professeur Zeigler.

La première partie de cet article introduit les concepts de base de nos travaux : DEVS, JDEVS, la théorie des ensembles flous, et le formalisme fuzzy-DEVS. La seconde partie propose une vision générale de notre environnement de modélisation. La troisième partie présente notre méthodologie de modélisation floue. Enfin, une conclusion reprend les points essentiels de notre travail et fournit des perspectives de travaux restant à effectuer.

ETAT DE L'ART

Dans cette partie nous introduisons les différentes approches et travaux à la base de notre étude. Nous décrivons dans un premier temps le formalisme DEVS, puis l'environnement générique JDEVS. La troisième partie est consacrée à la théorie des ensembles flous et dans la dernière nous présentons une approche fuzzy-DEVS mettant en oeuvre la théorie du flou dans un environnement DEVS.

Le formalisme DEVS

Les concepts de base de l'approche DEVS sont destinés à contrôler la difficulté du problème étudié, en réduisant l'analyse du système, à l'étude d'une somme de sous-systèmes plus simples. Notre environnement basé sur la notion de hiérarchie, permet ainsi d'appréhender la complexité inhérente à un problème de manière tout à fait graduelle. (2) Avec : -X M : l'ensemble des ports d'entrée ; -Y M : l'ensemble des ports de sorties ; -C M : la liste des modèles composant le modèle couplé CM ; -EIC : l'ensemble des liens d'entrée connectant le modèle couplé à ses composants ; -EOC : l'ensemble des liens de sortie connectant les composants au modèle couplé ; -IC : l'ensemble des liens internes connectant les composants entre eux ; -L : liste des priorités entre composants ; La simulation est effectuée en associant à chaque composant un simulateur permettant de mettre en oeuvre les algorithmes de simulation correspondants. DEVS permet donc au modélisateur de s'abstraire totalement de l'implémentation des simulateurs. Une fois le modèle construit et quelle que soit sa forme, B.P. Zeigler a défini un simulateur capable de prendre en compte n'importe quel modèle décrit suivant le formalisme DEVS, et a développé le concept de simulateur abstrait (Zeigler, 1984). L'architecture d'un tel simulateur représente une description algorithmique permettant de mettre en oeuvre les instructions implicites des modèles issus du formalisme DEVS, afin de générer leur comportement. L'intérêt majeur d'un tel simulateur réside dans le fait que sa construction est indépendante du modèle.

Lorsque le formalisme DEVS est replacé dans le contexte spécifique d'un domaine d'application, il se montre trop souvent abstrait, il est alors nécessaire d'enrichir sa syntaxe pour permettre de simplifier la spécification de types de modèles particuliers.

Le formalisme JDEVS

Le formalisme JDEVS [Filippi, 2003]

La théorie des ensembles flous

La théorie des ensembles flous introduite par Zadeh (Zadeh, 1965) offre une palette d'outils pour formaliser les processus de raisonnement humain. C'est un moyen efficace de prendre en compte l'imprécision dans des connaissances. Elle permet alors de modéliser pour les systèmes informatiques des modes de raisonnement proches des modèles humains (Bouchon Meunier, 1985).

ENVIRONNEMENT DE MODELISATION

Le formalisme DEVS a montré sa pertinence comme base unificatrice permettant la coopération de différents types de modèles. Le développement formel d'un environnement basé sur ce formalisme est le fruit de travaux développés depuis huit ans dans notre laboratoire [START_REF] Aiello | Environnement Orienté Objet de Modélisation et de Simulation à Evénements Dis[END_REF], [Delhom, 1997], [Filippi, 2003].

Ces travaux constituent les bases de notre environnement logiciel.

Description de l'approche

Nos travaux ont pour but de définir, non seulement un nouveau module permettant la modélisation et la simulation de systèmes complexes à paramètres vagues, mais également une nouvelle approche d'utilisation qui permet au spécialiste du domaine de représenter les systèmes à étudier indépendamment de l'outil utilisé. Ce module sera intégré au coeur du formalisme déjà développé à l'université de Corse : JDEVS.

Rôles et acteurs

Afin de décrire notre approche, nous avons à l'aide du langage UML [Booch et al., 1998] axé notre réflexion sur la définition des rôles, et les exigences des utilisateurs envers l'environnement. Ainsi nous avons pu identifier les différents acteurs, décrire leurs rôles, et définir les interactions existantes entre chaque niveau.

Constructeur d'infrastructure CI

4.2.3

Spécialiste du domaine Ils vont nous donner des informations en provenance du terrain ainsi qu'une vue générique du problème tout en ayant à la fois une expérience et des besoins précis en matière de résultats (figure 3). Ils n'ont pas forcément de connaissances en informatique, et sont spécialistes du domaine à la base de l'expérience, par exemple pour l'astronomie : physiciens, astrophysicien, ingénieur en électronique spatiale, spécialiste des télescopes... Leurs connaissances exprimées de manière linguistique aident à la réalisation du modèle de base ainsi qu'à regrouper les données d'entrées et exploiter les données de sorties.

3.2.4

Interactions entre niveaux La figure 4

Place dans l'environnement

Nous avons vu que le formalisme JDEVS ne demandait qu'a être étendu. Tout comme les packages déjà développés (Feed back-DEVS, Vector-DEVS …) et intégrés au coeur, le formalisme DEVS-Flou doit s'insérer dans cet environnement (figure 5).

METHODOLOGIE DE MODELISATION FLOUE

Notre méthodologie de modélisation doit être compatible avec les standards DEVS. DEVS est basé sur le paradigme des évènements discrets, afin de prendre en compte des données incertaines, il est nécessaire d'apporter quelques modifications à la structure de ces évènements.

Evènement DEVS

Le Dans DEVS un évènement a lieu à un temps donné, il modifie l'état (la valeur) d'une seule variable. Dans le cas où l'état de plusieurs variables doit être modifié, on génère plusieurs évènements à la même date (au même moment), qui sont traités par les algorithmes de simulation suivant une liste de priorité. Par exemple si trois variables doivent être modifiées par un événement E qui a lieu au temps T on l'éclate en trois évènements E1, E2, E3 pris en compte toujours au temps T mais suivant une liste de priorité définie par l'utilisateur.

Comme nous venons de la préciser, dans le formalisme DEVS un événement doit être traité à une date T bien précise. Comme la notion d'événements est à la base du processus de simulation et que notre approche est uniquement basée sur la modification du processus de modélisation, il n'est donc pas possible d'intégrer la notion de logique floue pour la variable de temps. Ceci passe par une évolution dans la définition des évènements DEVS.

Evènement DEVS-Flou

A partir de la définition d'un évènement DEVS, on constate que les paramètres incertains peuvent intervenir à plusieurs niveaux : sur le temps, sur les valeurs, et sur le temps et les valeurs. On distingue donc trois types d'évènements DEVS-Flou. A partir de la formule (4) il est possible de calculer la valeur de la variable à n'importe quel temps t, en connaissant les valeurs de π et de ζ au temps courant t cour , on utilise pour cela la formule suivante : : pente qui oriente la courbe décrivant la possibilité que t soit à t . A plus long terme nous souhaitons définir un ensemble de fonctions de changement de domaines, et identifier les différentes méthodes à employer pour passer d'un domaine à un autre. On entend par changement de domaine la définition de fonction liant deux domaines différents et permettant de passer plus ou moins facilement de l'un à l'autre tout en conservant la validité de tous les paramètres. Il sera ensuite nécessaire de valider la généricité de l'approche sur plusieurs domaines d'application.

Evènement à valeurs floues

( 1 )

 1 soit des messages internes, message d'un modèle à destination de lui-même, pour prendre en compte un changement d'état, (2) soit des messages externes émis par un modèle à destination d'un autre modèle.

Figure 1 .

 1 Figure 1. Comportement d'un modèle atomique DEVS Le modèle atomique est défini par la structure suivante : AM = < X, Y, S, t a , δ int , δ ext , λ > (1) Avec : -X : l'ensemble des ports d'entrée ; -Y : l'ensemble des ports de sortie ; -S : l'ensemble des états du système ; -t a : la fonction d'avancement du temps (ou de durée de vie d'un état) ; -δ int : la fonction de transition interne déclanché par l'arrivée d'un message interne ; -δ ext : la fonction de transition externe déclenché par l'arrivée d'un message externe ; -λ : la fonction de sortie ; Le modèle couplé est défini par la structure suivante : CM = < X, Y, C, EIC, EOC, IC, L >(2) Avec : -X M : l'ensemble des ports d'entrée ; -Y M : l'ensemble des ports de sorties ; -C M : la liste des modèles composant le modèle couplé CM ; -EIC : l'ensemble des liens d'entrée connectant le modèle couplé à ses composants ; -EOC : l'ensemble des liens de sortie connectant les composants au modèle couplé ; -IC : l'ensemble des liens internes connectant les composants entre eux ; -L : liste des priorités entre composants ;

  fournit un outil générique et évolutif de modélisation et de simulation de systèmes complexes. Il est basé sur une architecture logicielle, organisée sous la forme d'un cadriciel (framework), qui permet l'ajout ultérieur de techniques (telles que la logique floue, les réseaux de neurones …), par la voie de packages spécifiques. L'utilisation de packages permet de respecter la cohérence de l'architecture globale du cadriciel tout en assurant son évolutivité. De plus, grâce à l'utilisation d'un formalisme unificateur, DEVS[Zeigler, 2000], sur lequel est basé chaque technique ajoutée au cadriciel, il est possible d'assurer la compatibilité entre les différents modèles créés. Cet outil a pour but de servir toute la communauté scientifique étudiant les systèmes complexes, il utilise des méthodes originales de modélisation et de simulation accessibles à tous : (1) le modèle est facile à créer et réutilisable (stocké dans des bibliothèques[Bernardi et Santucci, 2002]), grâce à une interface graphique ;(2) l'approche est modulaire ; (3) la phase de modélisation est indépendante de la simulation… De plus des techniques d'étude de systèmes permettant au modélisateur de conceptualiser les modèles selon différents paradigmes ont enrichi le cadriciel : (1) Feedback-DEVS, s'inspire du formalisme F-DEVS[Kofman et al., 2000], il permet la spécification de modèles adaptatifs, auto-apprenants, autorisant la construction de modèles empiriques ; (2) les automates cellulaires, cette méthode est fréquemment utilisée pour l'étude de systèmes ayant des dimensions spatiales et est associé à un mode de représentation de l'espace (SIG) ; (3) Vector-DEVS, cette approche originale est adaptée des méthodes mathématiques de "front tracking"[Glimm et al., 1996] permettant l'étude de la propagation d'un phénomène par la simulation de la dynamique de son interface physique. L'intérêt de ce cadriciel est d'être ouvert et de fournir une base théorique forte pour permettre la réutilisation, le stockage et le couplage simplifié de modèles hétérogènes. Toutefois, sans extensions, ce cadriciel ne permet d'étudier qu'un nombre limité de systèmes, en particulier nous proposons l'ajout d'un package spécifique basé sur la théorie de ensemble flou permettant l'étude de systèmes a paramètres vagues.

Figure 2 .

 2 Figure 2. Exemple de fonction floue En logique booléenne un évènement a lieu à une date donnée t1 ; en logique floue comme le montre la figure 2, un évènement peut avoir lieu à n'importe quelle date entre t1-δt et t1+δt avec, en fonction de la date, des possibilités différentes. 2.4 Le formalisme fuzzy-DEVS Le formalisme fuzzy-DEVS introduit par Y. Kwon dans (Kwon et al., 1996) dérive du formalisme DEVS tout en conservant sa sémantique, ses concepts et sa modularité, il étend les fonctions caractéristiques de DEVS aux ensembles flous. Il permet la modélisation et l'analyse de systèmes complexes à évènement discret avec une structure et un comportement partiellement inconnus, bien que lors de la simulation les paramètres flous soient transformés en données réelles à l'aide de fonctions de défuzzyfication (Anglani et al). De plus le modèle atomique fuzzy-DEVS, contrairement au modèle atomique DEVS est non déterministe (Kwon et al., 1996) et ne permet pas de détermine l'état suivant du système. Enfin la propriété de fermeture sous composition du formalisme DEVS (Zeigler, 1984) (Vangheluwe, 2001) n'est pas respectée. Ces contraintes ne nous permettent pas d'intégrer les modèles fuzzy-DEVS dans un environnement de multimodélisation.

  Il développe le noyau du système (figure 3), celui-ci doit être assez stable et ouvrable pour permettre d'effectuer des mises à jour et d'y intégrer de nouveaux formalismes. Les packages (liés à des formalismes spécifique) doivent permettre de modéliser et de simuler les problèmes posés par le spécialiste du domaine et traduits par le constructeur d'infrastructure. Dans notre cas, son rôle est d'intégrer le formalisme (DEVS-Flou) au coeur de l'application, c'est-à-dire à JDEVS. Il est indispensable que le constructeur d'infrastructure possède des compétences en programmation et connaisse DEVS. L'intérêt de cette démarche est double : premièrement valider notre approche et enrichir son environnement générique tout en complétant l'outil JDEVS et deuxièmement en développant une approche modulaire fondée sur DEVS permettre d'agréger un package sans avoir à réaliser de modification sur le modèle de base.

Figure 3 .

 3 Figure 3. Diagramme de cas d'utilisations 4.2.2 Constructeur d'application CA Ils vont récupérer les renseignements en provenance des spécialistes du domaine et les transposer de manière formelle (figure 3). Ils font l'interface entre les experts de domaines (spécialistes) et le constructeur d'infrastructure (CI), pour ce faire ils doivent réaliser les fonctions de transfert de niveaux et posséder des compétences en informatique et dans le domaine étudié. Leur tâche est d'interpréter le langage des experts pour le rendre accessible au constructeur d'infrastructure, puis de choisir ou créer le modèle le plus adapté aux problèmes posés, de transcrire les besoins collectés en fonction du temps en évaluant les caractéristiques des paramètres à prendre en compte.

  représente et décrit les interactions entre niveaux nécessaires à l'intégration du flou dans notre infrastructure logicielle. L'expert décrit en langage naturel les spécifications du système étudié, c'est-à-dire qu'il traduit des données extraites du terrain ou issus de son expérience de manière compréhensible et exploitable par le constructeur d'application (CA). L'interface Expert-CA est la représentation de données à l'aide de fonctions floues, cette interface permet de faire travailler l'expert et le CA en collaboration et d'exploiter les outils que fournit la théorie des ensembles flous pour la représentation de systèmes à paramètres flous.

Figure 4 .

 4 Figure 4. Rôle des intervenants dans l'environnement Le constructeur d'application traduit les données et modélise le système. Il regroupe les données d'entrées et définit les méthodes permettant de traiter le flou. L'organisation de l'application de façon modulaire en vue de son intégration par le constructeur d'infrastructure (CI) se fait au niveau de l'interface CA-CI. Les spécifications et les méthodes permettant le traitement de systèmes flous sont adaptées afin de permettre leur intégration au coeur du logiciel. Le constructeur d'infrastructure définit les caractéristiques du formalisme DEVS-Flou, et implémente les méthodes définies ci-dessus. Au niveau de l'interface CI-Coeur, il développe et/ou adapte le formalisme pour permettre le traitement de données floues. Enfin il implémente DEVS-Flou et l'intègre à JDEVS. Nous pouvons constater que chaque intervenant peut être lié, ou est responsable d'une des étapes nécessaires à la réalisation du logiciel : spécification, définition des méthodes de traitement, et implémentation. Ceci nous permet d'utiliser au mieux les compétences de chacun et d'avoir une vision élargie du problème.

Figure 5 .

 5 Figure 5. Environnement logiciel Tout au long de son développement du package DEVS-Flou les caractéristiques de compatibilité avec DEVS et JDEVS seront au centre de nos préoccupations. La partie suivante présente notre méthodologie de modélisation ainsi que les aménagements effectués, nécessaire à la compatibilité du formalisme avec l'approche DEVS.

  formalisme DEVS est basé pour la modélisation sur deux types composants : les modèles couplés et atomiques. Ces composants possèdent des ports d'entrée, des ports de sortie et des variables. L'échange des données s'établit à travers les ports des différents éléments d'un modèle, grâce à deux types d'évènements fondamentaux : les évènements externes et les évènements internes. Un évènement externe prévu à l'instant t représente une modification (à l'instant t) de la valeur d'un ou plusieurs ports d'entrée appartenant à un élément donné M. Ceci a pour conséquence une modification des variables de M, à l'instant t. Un évènement interne prévu à l'instant t représente une modification des variables de M (à l'instant t), sans qu'aucun évènement externe n'intervienne. De plus, l'arrivée d'un évènement interne provoque, à l'instant t, un changement de valeur sur un ou plusieurs ports de sortie du modèle M. Un évènement DEVS peut être caractérisé par : E = (temps; port; valeur) (3) Le premier champ représente le temps d'occurrence de l'évènement, le second désigne le port sur lequel l'évènement intervient, et le troisième symbolise la valeur de l'évènement.

  Un évènement à valeurs floues est décrit par la formule (4) qui permet de définir, à un temps donné, le degré de possibilité qu'une certaine variable d'état (var) prenne une nouvelle valeur (val). Ces possibilités seront calculées grâce à l'interprétation de fonctions floues et à un ensemble de règles défini par les spécialistes du domaine. : degré de possibilité que var prenne la valeur val au temps t ; -val var : pente qui oriente la courbe qui décrit la possibilité qu'a var d'être à l'état val à partir de t.

  val

Figure 7 .

 7 Figure 7. Composant DEVS-Flou, modèle à temps et valeurs flous. La figure 7, présente un composant DEVS-Flou pouvant être assimilé à un modèle couplé DEVS. Ce modèle peut prendre en entrée des évènements à paramètres flous sur les valeurs ou les dates. Comme nous ne pouvons pas traiter avec la même méthodologie ces deux paramètres, les modules "Time-Defuzzyfication" et "Time-Fuzzyfication" permettent en modifiant le flou sur le temps de résoudre notre problème. -La fonction Time-Defuzzyfication : transforme en entrée un évènement à temps flou en évènement à valeur floue et à temps fixé. -La fonction Time-Fuzzyfication : transforme en sortie un évènement à temps fixé en évènement à temps flou, c'est la fonction inverse. Ces fonctions seront définies comme des modèles atomiques afin de respecter l'approche DEVS. Pour les évènements à temps et valeurs flous, les deux approches seront utilisées.4.3 Évènements externes ou internes flous

Figure 8 .

 8 Figure 8. Fonction floue représentant le temps mit par Rosetta pour parcourir 135000KM 2. La seconde étape consiste à modéliser à l'aide de fonctions floues ces données. La figure 8 représente cette modélisation. 3. Nous avons pu voir que pour traiter un flou sur des données temporelles, il est nécessaire de transformer ce flou en flou sur les valeurs des variables. La troisième étape a pour but de transformer avec des fonctions de transition de domaine un flou sur le temps en flou sur les valeurs. Au minimum Rosetta parcours 135000Km en 70 minutes, donc en 60 elle en parcourt 115000. Au maximum elle parcourt 135000Km en 50 minutes donc en 60, elle en parcourt 160000. La figure 9 représente la distance en Km parcourue par Rosetta en 60 minutes et est le fruit de ce changement de domaine.

Figure 9 .

 9 Figure 9. Fonction floue représentant la distance parcourue par Rosetta en 60 minutes après avoir appliqué la fonction Time-Defuzzyfication 4. Le flou intervenant maintenant au niveau des valeurs des variables, la dernière étape consiste à appliquer la formule (4). Où : -val est la valeur choisie en abscisse ; -π la valeur correspondant à val en ordonnée ; -ζ le sens du vecteur correspondant au coefficient directeur de la courbe aux points [val;π].

  Le simulateur abstrait de DEVS traite les évènements en les insérant dans un échéancier [] en fonction de la différence entre leur temps et le temps courant. Traiter une date incertaine au niveau du simulateur est très délicat car la simulation a lieu à une date fixée à l'avance, et de plus un évènement influence souvent les évènements suivants. L'un des moyens pour ne pas avoir à gérer les événements avec un temps T qui soit incertain est de transformer le flou au niveau des dates (du temps) en flou au niveau des valeurs. Ce mécanisme revient à "defuzzifier" le temps, c'est-àdire à supprimer l'incertitude pour la transformer en valeur réelle. La théorie des ensembles flous nous permet de rester proche du mode de représentation de données des experts, qui utilisent des fonctions floues pour représenter des incertitudes au niveau du temps et des valeurs des variables. En entrée et en sortie des composants le temps pourra être flou, par contre le flou sur le temps devra être transformé en flou sur les variables au niveau des composants.

											Formule d'un évènement à temps flou : val port t var, , , ~avec occ t t t t , ~var) , (	,	t t	occ	(6)
											Où :
											-	occ t var) t , (	: degré de possibilité que t soit à
											t	[ t	, min t	max	]	, t date d'occurrence d'un évè-
											nement sur var (var prend val).
											-	t t	occ
	val (var, t	cour	)	val var	t (	cour	t	)	t (var,	)	(5)
	4.2.2	Evènement à temps flou

crets de Systèmes Complexes. Thèse de Doctorat, Université de Corse. Anglani, P., Caricato, A., Grieco, A.., Nicci, F., Matta, A., Semeraro, Q. et Tolio, T. Evaluation of capacity expansion by means of Fuzzy-DEVS, MURST Project Bernardi, F. Conception de bibliothèques hiérarchisées de modèles réutilisables selon une approche orientée objet, Thèse de doctorat, (2002) Bernardi, F. et Santucci, J. (2002), Model design using hierarchical web-based libraries, Dans Actes de la conférence 39th conference on Design automation, volume 1, pages 14.17. New Orleans, USA. Booch, G., Rumbaugh, J., et Jacobson, I. (1998), The Unified Modeling LanguageReference Manual. Addison-Wesley. Bouchon Meunier, B. La logique floue et ses applications, (1985) Delhom, M. (1997). Modélisation et Simulation Orientées Objet, Contribution àl'Etude du Comportement Hydrologique d'un Bassin Versant. Thèse de Doctorat, Université de Corse. Filippi, J.-B., Bernardi, et Delhom, M. (2002), The JDEVS environmental modeling and simulation environment, Actes de la conférence IEMSS 2002 conference on Integrated Assessment and Decision Support, 3 :283.288. Lugano, Suisse. Filippi, J. Une architecture logicielle pour la multimodélisation et la simulation à évènement discrets de systèmes naturels complexes. Thèse de Doctorat, Université de Corse, (2003) Fishwick, P. Simulation Model Design and Execution: Building Digital Worlds, Prentice Hall, nj, englewood cliffs edition, (1995) Glimm, J., Simanca, S., Smith, T., et Tangerman, F. (1996), Computational physics meet computational geometry, Rapport Technique SUNYSB-96-19, State University of New York at Stony Brook. Kofman, E., Giambiasi, N., et Junco, S. (2000). Fdevs : A general DEVSbased formalism for fault modeling and simulation. Dans Actes de la conférence 2000 European Simulation Symposium, volume 1, pages 77.82. Hamburg, Germany. Kwon, Y., Park, H., Jung, S., et Kim, T. (1996), Fuzzy-DEVS Formalisme :Concepts, Realization and Application, Proceedings AIS 1996, pages 227.234. Lee, K. et Fishwick, P. Dynamic Model Abstraction, Proceedings of the Winter Simulation Conference, (1996) Vangheluwe, H.L.M. The discrete event system specification (DEVS) Formalism, CS522 Fall Term, (2001) Zadeh, L. Fuzzy Sets, Inform Control, Vol. 8 pp. 338-353, (1965) Zeigler, B. Theory of Modeling and Simulation, Academic Press, (1976) Zeigler, B. Multifaceted modelling and discrete event simulation, Academic Press, (1984) Zeigler, B. (2000), Theory of Modeling and Simulation. Academic Press, 2 nd Edition, ISBN : 0127784551.


Samir Chouali
email: chouali@lifc.univ-fcomte.fr

Cooperation Between the B Method and the Automata Theory to Check the Component Interoperability

Keywords: Component interoperability, compatibility, substitutability, B method, verification

Component interoperability is one of the essential issues in the component based development, since it allows the composition of reusable heterogenous components developed by different people. In this paper, we propose an approach to formally verify component interoperability at signature, semantics, and protocol levels. It is based on the use of the B formal method for specifying component interfaces and finite transition systems for specifying component protocols. The verification is done with the B theorem prover and the verification of the simulation relation between transition systems. This approach allows to decide whether two components can interoperate if assembled together and whether a component can be replaced by another component.

Introduction

The component based development is widely used in software engineering. Its aim is to develop software systems by assembling a collection of pieces that are independently produced. These pieces are called components. The advantages of this approach are the reusability of software components which involves a reduction of the development cost, and the flexibility of developed systems.

A component is a unit of composition with contractually specified interfaces and explicit dependencies [START_REF] Szyperski | Component Software[END_REF]. An interface describes the services offered or required by a component without disclosing the component implementation. It is the only access to the information of a component. The offered services by a component are described by an offered interface and the required services are described by a used interface.

The component interoperability is an essential issue in the component based development. The success of applying the component based approach depends So, the verification of component interoperability involves the verification of the interface compatibility or interface equivalence on the components that will be connected or the component that will be replaced.

The specification of the interfaces plays an important role in the verification of their compatibility. Most current interface modelling languages (IDLs), used in several component oriented platforms like JavaBeans [START_REF]JavaBeans Specification, Version 1.01[END_REF], CORBA [START_REF]The Common Object Request Broker: Architecture and Specification, Revision 2.2[END_REF], or COM [START_REF]The Component Object Model Specification, Version 0.9[END_REF], are limited for expressing signature (operation names, types, parameters) information. They provide insufficient information about component behaviors. Hence, one cannot insure trust in component based systems.

The design by contract approach proposed by B. Meyer [START_REF] Meyer | Object-Oriented Software Construction[END_REF] is the first evolution toward a specification approach that proposes a way to insure trust in components. B. Meyer proposes to annotate interface specifications with assertions that provide pre and postconditions of the operations. Several other works [START_REF] Han | A comprehensive interface definition framework for software components[END_REF][START_REF] Hernandez | Object interoperability[END_REF] have proposed to enhance component interfaces by providing information at signature, semantics (the meaning of operations) and protocol (order in which the operations of a component are called) levels. Despite these enhancements in the interface specification, we believe that there is not enough information in component interfaces to perform a formal verification of the interface compatibility.

In this paper we deal with the formal specification of the interfaces and the verification of their compatibility at the signature, semantics, and protocol levels. We propose to specify interfaces with the B method and to enhance them by the specification of protocols using the automata theory language [START_REF] Kleene | Representation of events in nerve nets and finite automata[END_REF]. The B method allows an abstract specification of systems to be developed step by step using the refinement until the implementation. Therefore we consider that the B specification of an interface is an abstraction of a component implementation.

The B theorem prover is used to verify a step of the interface compatibility. We also exploit the B specifications of the interfaces and their protocol specifications in order to model the behavior of software components with transition systems [START_REF] Arnold | Mec: a system for constructing and analysis transition systems[END_REF]. Thus, we verify the simulation relation between the transition systems, which is the final step of the verification of the interface compatibility.

In the following section we give an overview of the B method. In Section 3 we present the specification of component interfaces and illustrate it by the example of the car wiping system. In Section 4 we present the verification approach of the component interoperability. In Section 5 we present related work. In section 6 we terminate the paper by a conclusion. The B method [START_REF]The B Book[END_REF] is a formal software development approach allowing to develop software for critical systems. It covers the entire development process from abstract specifications to an implementation. The B method is based on the set theory. The basic building block of a B specification is the abstract machine that is similar to a module or a class in an object oriented development. A B specification is composed of one or many abstract machines (examples of B machines are given in Section 3), each of them describes a set of variables, invariance properties (also called safety properties) relating to these variables, an initialization which is a predicate that initializes the variables, and a list of operations. The specification of an operation consists of a precondition part and a body part. The precondition expresses the requirement that must be met whenever the operation is called. The body expresses what the operation achieves, it is expressed with a generalized substitution. The states of a specified system are only modifiable by operations that must preserve an invariant.

With the B method, a system is developed by refinement. The refinement is used to transform step by step an abstract specification into a concrete representation. At each refinement step, you have to prove that the refined specification is correct with its abstraction. Therefore the implementation must refine its abstract specification. The verification with the B method is automated. The B theorem prover, Atelier B [START_REF] Steria | Preuves et Exemples[END_REF], allows the verification of invariance properties and the refinement relation.

Specification of component interfaces

Our goal is to propose an approach to specify component interfaces in order to verify the interface compatibility. This work takes place in the context where components are specified as black boxes, then deployed without knowing details of their implementation. In this context, the specification of component interfaces plays an important role because it is the only description of the component.

We propose to specify components interfaces with the B method and augment the interface specifications with protocol specifications that must be respected by the order of the operation calls. We apply this approach to a case study.

Specification structure

Traditional approaches of interface specification provide signature of operations and their pre and postconditions. In many cases there are not sufficient information in interfaces specifications in order to detect the problems of components 3.1.1 Interface Specification with the B method A B specification of an interface is composed of the following information:

• The name of the B machine: it is the name of the associated interface.

• The variables of the interface: the set of variables used in the operation definition.

• The initialisation: the initial value of the variables.

• The invariant: describes the property that a component must satisfy in each state.

• The operations: each operation is specified by a precondition and a body which expresses the transformation performed on states by an operation.

Protocol specification

In the B method, it is not possible to specify a particular order of operation calls. Therefore we use the regular language to specify component protocols. We specify a protocol as a set of finite words that are made up over an alphabet which is a set of the called operation names.

A protocol is described by the following formula: (((operation name 1 ).(operation name ′ 1 ). . . .) * + . . . +((operation name i ).(operation name ′ i ). . . .) * + . . .), using the following operators: • ′′ . ′′ expresses the sequencing in the operation calls. For example (operation name 1 . operation name 2 ) means that the operation name 1 will be called before the operation name 2 ,

• ′′ + ′′ expresses the choice. For example (operation name 1 + operation name 2 ) means that either the operation name 1 or the operation name 2 will be called,

• ′′ * ′′ is used to express the repetition. For example (operation name 1 . operation name 2 ) * means that the operation name 1 and the operation name 2 will be called a finite number of times.

Case Study: a car windscreen wiping system

We illustrate our approach by considering a car windscreen wiping system [START_REF] Kouchnarenko | Refinement and verification of synchronized component-based systems[END_REF]. This system receives messages from an environment, a car driver, and activates the windscreen wiper. It has two operational modes:

• manual: the car driver selects the speed for the windscreen wiper. Then the wiping system receives messages from the car driver and sends messages in order to activate the windscreen wiper with the selected speed,

• automatic: the wiping system is activated by the car driver and the selection of the speed for the windscreen wiper is done automatically according to the quantity of the detected rain.

The wiping system can send messages to activate the windscreen wiper with three different speeds: the first speed, the intermediate speed and the second speed.

In order to construct this system, we dispose of three components provided by different software designers. The components are:

• the control lever CLever component,

• the windscreen wiper WWiper component,

• the rain sensor RSensor component.

The CLever component

It allows to detect the mode of the wiping system selected by the car driver, automatic or manual. In the first mode, the component CLever sends a message to activate the automatic mode for the wiping system. In the second mode, the car driver can select two speeds for the windscreen wiper:

• speed1: the component CLever sends a message to the environment in order to activate the first speed for the windscreen wiper,

• speed2: the component CLever sends a message to the environment in order to activate the second speed for the windscreen wiper.

Remark 3.1 Note that the component CLever does not offer the possibility to select the intermediate speed for the wiping system.

The component CLever has three interfaces: the offered interfaces OIManual and OIAutoCL, and the used interface UICLever. We only describe the offered interface OIManual. The B specification of this interface is given in figure 1. The operations defined in the interface OIManual are:

• Cl Speed1: the car driver activates the first speed for the wiping system.

• Cl Speed2: the driver activates the second speed for the wiping system.

• Cl Stop: the driver stops the wiping system.

The protocol that must be respected by the operation calls in the interface OIManual is:

(Cl Speed1.(Cl Speed2.Cl Speed1) * .Cl Stop) * .

The WWiper component

It receives messages from the environment and activates (with the first, the second or the intermediate speed) or stops the windscreen wiper. This component has three interfaces, the used interfaces UIManual and UIAu-toWW, and the offered interface OIWWiper. We only describe the used interface UIManual. The B specification of this interface is given in figure. The operations defined in the interface UIManual are:

• Cl Stop, Cl Speed1, Cl Speed2: these operations have the same description as those described in the interface OIManual,

• Cl Speedi: the driver activates the intermediate speed for the wiping system.

The protocol that must be respected by the operation calls in this interface is:

((Cl Speedi.Cl Stop) * . (Cl Speed1.(Cl Speed2.Cl Speed1) * .Cl Stop) * . (Cl Speedi.Cl Stop) * ).

The RSensor component

It is operational in the automatic mode of the wiping system. It allows to detect the quantity of rain and to send messages to its environment in order to activate the windscreen wiper with the appropriate speed. it can detect three cases: there is no rain, there is little rain and there is big rain. This component is described by the offered interface OIAutoRS and the used interface UIAutoRS.

The wiping system

The architecture of the wiping system using these three components is proposed in figure 3. It is described using UML 2 notations [START_REF] Doldi | UML 2 Illustrated -Developing Real-Time & Communications Systems[END_REF].

Verification of component interoperability

In order to verify the component interoperability, it is necessary to treat two cases:

• verification of component compatibility: verify whether two software components can be related.

• verification of component substitutability: verify whether a component can be replaced by another component.

Verification of component compatibility

To determine whether two components can interoperate, we propose a compatibility verification between offered and used interfaces because components interoperate via these interfaces. We use the B theorem prover, and the operational semantics of the interface specifications (transition systems) of offered and used interfaces to perform the verification. We split the verification approach into two steps:

• Invariant verification: since we define an invariant in the interfaces, we must verify that the invariant provided in the used interface is satisfied by the specification of the appropriate offered interface.

• Verification of interface compatibility at signature, semantics and protocol levels between an offered and used interfaces: to verify that required services described by a used interface are compatible with offered services described by an offered interface, it is necessary to verify the compatibility between these interfaces. Therefore, we verify that the component behavior described by an offered interface simulates the component behavior described by the corresponding used interface.

We illustrate our verification approach by checking whether the component CLever interoperates with the component WWiper via the interfaces OIManual and UIManual.

Invariant verification

In order to insure that the component CLever can interoperate with the component WWiper via the offered interface OIManual and the used interface UIManual, we must prove that the operations specified in the interface OIManual satisfy the invariant I u specified in the interface UIManual. Since we specify interfaces using the B method, we use the B theorem prover to perform this verification. The verification will be performed on a new B specification obtained by modifying the OIManual specification and taking into account information provided by UIManual. So, we describe below two steps allowing to construct a B specification where the invariant I u is specified and also the operations of the offered interface OIManual are specified. This new specification is obtained as follows:

• We modify the invariant of the interface OIManual : The invariant of the new specification is I o ∧ I u , where I o is the invariant of the interface OIManual.

• We add in the specification of OIManual variables and sets of UIManual which are not defined in OIManual. If there exists a set S which is defined in the interface OIManual and in the interface UIManual with more variable values, then we replace the set S in OIManual by the set S of UIManual (see the example below). Finally, initialize the new variables defined in the specification of OIManual.

After carrying out these two steps, we obtain a new B specification presented in figure 4 in which the value sp i has been added in the set CL P osition. We did not change the invariant of the interface OIManual because this interface has the same invariant as the one defined in UIManual. The verification with the B theorem prover shows that the new B specification is valid, which means that the operations preserves the invariant. Therefore the operations of the offered interface OIManual satisfy the invariant provided by the used interface UIManual. 4.1.2 Verification of interfaces compatibility at signature, semantics and protocol levels The verification of the compatibility between the offered interface OIManual and the used interface UIManual is based on verifying that the component behavior described by the B specification of the offered interface and its protocol simulates the component behavior described by the B specification of the used interface and its protocol.

The steps which compose this verification approach are:

• Construction of the transition systems that capture the component behavior described in the specification of offered and used interfaces: we exploit the protocol specifications and the B specification of the interfaces to construct these transition systems.

• Verification of the interface compatibility by defining and verifying the relation of simulation between the transition systems obtained in the above step.

Construction of the transition systems corresponding to the interface specifications: The protocols specified in the interfaces OIManual and UIManual are respectively:

• (Cl Speed1.(Cl Speed2.Cl Speed1) * .Cl Stop) * . These protocols are specified with a finite regular language which has the alphabet composed of operation names specified in the interfaces. According to the Kleene theorem [START_REF] Kleene | Representation of events in nerve nets and finite automata[END_REF], we can model these protocols with finite transition systems [START_REF] Arnold | Mec: a system for constructing and analysis transition systems[END_REF].

The transition systems do not express the total behaviors described in the interfaces, because the values of their states are not significant. Indeed, they only present the information at the levels of operation signature and protocols but not at the level of the semantics of the operation (their pre and postconditions). Therefore, we enhance these transition systems by changing the values of their states. We use the B specification of the interfaces in order to decorate the states of the transition systems by a set of atomic propositions that correspond to pre and postconditions of the operations. The approach of constructing the transition systems is presented as follows:

propositions which are the equality between the variables and their values.

• From the operations of the B specification of an interface, we decorate the other states by a set of atomic propositions which are the equality between the variables and their new values. The values of variables in a state s i , such that t def = s i-1 op → s i is a transition, are obtained by applying the generalised substitution of the operation op on the variables of the state s i-1 .

By applying our approach on the previous example, we obtain the transition systems T S o (see figure 5) and T S u (see figure 6) that model both behaviors of software components described respectively by the offered interface OIManual and the used interface UIManual. These transition systems allow to know all the authorized behaviors for the component CLever corresponding to the specification of the interfaces OIManual and UIManual.

The transition system T S o def = S 0o , S o , → o , L o , F o is composed of the following information:

• the initial states: S 0o = {s 0 }

• the set of states: S o = {s 0 , s 1 , s 2 }

• the transition relation → o expressed by the following set of transitions:

{s 0 Cl Speed1 → s 1 , s 1 Cl Speed2 → s 2 , s 2 Cl Speed1 → s 1 , s 1 Cl Stop → s 0 } • the labelling function L o defined by: L o (s 0 ) = {cl pos = stop}, L o (s 1 ) = {cl pos = sp 1 }, L o (s 2 ) = {cl pos = sp 2 }
• the set of the final states: The transition system T S u def = S 0u , S u , → u , L u , F u is composed of the following information:

F o = {s o }.
• the initial states: relation of Milner [START_REF] Milner | Communication and Concurrency[END_REF]. A transition system T S 0 simulates a transition system T S 1 according to the Milner definition if and only if the system behavior described by T S 1 is included in the system behavior described by T S 0 .

S 0u = {s ′ 0 } • the set of states: S u = {s ′ 0 , s ′ 1 , s ′ 2 , s ′ 3 } • the transition relation → u expressed by the following set of transitions: {s ′ 0 Cl Speed1 → s ′ 1 , s ′ 1 Cl Speed2 → s ′ 2 , s ′ 2 Cl Speed1 → s ′ 1 , s ′ 1 Cl Stop → s ′ 0 , s ′ 0 Cl Speedi → s ′ 3 , s ′ 3 Cl Stop → s ′ 0 } • the labelling function L u is defined as follows: L u (s ′ 0 ) = {cl pos = stop}, L u (s ′ 1 ) = {cl pos = sp 1 }, L u (s ′ 2 ) = {cl pos = sp 2 }, L u (s ′ 3 ) = {cl pos = sp i } • the set of the final states: F u = {s ′ o }.

Verification of the relation of simulation: We define a relation of simulation between two transition systems as an adaptation of the definition of the simulation

In our case, we need to take into account the transition labels in order to verify components compatibility. In Milner's definition the transition are not labelled. • Compatibility at signature and semantics levels: the operations described in OI and U I are expressed in T S o and T S u by transitions. Source and target states of these transitions are decorated with a set of atomic propositions which expresses respectively pre and postconditions of the operations. Furthermore transitions are labelled with operation names. According to Definition 1 and Definition 2, the verification of the simulation relation implies the verification of the matching of transitions between T S o and T S u at signature and semantics (operation names, pre and postconditions) levels. This involves the verification of the compatibility at signature and semantics levels. ✷

Definition 1 Let T S o = S 0o , S o , → o , L o , F o and T S u = S 0u , S u , → u , L u , F u be two transition systems. Let R be a relation between S u S o , R ⊆ S o × S u . R is a relation of simulation iff for each couple of states (s i , s ′ i ) ∈ S o × S u we have: • if (s i , s ′ i ) ∈ R, then L u (s i ) ⊆ L o (s ′ i ) • if (s i , s ′ i ) ∈ R and s ′ i a → s ′ i+1 ∈→ u ,
Case study: In order to verify that the interface OIManual is compatible with the interface UIManual, we must verify that the relation of simulation R holds between the two transition systems T S o and T S u . The verification requires the parallel exploration of the transition systems T S o and T S u by beginning from their initial states. Therefore, the proof that T S o simulates T S u is the proof that the initial states (s 0 , s ′ 0 ) ∈ R such that s 0 is the initial state of T S o and s ′ 0 is the initial state of T S u .

We illustrate the verification algorithm of the simulation relation by verifying whether T S o simulates T S u as follows:

• verify the first condition of the relation on the couple (s 0 , s ′ 0 ): the condition is verified because

L o (s 0 ) = L u (s ′ 0 ), • verify the second condition on (s 0 , s ′ 0 ): there is a transition s ′ 0 Cl Speedi → s ′ 3 ∈→ u in T S u , but there is not a transition s 0 Cl Speedi → s 3 ∈→ u such that (s 3 , s ′ 3 ) ∈ R. Therefore (s 0 , s ′ 0 ) ∈ R.
The verification of the simulation relation between the transition systems T S o and T S u shows that T S o does not simulate T S u . That means that the interfaces OIManual and UIManual are not compatible. Therefore, the behavior required by the component WWiper is not offered by the component CLever. The verification fails because the component WWiper requires the operation Cl Speedi that is not offered by the component CLever (see the dashed transition in the transition system T S u in figure 6).

Verification of component substitutability

To determine whether a defective component can be substituted by another component, we propose an approach based on the verification of the relation of equivalence between component specifications. This approach allows to determine whether the behavior of the defective component is equivalent to the behavior of the substitute component.

In order to illustrate this approach, we present in the figure 7 two components control lever CLever and CLever'. Suppose that we need to replace the component CLever by the component CLever'. To reach this goal, the component CLever' must satisfy the following constraints: To check this constraint it is necessary to verify the equivalence between component behaviors described in the used interfaces of CLever and CLever'. In our example (see figure 7), we verify that the behavior described in the interface UClever is equivalent to the one described in the interface UClever'.

• The set of the services offered by the component CLever' must be the same as the set of the services offered by the component CLever. To check this constraint it is necessary to verify the equivalence between component behaviors described in the offered interfaces. In our example, we verify that the behavior described in the interface OIManual is equivalent to the one described in the interface OIManual', and we also verify that the behavior described in the interface OIAutoCL is equivalent to the one described in the interface OIAutoCL' .

To verify the equivalence between the component behaviors, we propose an approach based on the B method and on a relation between transition systems. This approach is divided into two steps:

• Equivalence between invariants: we verify the equivalence between the invariants defined in the offered interfaces and between the invariants defined in the used interfaces. In our example, we verify that the invariant defined in the offered interface OIManual is equivalent to the invariant defined in the interface OIManual'. We use the B theorem prover and the B specification of the interfaces to perform this verification.

• Equivalence between component interfaces: in this step, we verify the equivalence between component behaviors described in the offered interfaces and the equivalence between component behaviors described in the used interfaces.

In the example in figure 7, we verify equivalence between component behaviors described in OIManual and OIManual', and between OIAutoCL and OIAutoCL'.

We also verify equivalence between component behaviors described in UClever and UClever'. To perform this verification we define and we check the relation of bisimulation (this relation is defined in the next paragraph) between the transition systems that model the component interfaces (relation of bisimulation between offered interfaces and between used interfaces). So, we verify that the relation of bisimulation holds between the following transition systems • the transition systems describing the offered interfaces OIManual and OIMan-ual', • the transition systems describing the offered interfaces OIAutoCL and OIAu-toCL', • the transition systems describing the used interfaces UClever and UClever'.

In the following, we define the relation of bisimulation between transition systems. This relation is based on the relation of simulation defined in the last section.

A transition system T S ′ bisimulates a transition system T S if and only if the system behavior described by T S ′ is the same as ( we say also that is equivalent) to the system behavior described by T S.

Definition 3 Let T S = S 0 , S, →, L, F and T S ′ = S 0 ′ , S ′ , → ′ , L ′ , F ′ be two transition systems. Let R be a relation of simulation between S and S ′ . Let α be another relation between S and S ′ , α ⊆ S × S ′ . α is a relation of bisimulation iff for each couple of states (s i , s

′ i ) ∈ S × S ′ we have: if (s i , s ′ i ) ∈ α, then (s i , s ′ i ) ∈ R and (s ′ i , s i ) ∈ R
′ , α ⊆ S × S ′ . T S ′ bisimulates T S iff ∀s 0 .(s 0 ∈ S 0 ⇒ ∃s ′ 0 .(s ′ 0 ∈ S ′ 0 ∧ (s 0 , s ′ 0 ) ∈ α))
According to Definition 4, the transition T S ′ bisimulates the transition system T S if and only if the bisimulation relation holds between their initial states.

Related Work

Several works have been proposed in the context of specifying component interfaces and verifying their compatibility.

Cheesman and Daniels [START_REF] Cheesman | UML Components -A Simple Process for Specifying Component-Based Software[END_REF] propose to specify component interfaces using UML [START_REF] Rumbaugh | Unified Modeling Language Reference Manual[END_REF] and OCL [START_REF] Warmer | The Object Constraint Language: Precise Modeling with UML[END_REF] notations. The interface specification includes: an information model that provides the type of the information expressed in the interfaces (it is specified using UML class diagram), invariants on the information model, and operation specifications that express operation signatures and pre-and postconditions. However this work does not propose any verification approach of interface compatibility.

Yellin and Storm [START_REF] Yellin | Protocol specifications and component adaptors[END_REF] propose a state machine based approach to specify protocols. Protocols are expressed in terms of abstract states and transitions. We are inspired by this work in order to model protocols. In contrast with our proposition, the approach of Yellin and Storm does not cope with the component interoperability at the semantics level but only at the protocol level.

Canal and al [START_REF] Canal | Extending CORBA interfaces with protocols[END_REF] use a subset of the polyadic pi-calculus to deal with component interoperability only at the protocol level. The pi-calculus is very well suited for describing component interactions. The limitation of this approach is the low-level description of the used language and its minimalistic semantics which does not provide rich feedback to system designers when errors are detected during protocol checks.

In [START_REF] Bastide | Formal specification and prototyping of CORBA systems[END_REF], Bastide et al use Petri nets to specify the behavior of CORBA objects, including operation semantics and protocols. This work correlates with our approach because we use transition systems that can be expressed as Petri nets, to express component behaviors. The difference to our approach is that we take into account the invariant in the interface specifications and we use the B approach to verify interface compatibility.

In [START_REF] Han | Temporal logic based specification of component interaction protocols[END_REF], J. Han specifies protocols with a temporal logic based approach. This approach leads to a rich specification for component interfaces.

Alfaro and Henzinger [START_REF] Alfaro | Interface automata[END_REF] propose an interesting approach which allows the verification of the interfaces compatibility based on the automata and game theories. This approach is well suited for checking the interface compatibility at the protocol level.

In [START_REF] Zaremski | Specification matching of software components[END_REF], Zaremski and Wing propose an interesting approach to compare two software components. It determines whether one component can be substituted for another. They use formal specifications to model the behavior of components and exploit the Larch prover to verify the specification matching of components.

The approaches described above treat the component interoperability at the semantics and the signature levels, or at the protocol level, not both. However, in this paper we propose an approach which handles the component interoperability and component substitutability at the both levels.

An interesting approach proposed in [START_REF] Smith | Specification, refinement and verification of concurrent systems -an integration of Object-Z and CSP[END_REF], allows to formally specify, refine and verify component based systems. It is based on Object-Z language and the process algebra CSP. The main difference with our approach is the specification language. In our case, we have chosen the B method to specify component interfaces in order to exploit the B theorem prover.

Conclusion

This paper presents an approach to verify component interoperability. We have considered two cases in the interoperability: component compatibility and component substitutability. This approach is based on the use of the B method for specifying component interfaces. An interface specification provides the following information:

• an initialization predicate which provides initial states of a component

• a list of operations, specified by means of their preconditions and generalized substitutions

• an invariant property that must be respected by the initialization predicate and the operations.

Specification of interfaces is enhanced by the specification of protocols with finite transition systems.

The approach to verify the component compatibility is composed of two steps. First, we verify with the B theorem prover that the invariant specified in a used interface is satisfied by the specification of the appropriate offered interface. Sec-ond, we use protocol specifications and B specification of interfaces to complete the verification of interface compatibility at the signature, semantics, and protocol levels by verifying the simulation relation between the transition systems that model component behaviors.

The approach to verify the component substitutability is based on the B method and the verification of the relation of bisimulation between transition systems that models offered interfaces and between transition systems that models used interfaces (interfaces of the defective component and the substitute component).

  Fig. 1. B machine corresponding to the interface OIManual of the component CLever

Fig. 2 .

 2 Fig. 2. B machine corresponding to the interface UIManual of the component WWiper

Fig. 3 .

 3 Fig. 3. Component architecture of the wiping system

Fig. 4 .

 4 Fig. 4. The new B specification obtained from OIManual and the invariant of UIManual

•

  ((Cl Speedi.Cl Stop) * . (Cl Speed1.(Cl Speed2.Cl Speed1) * .Cl Stop) * . (Cl Speedi.Cl Stop) * ).

Fig. 5 .

 5 Fig. 5. The transition system T So corresponding to the interface OIManual

Fig. 6 .

 6 Fig. 6. The transition system T Su corresponding to the interface UIManual

Definition 2

 2 then there exists s i+1 ∈ S o such that s 1 a → s i+1 ∈→ o and (s i+1 , s ′ i+1 ) ∈ R. After defining the relation of simulation between the states of transition systems, we define what it means that a transition system simulates another transition system. Let T S o = S 0o , S o , → o , L o , F o and T S u = S 0u , S u , → u , L u , F u be two transition systems. Let R be a relation of simulation between S u and S o , R ⊆ S o × S u . T S o simulates T S u iff ∀s ′ 0 .(s ′ 0 ∈ S 0u ⇒ ∃s 0 .(s 0 ∈ S 0o ∧ (s 0 , s ′ 0 ) ∈ R)) According to Definition 2, the transition T S o simulates the transition system T S u if and only if the simulation relation holds between their initial states. Theorem 4.1 Let T S o and T S u be two transition systems that model respectively an offered interface OI and a used interface U I. When the relation of simulation R holds between the states of T S o and T S u , then the interfaces OI and U I are compatible at signature, semantics and protocol levels. Proof. Suppose that T S o simulates T S u . • Compatibility at protocol level: T S o and T S u model respectively the interfaces OI and U I. The specification of these interfaces includes the B specification and the protocol specification. According to Definition 1 and Definition 2, the verification of the simulation relation is based on the parallel exploration of the transition systems T S o and T S u . Thus we verify that the traces of the paths explored in T S u are contained in the traces of the paths explored in T S o . Consequently, verifying the relation of simulation implies verifying whether the set of the operation calls described in U I are included in the set of the operation calls described in OI.

Fig. 7 .

 7 Fig. 7. component substitutability

Definition 4

 4 After defining the relation of bisimulation between the states of transition systems, we define what means that a transition system bisimulates another transition system. Let T S = S 0 , S, →, L, F and T S ′ = S 0 ′ , S ′ , → ′ , L ′ , F ′ be two transition systems. Let α be a relation of bisimulation between S and S

Chouali

• From the clause Initialization of the B specification of an interface, we decorate the initial states of the transition system that model the protocol by a set of atomic

• The set of services required by the component CLever' must be the same as the


F Bouquet
email: bouquet@lifc.univ-fcomte.fr

C Grandpierre
email: grandpierre@leirios.com

B Legeard
email: legeard@leirios.com

F Peureux
email: peureux@leirios.com

N Vacelet
email: vacelet@leirios.com

M Utting

A subset of precise UML for Model-based Testing

Keywords: D.2.1 [Requirements/Specifications] D.2.5 [Testing and Debugging] Reliability, Verification Model-Based Testing, UML, OCL

This paper presents an original model-based testing approach that takes a UML behavioural view of the system under test and automatically generates test cases and executable test scripts according to model coverage criteria. This approach is embedded in the LEIRIOS Test Designer tool and is currently deployed in domains such as Enterprise IT and electronic transaction applications. This model-based testing approach makes it possible to automatically produce the traceability matrix from requirements to test cases as part of the test generation process. This paper defines the subset of UML used for model-based testing and illustrates it using a small example.

INTRODUCTION

There are several views of model-based testing: for example the generation of test cases from an environment model (see e.g. [START_REF] Prowell | JUMBL: A Tool for Model-Based Statistical Testing[END_REF] based on a usage profile statistical model) or the generation of test cases with oracles from a behaviour model (see [START_REF] Utting | Practical Model-Based Testing -A tools approach[END_REF] for more details on model-based testing approaches). In this paper, we define model-based testing as a process to automatically generate test cases and executable test scripts from a behaviour model of the system under test (SUT). The model formalizes the expected behaviour to be tested on the SUT. Generated tests are sequences of operation invocations on the SUT, and include the expected output (the oracle information), so that test verdicts can be assigned automatically during test execution [START_REF] Bernard | Model-based Testing from UML Models[END_REF]. Moreover, each behaviour of the SUT model can be labelled with a particular requirement identifier, which makes it possible to generate a traceability matrix that links the generated tests to the initial requirements of the informal specification [START_REF] Bouquet | Requirement Traceability in Automated Test Generation -Application to Smart Card Software Validation[END_REF].

The Unified Modeling Language1 (UML) is widely used as a modelling support for model-based testing. There are several reasons for this interest. Firstly, UML provides a large set of diagrammatic notations for modelling purposes, with several complementary representations. A static representation (i.e. class diagrams) is used to model the points of control and observation of the SUT and the data that represents the abstract state of the SUT. A dynamic representation (e.g. state diagrams or activity diagrams) is used to model the expected behaviour of the SUT. Secondly, the Object Constraint Language (OCL [START_REF] Warmer | The Object Constraint Language Second Edition: Getting Your Models Ready for MDA[END_REF]) associated with UML makes it possible to have precise models -this means that the expected behaviour can be formalized using OCL. Thirdly, UML is the de-facto industrial standard for modelling enterprise IT applications; most software engineers have had some first level training on UML -this is an important point to facilitate the acceptance of a disruptive process such as model-based testing.

However, UML contains a large set of diagrams and notations, defined in a flexible and open-ended way using a meta-model 2and with some freedom allowed for different interpretations of the semantics of the diagrams by different UML tools. So for practical model-based testing it is necessary to select a subset of UML and clarify the semantics of the chosen subset so that model-based testing tools can interpret the UML models.

The paper defines a subset of UML 2.1 (the latest version of UML) for model-based testing purposes. This subset allows formal behaviour models of the SUT to be designed, which can be mechanically interpreted to generate test suites. The subset uses class, instance and state diagrams, plus OCL expressions. Such UML models are used as input for a model-based test generator, called LEIRIOS Test Designer, that automates -using theorem prover technology -the generation of test sequences, covering each behaviour in the model. This paper is organized as follows. Section 2 introduces the subset of UML and OCL we are proposing. Section 3 shows on a small Stack example how this notation can be used to develop a behaviour model for test generation purposes, and exhibits the generated test cases. Section 4 discusses some related work and Section 5 gives conclusions. One of the main contributions of the paper is to identify a subset of UML that is expressive enough to model a variety of industrial applications, and has a clear semantics that allows executable models to be written for test generation purposes. Another contribution is a novel active/passive interpretation of OCL expressions that allows OCL to be used as an action language in UML state machines and class diagrams.

A UML SUBSET

In this section, we define the UML subset we propose for modelbased testing. The goal of this subset is to offer precise, necessary and sufficient modelling features to design behaviour models for test generation purposes. We call this subset UML-MBT.

UML diagrams

The proposed subset for model-based testing is based on three diagrams: UML class diagrams (to model the points of control and observation of the SUT), object diagrams (to define test data), state-machines and OCL 3 (to model dynamic behaviour of the SUT). UML offers several other diagrams, but these are sufficient to design comprehensive, precise and interpretable models to test finite state systems with our tool. To model dynamical behaviour, we use state machine rather than UML sequence diagrams because state machines allow richer behaviours to be specified, with better support for loops and alternative paths. This section defines the subsets of these UML diagrams that are used to design UML-MBT models for automated test generation.

Class diagrams

The UML class diagram is the static view of the model. It describes the abstract objects of the system and their dependencies. The UML elements available to model the class diagram are the following elements:

• Classes define the types of the objects of the system.

Inheritance is not yet implemented. For integers, a restricted domain is recommended for testing purposes (for example the integer interval [-32668, 36767]). Object types are represented using 1-1 associations, rather than attributes. • Operations model the actions owned by an object. An operation can be defined with parameters (input and output) that can be typed as Boolean, integer, enumeration literal or object. OCL preconditions and postconditions can be used to formalise the behaviour of an operation.

Object diagrams

The UML object diagram lists the concrete objects used to compute test cases, and defines the initial state of the model. Each object diagram must be an instantiation of the associated class diagram. Notice the following restriction: objects can not be created or deleted dynamically by the actions designed in the model. So all objects used to describe the life cycle of the system must be defined in the object diagram. The dynamic creation (resp. deletion) of entities in the concrete system is simulated by creation (resp. deletion) of links between objects in the UML model. The following UML elements can be used in object diagrams:

• Objects, or class instances, are the concrete objects of the system that are used in the generated tests. Every slot -or attribute instance -of every object must have a value. • Links, or association instances, define the dependencies between the objects in the initial state of the system.

State-machines

State-machine diagrams are an optional part of a UML-MBT model. They are used to model the dynamic behaviour of the SUT as a finite state transition system. The UML state machines used in UML-MBT may contain the following elements:

• initial (and optionally final) states,

• simple states, used to define the different system states of the SUT lifecycle, • single transitions, used to model SUT actions. Transitions may be between two states, reflexive, or internal. A transition is composed of :  an optional event (optionally defined with input parameters that can be typed as Boolean, integer, enumeration literal or object) that triggers the transition,  an optional guard that is a Boolean expression used to determine whether or not the transition can fire,  an optional action that updates the model data.

The semantics of state machine processing is based on the UML run-to-completion processing assumption. Run-to-completion processing means that an event occurrence can only be taken from the pool of operations declared in the class diagram. Moreover, this event can be dispatched only if the processing of the previous current occurrence is fully completed (to avoid concurrency conflicts during the processing of events). The processing of a single event occurrence by a state machine is known as a run-tocompletion step. Before commencing on a run-to-completion step, a state machine has to be in a stable state configuration (a state in which no more transitions can be fired without external events). Thus, an incoming event will never be processed while the state machine is in some intermediate and inconsistent situation. A runto-completion step can also be viewed as a complex state transition between two stable states of the state machine. Just as OCL is used in class diagrams, to formalise the expected behaviour of class operations, OCL is also used within state machines to formalize transitions between states. -the guards and the effects of transitions are expressed as OCL predicates.

OCL 2.0 subset

To be able to execute transition actions and operation postconditions, UML-MBT uses an operational interpretation of OCL expressions used in such contexts. For example the OCL expression self.attribute=true can be used in two different contexts: a passive and an active context. A passive context is used to express constraints on the system under test, while an active context is used to express state changes in the model. So the expression self.attribute=true is interpreted and evaluated as a standard Boolean expression in a passive context. In an active context it is interpreted as an assignment of the value true to the Boolean state variable attribute. We found it necessary to introduce this active/passive operational interpretation of OCL into UML-MBT because of the lack of frame information in OCL. That is, an OCL postcondition such as attribute1=attribute2 states that the two attributes must be equal after the operation, but does not specify the operational details of which attribute (attribute1 or attribute2 or both) was updated in order to satisfy the postcondition. In this section, we explain how UML-MBT classifies each OCL Boolean expression as being either passive or active, and describe the meaning of each supported OCL operator in each context. This non-ambiguous interpretation of OCL expressions makes it possible to use OCL as an executable action language for modelbased testing UML models.

The two interpretations (passive and active) were described briefly in [START_REF] Utting | Practical Model-Based Testing -A tools approach[END_REF], but are described in detail in Section 2.2.1 and Section 2.2.2. It should be noted that some OCL operators are allowed in both contexts so appear in both sections.

Passive OCL contexts

In UML-MBT, an OCL passive expression is an OCL expression that is used in a passive context. This includes operation preconditions, transition guards, decisions in conditional structures and all sub-expressions of other passive expressions. Passive expressions are used to test the state variables of a model --they do not modify the model state. This section defines the set of all supported OCL passive expressions in UML-MBT.

Boolean operators

Integer operators

Enumeration operators

Collection operators

Collection iterative operators

Active OCL contexts

In UML-MBT, an OCL active expression is an expression that is used in an active context. This includes operation postconditions, transition actions, action in the then or else part of a conditional structure, or a sub-expression of an active expression. Active expressions are used to change the values of state variables and to define values for the return parameter of operations. This section defines the set of all supported OCL active expressions in UML-MBT.

Assignment operator =

OCL uses the equality symbol to compare two elements (e1=e2). However, in an active context, we interpret this operator as an assignment operator. The left hand variable is assigned the value of the right hand expression. Thus this operator becomes noncommutative in an active context. For example the expression self.attribute = true sets the value of self.attribute to the Boolean value true. The assignment operator can be used to update any attribute value, any link and any set of links.

oclIsUndefined / isEmpty operators

In an active context these operators are used to delete linksassociation instances. The operator expr.oclIsUndefined(), where expr refers to an association between classes with multiplicity 1 or 0..1, deletes any existing link and sets expr to null. Similarly, expr.isEmpty(), where expr refers to an association whose maximum multiplicity may be greater than one, deletes all the related links and sets expr to the empty set.

forAll iterative operator

The active expression coll->forAll(expr) operator applies the active expression expr to each object in the collection coll. This is similar to a loop in an imperative language.

and operator

In an active context the operator and acts as a separator between two active expressions.

if-then-else structure

This structure makes it possible to perform conditional execution of active OCL expressions. The basic use is "if condition then action1 else action2 endif", where condition is a Boolean passive expression and action1, action2 are active expressions.

All these active expression operators will be used in the model example given in section 3.

UML/OCL for MBT: key issues

The UML-MBT subset of UML defined in this paper needs specific interpretations in order to manipulate behavioural models and generate tests. We present here some key issues we address when generating tests with UML using the UML-MBT subset.

Model behaviours

The UML-MBT subset allows designing behavioural models. These behaviours are designed in the operation postconditions (in the class diagram) and in the transition actions (in state machines).

A set of consecutive actions -active expressions -defines the model behaviours. A conditional structure makes it possible to model alternative and complex behaviours in a single action or postcondition.

Example 1. Behaviours from operation postcondition

Given the static operation getType -from a class Trianglewhich returns the type of a triangle defined by its sides (a, b and c). This example is a version from the well-known example mentioned in [START_REF] Myers | The Art of Software Testing[END_REF]. The operation expressed with OCL notation is the following: In this postcondition of the "getType" operation, we clearly distinguish the four behaviours of the operation which define the four different triangle types.

The model behaviours allow generating tests on the basis of cause/effects defined via OCL expressions. We call test target a pair cause/effect that corresponds to a path in a post condition of an operation. More precisely, a test target is a pair defining an operation (or action linked to a transition) including the effect of the test target and one target context that makes it possible to produce the effect. For the postcondition of the "getType" operation, the following test targets are computed: In addition, our interpretation of OCL makes it possible to increase or decrease the number of model behaviours, and so the number of test targets. The Boolean keywords true and false used in an active context allow tuning the test target generation. The true keyword used in an active context is interpreted to mean skip (that is, no change), while the false keyword is interpreted to mean infeasible behaviour, so no test targets will be produced for any path through an OCL active expression that contains false. These active interpretations of true and false are typically used in one branch of a conditional structure, to control test generation. Notice that both branches of an OCL if-then-else structure must always be filled, which is why it is sometimes useful to use true or false in one branch.

OCL undefined value

Model-based testing is used to generate concrete tests from an abstract model. So an executable test must be defined with concrete values for each variable or parameter. Now, OCL suggests the specific value undefined to qualify an expression without defined value. This undefined value is similar to the null value in Java. In OCL it can be tested with the special operator oclIsUndefined().

An OCL expression is evaluated to the undefined value in the following cases:

• When the expression coll->any(expr) has no object to return, because there are no objects in coll that satisfy expr. That is, coll->select(expr) is empty. • When the expression exp.role is applied to an empty association (that is, no link is defined between the object expressed by exp and the target object expressed by role). • When a division or a modulo by zero occurs.

An OCL expression is undefined if it contains any subexpression whose value is undefined. That is, all operators are strict in their interpretation of undefined. Note that this is one difference from the usual OCL semantics for Boolean operators, which use a three-valued non-strict interpretation of undefined -the UML-MBT style is to use explicit if-then-else expressions in such cases. This strict interpretation has an effect on the model behaviours and so on the test targets extracted from the model. Thus a test target for which the target context and/or the target effect is evaluated to undefined cannot be reached and so will give no test for the corresponding behaviour. The expression if cond then action1 else action2 endif generates the test targets t1 defined by cond and action1 and t2 defined by not(cond) and action2. If cond is undefined both test targets are unreachable. If action1 is undefined then t1 is unreachable. If action2 is undefined then t2 is unreachable.

Specific ANY operator

The OCL any operator is used on a collection to obtain an arbitrary element of the collection. If several elements satisfy the any expression, the element is chosen non-deterministically. If no element respects the expression, then the any operator returns the undefined value. So our strict interpretation of undefined means that when no object satisfies an any operator, the corresponding behaviour will not be reachable.

In addition, the any operator is normally non-deterministic. The expression coll->any(expr) returns an arbitrary object of coll for which expr is true. However, to ensure reproducibility of test generation the execution of such an expression must always return the same object for the same test. We satisfy these requirements by taking the test context into account when choosing the object to be returned by an any expression. The any operator interpretation is illustrated in the following example.

Example 2. any operator interpretation

Consider a class called A with an integer attribute named attr. Consider three instances, a1, a2 and a3, of the class A, with a1.attr=1, a2.attr=2 and a3.attr=3. Consider the following postcondition expressed in OCL. In this postcondition the first behaviour is reachable, because any(attr>1) is verified by instance a2, the second behaviour is also reachable, because any(attr>1) is verified by instance a3, but the last behaviour is unreachable. However if the any expression was attr<1, no behaviour would be reachable in this postcondition.

The any operator can return different objects (a1 or a2 here), but always the same object for the same behaviour. In the example, a2 is always given to reach the first behaviour; a3 is always given to satisfy the second behaviour.

Requirements traceability

UML-MBT supports the expression of requirements that are external to the model (they usually come from the informal and often textual, specification of the system). A requirement can be related to any effect designed in the operation postconditions or in the transition actions. Such effects are also directly annotated in the OCL constraints with a specific identifier that refers to the expression of the related requirement.

Concretely a requirement is expressed with a specific form of comment block. The start and the end requirement markers are "/*@REQ:" and "@*/". Everything enclosed in this specific comment block is considered to be a declaration of requirements.

The Stack example of the next part illustrates the use of these requirement identifiers to achieve requirement traceability.

APPLICATION EXAMPLE

We propose in this section an example of the application of model-based testing with the UML-MBT set in order to generate tests from a specification modelled with UML/OCL.

In this example, the system under test is a chained stack of generic elements. The stack is loaded via a push operation and is emptied via a pop operation. The elements to push are randomly chosen from a pool of elements. The maximum size of the stack is the constant MAX. A list of functional requirements which must be assumed is given in Table 9.

In addition this example shows the different specific points presented in the previous section.

Requirements

We consider that the system under test has to satisfy the following requirements. The stack is loaded with elements from the pool. The elements are loaded one by one and chosen randomly from the pool. This element is automatically deleted from the pool.

Table 9. Stack Requirements

automatic_reinsertion A popped element is automatically put into the pool.

The Stack Model

We present here a model of the Stack system, designed for test generation purposes. Some modelling choices are discussed too. We have three object types in the system. The stack is composed of chained elements taken from a pool. This pool contains a collection of elements. Notice the use of the isEmpty() operator in an active context in order to empty out the pool. Also notice the two requirements set on these operations: pool_empty and pool_fill.

Class diagram

Initial state

Figure 2 presents the object diagram that depicts the initial state of the system under test.

Figure 2. The initial state of the Stack model

In the initial state, the stack and the pool are empty. The link between the stack and the pool is created. Note the MAX constant, arbitrarily set with 3.

State-machine

Figure 3 presents the state-machine used to describe the different dynamic states of the system under test.

Test targets and generated tests

The test targets computed from the model shown in the previous diagrams are given in Table 10. From these targets we generate the following tests presented in Table 11. More precisely, for each test target, we use an automated theorem prover [8] to search for a path from the initial state to that target, and data values that satisfy all the constraints along that path. This is similar to a symbolic model-checking approach [START_REF] Jéron | Test generation derived from model-checking[END_REF][START_REF] Ammann | Using Model Checking to Generate Tests from Specifications[END_REF]. A test is also composed of:

• a preamble (potentially empty); the sequence of operations called to reach the targeted behaviour, • a body, the execution of the targeted behaviour, • a postamble (potentially empty); the sequence of operations to return to the model initial state.

The generation of postambles is optional.

In the Stack model, the generated tests cover all the behaviours that were modelled, and all the states and transitions of the statemachine.

In addition we can construct the traceability matrix of the requirements that are designed in the model and linked with the test targets.

Note that some tests have no postamble. This means that the model initial state is not reachable from the state, in which the system under test is.

RELATED WORK

They are numerous model-based testing approaches that use UML as modelling notation 4 . Some of them are based on sequence or interaction diagrams to express scenarios (see e.g. [START_REF] Beyer | Automated TTCN-3 Test Case Generation by Means of UML Sequence Diagrams and Markov Chains[END_REF]), state machines to express behaviour models (see e.g. [START_REF] Vieira | Object-Oriented Specification-Based Testing Using UML Statechart Diagrams[END_REF]) or combine them (see e.g. [START_REF] Briand | A UML-Based Approach to System Testing[END_REF]). Few approaches are using OCL as an action language for model-based testing. B. K. Aichernig proposes an approach based on mutation analysis of OCL specifications [START_REF] Aichernig | Percy Antonio Pari Salas: Test Case Generation by OCL Mutation and Constraint Solving[END_REF], and Bruel et al [START_REF] Benattou | Generating Test Data from OCL Specification[END_REF] proposes a combination of test cases using an approach very similar to the test target computation proposed in this paper. But there is currently no subset of UML/OCL clearly proposed for model-based testing.

CONCLUSION

This paper introduced a subset of UML/OCL for model-based testing. In Section 3, we illustrated how this UML-MBT subset of UML can be used to write a precise model of a Stack system, which is executable and a good basis for test generation. The stack model is very small, and it would not be difficult to generate a similar test suite manually -but with larger industrial models many more tests are needed to cover the model, and the cost benefits of model-based testing become more significant. The UML-MBT subset of UML is fully supported by the LEIRIOS Test Designer v3.0 tool (see [START_REF] Bernard | Model-based Testing from UML Models[END_REF][START_REF] Bouquet | Requirement Traceability in Automated Test Generation -Application to Smart Card Software Validation[END_REF]

context:

  Triangle::getType(a:Integer, b:Integer, c:Integer):TYPE pre: a>0 and b>0 and c>0 post: if a+b<=c or a+c<=b or b+c<=a then result = TYPE::NO_TRIANGLE else if a=b or b=c or a=c then if a=b and b=c then result = TYPE::EQUILATERAL else result = TYPE::ISOSCELES endif else result = TYPE::SCALENE endif endif

  post: let obj = A.allInstances()->any(attr>1) in if obj.attr = 2 then result = MSG::MSG1 else if obj.attr > 2 then result = MSG::MSG2 else result = MSG::MSG3 endif endif

  Requirement description pool_empty The pool can be emptied out by one operation pool_fill The pool can be completely filled by one operation empty_stack_exception A pop operation on an empty stack generates an exception full_stack_exception When the stack size equals MAX, a push operation on the stack generates an exception random_element, automatic_delete

Figure 1

 1 Figure 1 presents the class diagram. It depicts the different objects of the system under test and the dependencies between them.

Figure 1 .

 1 Figure 1. The class diagram of the Stack model

Figure 3 .

 3 Figure 3. The state-machine of the Stack model

Table 1

 1 lists the Boolean operators available in the UML-MBT set. In this table p1 and p2 are passive Boolean expressions.

Table 1 . OCL Boolean operators OCL notation Operator Result type

 1

	p1 = p2	equals	Boolean
	p1 <> p2	not equals	Boolean
	p1 or p2	disjunction	Boolean
	p1 xor p2	excl. disjunction	Boolean
	p1 and p2	conjunction	Boolean
	not p1	negation	Boolean

Table 2

 2

lists the integer operators available in UML-MBT. In this table i1 and i2 are integer expressions.

Table 2 . OCL integer operators OCL notation Operator Result type

 2

	i1 = i2	equals	Boolean
	i1 <> i2	not equals	Boolean
	i1 < i2	lesser	Boolean
	i1 > i2	greater	Boolean
	i1 <= i2	lesser or equal	Boolean
	i1 >= i2	greater or equal	Boolean
	i1 + i2	plus	Integer
	i1 -i2	minus	Integer
	-i1	unary minus	Integer
	i1 * i2	multiplication	Integer
	i1.div(i2)	division	Integer
	i1.abs()	absolute value	Integer
	i1.mod(i2)	modulo	Integer
	i1.max(i2)	maximum	Integer
	i1.min(i2)	minimum	Integer

Table 3

 3 lists the enumeration operators available in UML-MBT. In this table e1 and e2 are enumeration literals.

	Table 3. OCL enumeration operators
	OCL notation	Operator	Result type
	e1 = e2	equals	Boolean
	e1 <> e2	not equals	Boolean
	2.2.1.4 Object/Class operators

Table 4

 4 lists the UML-MBT operators applicable to classes or objects (class instances). In this table o1 and o2 are objects and c1 is a class.

	Table 4. OCL class/objects operators
	OCL notation	Operator	Result type
	o1 = o2	equals	Boolean
	o1 <> o2	not equals	Boolean
	o1.oclIsUndefined() is null	Boolean
	c1.allInstances()	get all instances	Set

Table 5

 5 lists the collection operators available in UML-MBT. In this table s1 and s2 are sets of objects and o1 is an object.

	Table 5. OCL collection operators
	OCL notation	Operator	Result type
	s1 = s2	equals	Boolean
	s1 <> s2	not equals	Boolean
	s1->size()	size	Integer
	s1->includes(o1)	includes	Boolean
	s1->excludes(o1)	excludes	Boolean
	s1->includesAll(s2)	includes all	Boolean
	s1->excludesAll(s2)	excludes all	Boolean
	s1->isEmtpy()	is empty set	Boolean
	s1->notEmpty()	is not empty set	Boolean
	s1->including(o1)	including	Set
	s1->excluding(o2)	excluding	Set

Table 6

 6

lists the collection iterative operators available in UML-MBT. In this table s1 is a set of objects, p1 is a passive Boolean expression and o1 must be the name of an association link in the class diagram. Note that the expression s1->collect(o1) can also be written more simply as s1.o1.

Table 6 . OCL collection iterative operators

 6

	OCL notation	Iterative operator	Result type
	s1->collect(o1)	collect	Set
	s1->select(p1)	select	Set
	s1->exists(p1)	exists	Boolean
	s1->forAll(p1)	for all	Boolean
	s1->any(p1)	any	Object

Table 7 . Test targets of the getType operation Id Target context Target effect 1 a+b<=c or a+c<=b or b+c<=a

 7

	result=
	NO_TRIANGLE

  Table 8 shows the test targets generated from several examples of OCL conditional active expressions.

	Table 8. Test targets from conditional structures
	OCL expression	Test targets Target context Target effect
	if cond then act1	cond	act1
	else act2 endif	not(cond)	act2
	if cond then act1	cond	act1
	else true endif	not(cond)	skip
	if cond then act1 else false endif	cond	act1

! Source du renvoi introuvable

  The state-machine is clearly comprehensive. We can push and pop elements. The different states in which the stack can be are designed in this diagram. The transition actions are defined as follows:Notice the particular use of active expression expressed with operators that are interpreted as mentioned in Erreur

		action popForEmptyStack
		post:
		let element = self.top in
		self.top.oclIsUndefined()
		and self.size = self.size -1
		and self.pool.elements =
		self.pool.elements->including(element)
		/*@REQ:automatic_reinsertion@*/
	action pushOnEmptyStack
	post:
	let element = self.pool.elements->any(true) in self.top = element /*@REQ:random_element@*/ and self.size = self.size + 1 and self.pool.elements = self.pool.elements->excluding(element) /*@REQ:automatic_delete@*/	action popForLoadedStack post: let element = self.top in self.top = element.down and element.down.oclIsUndefined() and self.size = self.size -1 and self.pool.elements =
		self.pool.elements->including(element)
		/*@REQ:automatic_ reinsertion @*/
	action pushOnLoadedStack
	post:
	let element = self.pool.elements->any(true) in
	element.down = self.top
	/*@REQ:random_element@*/
	and self.top = element
	and self.size = self.size + 1
	and self.pool.elements =
	self.pool.elements->excluding(element)
	/*@REQ:automatic_delete@*/

. (oclIsUndefined()). The two requirements random_element and automatic_delete are linked with the actions push*. The requirement automatic_reinsertion is set on the actions pop*. The requirements empty_stack_exception and full_stack_exception are both linked to empty actions, written with the keyword true.

Table 10 . Test targets from the Stack model

 10

	Target definition

Table 11 . Generated tests on Stack model

 11

	Corresponding test

  for more detail on test generation strategies). This test generator takes UML models from Borland Together and IBM Rational Software Modelling tools and provides a plug-in that verifies the compliance of the UML model with the defined UML-MBT subset. It checks the model for OCL syntactic verification and consistency (e.g. verification that the instances verify the corresponding multiplicities in the class diagram). LEIRIOS Test Designer provides adapters to export generated test cases and test scripts in test management and execution tools such as HP/Mercury Quality Center. This UML-based model-based testing solution is currently deployed on large applications in the

UML is a notation from the Object Management Group -See www.omg.org

A meta-model is a language to describe the domains of applicative models and to define their semantic

See "model-based testing" section on Wikipedia to have an updated list of MBT tools -http://en.wikipedia.org/wiki/Model-based_testing domains of Enterprise IT information systems and eTransactions systems (banking, ticketing or e-Admin applications).