Memoire Online - EM-OCL : une extension mathématique d'OCL

Dans ce chapitre nous avons proposé une extension mathématique du langage OCL. Il était alors nécessaire d'examiner l'intégration des nouveaux concepts mathématiques (couples, relations et fonctions) dans le package Types afin de les métamodéliser. Ensuite, nous avons proposé des augmentations liées à la bibliothèque standard d'OCL en proposant les nouvelles classes génériques suivantes : Pair, BinaryRelation, PartialFunction, PartialSurjective, Total-Function, PartialInjective, TotalSurjective, TotalInjective, TotalBijection et PartialBijection.

Dans la suite de ce mémoire, nous proposons des utilisations potentielles de notre extension EM-OCL.

Introduction

Dans ce chapitre, nous proposons trois utilisations potentielles de notre extension mathématiques d'OCL : EM-OCL. La première utilisation concerne le développement incrémental de diagrammes de classes UML basé sur la technique de raffinement à l'instar des méthodes formelles comme B et Event-B. La deuxième utilisation concerne la validation des diagrammes de classes en se basant sur des scénarios plausibles décrits par des diagrammes d'objets. Enfin, la troisième utilisation permet d'exhiber les facilités offertes par EM-OCL en tant que langage de requêtes.

D'une façon informelle, le raffinement est un processus de transformation d'une spécification abstraite en une spécification concrète vérifiant que chaque transformation de spécification préserve bien sa correction vis-à-vis de la spécification précédente. On peut distinguer principalement deux catégories de raffinement : Le raffinement algorithmique (encore appelé raffinement de données) et le raffinement de détails.

Le raffinement algorithmique consiste à choisir une autre représentation mémoire de l'état du système modélisé afin :

- de minimiser l'espace mémoire utilisé et/ou le temps de calcul. Ainsi, le raffinement favorise l'élaboration des solutions efficaces.

- d'aller progressivement, sans se précipiter, vers la représentation ultime. Ainsi, le

Le raffinement de conception ou de détails consiste à spécifier un système de manière plus détaillée.

Le raffinement constitue la pierre angulaire des méthodes formelles comme B, Event-B, Z[8] et Object-Z[9].

Le raffinage a été défini de manière intuitive par J.R. Abrial ainsi "une substitution (travaillant dans le contexte d'une certaine machine abstraite M) est dite raffinée par une substitution T, si T peut être utilisée à la place de S sans que l'utilisateur de la machine s'en rende compte. En pratique, cela signifie que toutes nos attentes au sujet de S seront remplies par T. Si c'est le cas, alors T est dit être un raffinage de S, et S une abstraction de T [3]".

Contrairement aux méthodes formelles comme B et Event-B où le concept raffinement est précisément défini, UML [?] propose la dépendance stéréotypé «refine» ayant une définition très floue et plutôt considérée comme une simple décoration graphique.

Dans cette section, nous exhibons les possibilités offertes par EM-OCL afin d'utiliser la technique de raffinement en UML. Pour y parvenir, nous développons d'une façon incrémentale pas-à-pas en UML/EM-OCL l'application accès aux bâtiments modélisée en Event-B par J.R. Abrial et décrite en [19].

Le premier modèle du système est un modèle très abstrait dans lequel, il n'y aura pas de distinction entre le logiciel et le matériel. L'objectif principal du système est de contrôler l'entrée, la sortie, ainsi que la situation dynamique de la présence des personnes dans les bâtiments. Une simplification du modèle consiste à identifier l'extérieur à un bâtiment (dans lequel toute personne a le droit de se trouver).

- L'impossibilité pour une même personne de se trouver simultanément dans deux bâtiments distincts.(1)

- L'ensemble des personnes n'est pas vide.(5) - L'ensemble des bâtiments n'est pas vide.(6) - Chaque personne est autorisée à pénétrer dans un certain bâtiment (et pas dans d'autres).(7)

La modélisation de ce système est donnée par une seule classe, intitulée AccèsBâtiment, englobant les propriétés du système au fur et à mesure dans la phase de conception, contenant :

- deux attributs personne et bâtiment représentant respectivement l'ensemble des personnes et des bâtiments.

- une relation binaire autorisation représentant l'ensemble des couples "personne,bâtiment" dont chacun relie une personne à un bâtiment où elle est autorisée à se rendre. Une personne est autorisée à aller dans plusieurs bâtiments. De ce fait, il s'agit d'une relation binaire.

- une fonction totale situation représentant l'ensemble des couples "personne,bâtiment" dont chacun relie une personne au bâtiment auquel il se trouve, et représentant la dynamique des gens dans les bâtiments. Le fait qu'il s'agisse d'une fonction correspond à la formalisation de la propriété(2). Et le fait qu'elle soit totale correspond à la propriété(4).

- un attribut univers : l'extérieur est un bâtiment spécial. Dans la sémantique de l'opération de construction initialiser celle-ci se charge d'affecter toutes les personnes concernées au bâtiment univers.

La figure 3.1 représente la classe AccèsBâtiment dans l'étape de la spécification initiale .

Ce modèle doit être complété par la formalisation des contraintes décrites ci-dessus.

inv CS : personne-+notEmpty() inv C6 : bâtiment-+ notEmpty() inv C7 : autorisation-+includesAll(situation)

Une opération de construction intitulée initialiser , jouant le rôle d'un constructeur permettant d'initialiser l'ensemble des propriétés du système.

context AccèsBâtiment::initialiser(per :Set(String),bât :Set(String),aut : BinaryRelation(Pair(String,String)), sit :TotalFunction(Pair(String,String)))

pre: per-+notEmpty() and bât-+notEmpty()and aut-+notEmpty() and sit-+notEmpty()

pre: aut-+forAll(couple :Pair(String,String) | per-+includes(couple.first())and bât-+includes(couple.second()))

pre: sit-+forAll(couple :Pair(String,String) | per-+includes(couple.first())and couple.second()=univers)

post: personne=per and bâtiment=bât and autorisation=aut and situation=sit post: autorisation-+notEmpty()

A ce niveau d'abstraction, une seule transition est observée correspondant à l'entrée d'une personne p dans un bâtiment b. En effet, une personne p ne peut passer d'un bâtiment à un autre, que sip est bien autorisée de se trouver dans b, et si bien entendu, elle n'est pas déjà dans b.

pre: personne?includes(p) and bâtiment?includes(b) pre: situation?imageElt(p)<>b

pre: let couple: Pair(String,String)=Pair[] in autorisation?includes(couple.make(p,b))

post: let couple : Pair(String,String)=Pair[] in situation?includes(couple.make(p,b))

Remarque : Pour des raisons de simplification, nous ignorons dans la suite l'opération initialiser.

Dans cette étape, nous introduisons la communication possible entre les bâtiments. Une contrainte supplémentaire, évidente à respecter qu'un bâtiment ne communique pas avec luimême.(8)

La classe AccèsBâtiment, sera augmentée par l'attribut communication représentant l'ensemble des couples "bâtiment,bâtiment" qui relie chaque bâtiment à un autre avec lequel sensé communiqué. La figure 4.2 représente la classe AccèsBâtiment après premier raffinement.

À ce niveau d'abstraction, le seul événement intéressant est l'événement passer. En effet, les deux bâtiments concernés par le passage d'une personne doivent communiquer entre eux.

pre: let couple: Pair(String,String)=Pair[] in communication-+includes(couple.make(situation-+imageElt(p),b))

pre: let couple: Pair(String,String)=Pair[] in autorisation-+includes(couple.make(p,b))

post: let couple : Pair(String,String)=Pair[] in situation-+includes(couple.make(p,b))

Au cours de deuxième raffinement, nous introduisons les portes à sens unique faisant communiquer les bâtiments entre eux. Une personne peut entrer dans un bâtiment en franchissant une porte que si elle est débloquée pour elle. Les portes peuvent être physiquement bloquées. Elles ne peuvent pas être débloquées que pour une seule personne à la fois autorisée à entrer dans le bâtiment. Ceci peut être exprimée par la propriété suivante : toute personne est admise à franchir une porte faisant communiquer le bâtiment oil elle se trouve à un bâtiment oil elle est autorisée à aller. De plus cette personne ne doit pas être déjà engagée avec une autre porte(P1).

- origine : représentant une fonction totale, qui à chaque porte lui correspond son bâtiment origine.

- destination : représentant une fonction totale, qui à chaque porte lui correspond son bâtiment destination.

- acceptation : représentant une fonction injective partielle reliant chaque personne à la porte à laquelle elle est acceptée de franchir.

À ce modèle vient s'ajouter plusieurs contraintes, qui sont décrites en utilisant B : - L'ensemble des portes n'est pas vide.(9)

- Pour toutes ces portes, les bâtiments origine et destination représentent exactement les couples de bâtiments impliquées dans la relation communication introduite au cours du raffinement précédent. Ceci, peut être formulé comme suit:

- Lorsqu'une porte est débloquée pour une certaine personne, celle-ci se trouve dans le bâtiment d'origine de la porte en question. Ceci, peut être formulé en B par l'expression B suivante : (accepter; origine) ? situation.(11)

- Par ailleurs, la personne pour laquelle une porte est débloquée est bien autorisée à aller dans le bâtiment de destination de cette même porte .Ceci peut être formulé en B de la façon suivante : (accepter; destination) ? autorisation.(12)

inv C10 : communication=(origine-+inverse()-+seqComposition(destination) inv C11 : situation -+includesAll(accepter-+seqComposition(origine))

inv C12 : autorisation-+includesAll(acceptation -+seqComposition(destination))

La propriété (P1) exprimant la condition d'admission d'une personne à franchir une porte donnée , est donné par le prédicat admis, considéré comme un fonction utilitaire en utilisant la construction def.

situation ?imageElt(p)=origine?imageElt(po) and autorisation?includes(couple.make(p,b)) and acceptation ?dom()?(p))

débloquer.Une porte po est débloquée pour une personne pe que si cette dernière est admise à franchir po. Par conséquent, elle sera acceptée.

pre: personne ? includes(p) and bâtiment ? includes(b) pre: admis(pe,po)

post: let couple : Pair(String,String)=Pair[] in acceptation ?includes(couple.make(p,po))

refuser.Une personne pe est refusée de franchir une porte po que si elle n'est pas admise à y franchir.

context AccèsBâtiment::débloquer(p :String,po :String) pre: personne?includes(p) and porte?includes(po) pre: vrt?union(rge)? excludes(po)

L'événement passer est raffiné. Il peut se déclencher lorsqu'une personne est admis à entrer et que la porte est débloquée. Les actions associées sont le passage de la personne admise et la fermeture de cette porte. Ce raffinement s'accompagne d'un changement de paramètres de l'événement passer, le bâtiment est remplacé par une porte.

post: let couple :Pair(String,String)=Pair[] in situation?includes(couple.make(p,destination?imageElt(po)))

Dans cette étape de raffinement, on introduit les voyants lumineux dans le système. Un voyant vert est associé à chaque porte. Il est allumé tant que celle-ci est débloquée(14). Dès qu'une personne est passée, la porte se rebloque. Si au bout de 30 secondes, aucune personne ne passe une porte débloquée, celle-ci se rebloque toute seule. Dans les deux conditions, le voyant vert s'éteint.

De même, un voyant rouge est associé à chaque porte. Il est allumé et éteint dans les conditions suivantes :"Le voyant rouge d'une porte dont l'accès vient d'être refusé s'allume pour une période de 2 secondes, la porte restant évidement bloquée".

Une propriété, évidente à respecter, correspond à l'exclusion mutuelle pour les deux voyants soient allumés simultanément (14).

- vrt : représentant l'ensemble des portes dont les voyants verts sont allumés.

- rge : représentant l'ensemble des portes dont les voyants rouges sont allumés.

La figure 3.4 représente la classe AccèsBâtiment après troisième raffinement.

- Le codomaine de la fonction acceptation, correspond à toutes les portes qui sont engagées dans le processus éventuel de passage d'une certaine personne qui, cependant, n'est pas encore passée. Ceci est formalisé, en utilisant la notation B par :vrt = ran(accepter). Cette définition correspond partiellement à la formulation de la propriété (14).

- Par simultanéité, on introduit l'ensemble des portes dont le voyant rouge est allumé.

Les voyants verts et rouges d'une même porte ne peuvent pas être allumés simultané-

- La formulation de la contrainte (14), en notation B, est donnée par: vrtnrge = .

A ce niveau d'abstraction, deux nouveaux événements s'ajoutent au système. rebloquer.permet d'éteindre le feu vert d'une porte;

context AccèsBâtiment::débloquer(p :String,po :String) pre: personne ? includes(p) and porte? includes(po) pre: (vrt ? union(rge))?excludes(po)

post: let couple : Pair(String,String)=Pair[] in acceptation? includes(couple.make(p,po))

pre: personne ? includes(p) and porte? includes(po) pre: (vrt ? union(rge))?excludes(po)

pre: situation ? imageElt(acceptation?inverse(po))=destination ?imageElt(po) pre: not(admis(pe,po))

Chaque personne dispose d'une carte magnétique. Des lecteurs de cartes sont installés à chaque porte permettant de lire les informations contenues sur une carte. Ces informations seront par la suite transmise au micro-ordinateur de contrôle au moyen de message véhiculé par le réseau. De plus, chaque lecteur de carte est supposé resté bloqué entre le moment ou le contenu d'une carte est envoyé au système et la réception par ce lecteur de l'acquittement correspondant. Cet acquittement vient lorsque le protocole de passage est entièrement achevé(avec succès ou non).

- LBL : l'ensemble des lecteurs bloqués. Ceci est représenté par un ensemble des portes.
- mLe : l'ensemble des messages envoyés des lecteurs vers le système de contrôle,

représentée par les couples "portes,personnes" formant ainsi une fonction partielle

représentant l'information lue par le lecteur asocié à la porte sur la carte. - mLa : l'ensemble messages d'acquittement.

La figure 3.5 représente la classe AccèsBâtiment après troisième raffinement.

context AccèsBâtiment::débloquer(pe : String,po String) pre: personne? includes(pe) and porte? includes(po)

pre: let couple: Pair(String,String)=Pair[] in mLe? includes(couple.make(po,pe))

pre : let couple : Pair(String,String)=Pair[] in mLe-+ includes(couple.make(po,pe))

pre : acceptation = acceptation@pre-+soustractionDomaine(po) post : mLa= mLa@pre-+ union(po)

pre : acceptation = acceptation@pre-+ excludes(po) post : mLa= mLa@pre-+ union(po)

pre : situation -+ imageElt(acceptation -+inverse(po))= destination -+imageElt(po) post : acceptation= acceptation@pre-+soustractionRange(po)

context AccèsBâtiment::LECTURE(pe :String,po :String) pre : personne-+ includes(pe) and porte-+ includes(po) pre : LBL= @LBL-+union(po)

post : let couple : Pair(String,String)=Pair[] in mLe= @mLe-+union(couple.make(po,pe))

context AccèsBâtiment::ACQUITTEMENT(po :String) pre : LBL-+includes(po)

Nous avons développé d'une façon incrémentale pas-à-pas en UML-OCL l'application accès aux bâtiments en s'inspirant du processus de raffinement proposé par J.R. Abrial pour cette application [19]. Pour y parvenir, nous avons utilisé avec profit les nouvelles possibilités offertes par notre extension à OCL (EM-OCL) telles que : BinaryRelation, TotalFunction, PartialFunction et PartialInjective.

Le dernier modèle obtenu (voir figure 3.5) représente un modèle abstrait cohérent du futur système. Un tel modèle exhibe les propriétés formelles du futur système.

La classe AccèsBâtiment représentant le dernier modèle obtenu peut être raffinée davantage en prenant des décisions liées à l'identification des classes pertinentes au sens de l'approche par objets [4]. La vérification de la correction du raffinement peut être confiée à la plateforme Rodin d'Event-B moyennant des règles de transformation systématique d'UML/EM-OCL vers Event-B.

Un diagramme de classes comportant des classes d'analyse modélisant les concepts métier issus de l'application est censé traduire fidèlement des diagrammes d'objets supposés corrects. Autrement dit, nous commençons par la sélection des diagrammes d'objets représentatifs du monde réel à modéliser. Ensuite, nous vérifions si ces diagrammes respectent ou non les propriétés invariantes du diagramme de classes à valider. En cas d'échec, le coupable est le diagramme de classes. Nous préconisons l'idée d'un invariant global ( construction invariant proposée par EM-OCL ) afin de décrire les propriétés invariantes attachées à un diagrammes de classes.

- deux classes Personne et Bâtiment qui représentent l'ensemble des personnes et des bâtiments,

- deux associations autorisation et situation qui relient les classes Personne et Bâtiment. La multiplicité de l'association situation exprime le fait qu'une personne se trouve dans au plus un bâtiment. Quant à l'association autorisation, elle modélise les autorisations d'entrer dans différents bâtiments accordées à chaque personne.

Ce modèle doit être complété par les propriétés suivantes : - l'ensemble des personnes n'est pas vide,

- chaque personne est autorisée à entrer dans certains bâtiments,
- toute personne dans un bâtiment donné est autorisée à y entrer.

Description formelle en EM-OCL de l'invariant du système invariant - invariant global

persone_pas_vide : Personne::allInstances()?notEmpty() bâtiment_pas_vide : bâtiment::allInstances()?notEmpty() cardinalite : situation?size()=Personne::allInstances()?size() situation_autorisee : autorisation?includesAll(situation)

Afin d'écrire l'invariant donné ci-dessus, nous avons utilisé les conventions suivantes :

- le nom d'une association UML orientée désigne soit une relation binaire (BinaryRelation) soit une fonction (TotalFunction). Par exemple, l'association autorisation est de type BinaryRelation(Pair(Personne,Bâtiment)) et situation est de type TotalFunction(Pair(Personne,Bâtiment)). En outre, les deux multiplicités associées à l'association sont utilisées comme guides (voir TABLE 3.1) afin d'identifier avec précision la nature d'une fonction (totale, partielle, injective, surjective et bijective). Enfin, nous pouvons utiliser des contraintes associés au nom de l'association afin de préciser sa nature mathématique (voir 3^me colonne TABLE 3.1).

- la construction invariant offerte par notre extension EM-OCL comporte plusieurs prédicats étiquetés et reliés implicitement par and logique.

Par exemple, les deux diagrammes d'objets proposés par la figure 3.7 respectent l'invariant global du système.

En injectant une erreur voulue dans l'invariant (autorisation? excludesAll(situation) au lieu de (autorisation?includesAll(situation)), les deux diagrammes d'objets concernés ne respectent plus l'invariant global du système. Ainsi, le diagramme de classes proposé est incorrect.

UML

classe générique offerte par EM-OCL

UML/EM-OCL

BinaryRelation(Pair(A,B))

PartialFunction(Pair(A,B))

TotalFunction(Pair(A,B))

PartialInjective(Pair(A,B))

TotalInjectivePair(A,B))

PartialSurjective(Pair(A,B))

PartialBijective(Pair(A,B))

TotalBijective(Pair(A,B))

Le langage OCL offre des possibilités favorisant son utilisation en tant que langage de requêtes telles que : collect, select et reject. Mais les requêtes écrites en OCL doivent être liées à un contexte local c'est-à-dire à l'objet courant self. Ceci entraîne des difficultés relatives à l'écriture de telles requêtes. La figure 3.8 modélise des liens potentiels entre des entités issues d'un système bancaire simple. On se propose de formaliser en OCL et EM-OCL la requête suivante : pour chaque banque, trouver l'ensemble des ses comptes, en utilisant la construction body permettant de spécifier des requêtes utilitaires dans un contexte donné.

context Banque::comptesBancaires() :Set(TupleType(b :Banque , c :Compte)) body: Banque::allInstances()?iterate(b :Banque;

context Banque::comptesBancaires() :BinaryRelation(Pair(Banque,Compte)) body: cients?seqComposition(comptes)

La formulation en OCL utilise les constructions allInstances, TupleType et iterate. Elle a un aspect impératif : deux iterate imbriqués. Ainsi, elle est moins abstraite que celle d'EMOCL basée sur l'opération de composition séquentielle de deux relations (clients et comptes), offerte par la classe générique d'EM-OCL BinaryRelation.

EM-OCL : une extension mathématique d'OCL

Conclusion

Introduction