UNIVERSITEDEMONTR EAL VERIFICATION ALAVOL EE DE . - Polymtl.ca
UNIVERSITÉ DE MONTRÉALVÉRIFICATION À LA VOLÉE DE CONTRAINTES OCL ÉTENDUES SURDES MODÈLES UMLRAVECA-MARIA OARGADÉPARTEMENT DE GÉNIE INFORMATIQUEÉCOLE POLYTECHNIQUE DE MONTRÉALMÉMOIRE PRÉSENTÉ EN VUE DE L’OBTENTIONDU DIPLÔME DE MAÎTRISE ÈS SCIENCES APPLIQUÉES(GÉNIE INFORMATIQUE)DÉCEMBRE 2005c Raveca-Maria Oarga, 2005.!
UNIVERSITÉ DE MONTRÉALÉCOLE POLYTECHNIQUE DE MONTRÉALCe mémoire intitulé:VÉRIFICATION À LA VOLÉE DE CONTRAINTES OCL ÉTENDUES SURDES MODÈLES UMLprésenté par: OARGA Raveca-Mariaen vue de l’obtention du diplôme de: Maı̂trise ès sciences appliquéesa été dûment accepté par le jury d’examen constitué de:Mme. BOUCHENEB Hanifa, Ph.D., présidentM. MULLINS John, Ph.D., membre et directeur de rechercheM. AMYOT Daniel, Ph.D., membre
ivà Hamadou
vREMERCIEMENTSTout d’abord je voudrais remercier mon directeur de recherche, le professeur JohnMullins qui m’a encouragé à démarrer cette maı̂trise, m’a insufflé le goût de larecherche et m’a supervisé tout au long de ces deux dernieres années.J’aimerais citer et remercier mes professeurs de l’École Polytechnique: H. Boucheneb, N. Ignat, J. Pesant, et S. Wolf, qui par leurs cours et leurs travaux pratiquesont contribué à combler plusieurs lacunes de ma formation. Merci aussi à monsieurDaniel Amyot et à madame Hanifa Boucheneb pour leur participation au jury dece mémoire.En ce qui concerne le projet Socle qui a encadré ma recherche de maı̂trise, jevoudrais remercier tout spécialement mon collègue M. Bergeron, premier auteur dela première version de Socle, qui m’a beaucoup aidé à m’intégrer au projet et àdémarrer mon travail.Je ne saurais oublier la belle collaboration avec RDDC Valcartier (Recherche etDéveloppement pour la Défense du Canada) et surtout avec M. Robert Charpentier,qui a su nous encourager et conseiller à plusieurs reprises notamment pour fairela présentation du projet chez le IBM et pour la participation au concours desOCTAS (OCTets AS, concours organisé par la FIQ - Réseau de technologies del’information et des communications de Québec), d’où nous sommes sortis lauréats2005 dans la catégorie Relève Universitaire.Finalement, je tiens à remercier tous mes collègues du CRAC de cette époque André- Aiseinstadt: D. Azambre, P. Bachand, A. Fellah, S. Lafrance et H. Sardaounapour leur soutien et le fructueux travail d’équipe, mais aussi pour leurs franche etprécieuse camaraderie.
viRÉSUMÉL’outil Socle, conçu au laboratoire CRAC, permet de valider des logiciels orientésobjet, dès la phase de conception, par model-checking de contraintes OCL étenduessur des modèles UML. Ces contraintes disposent des opérateurs de points fixes capables de prendre en compte l’aspect temporel. La première version de l’outilSocle exige la construction explicite de l’espace d’états du système à analyser, cequi limite la taille du graphe à explorer. De plus la création dynamique d’objetsUML peut engendrer des espaces d’états infinis qui ne sont pas supportés par lemodel-checking.L’objectif de ce mémoire consiste à améliorer l’outil Socle en intégrant un algorithme de vérification à la volée. Cette approche, doublée d’une gestion judicieusede l’espace mémoire, offre l’avantage d’avoir à chaque instant seulement une partie du graphe en mémoire. Cette partie du graphe est construite et guidée enfonction des besoins de vérifications. Elle offre ainsi l’avantage, dans plusieurscirconstances, de contourner le problème d’explosion combinatoire, un handicapmajeur du model-checking. En effet elle permet d’arrêter la vérification dès qu’uneerreur a été détectée.L’application d’une telle technique requiert la définition d’un modèle formel dusystème à vérifier et d’une logique temporelle pour exprimer les propriétés requises.Le modèle formel que nous définissons dans ce travail est une structure de Kripkeétendue, capable d’exprimer les notions orientées-objet d’UML. La logique adoptéeest une extension d’OCL qui permet d’exprimer d’une part les notions orientéesobjet qui le lie à UML, et d’autre part, les propriétés sur les chemins d’exécutions.Finalement, nous avons validé cette technique par une importante étude de cas proposée par notre collaborateur du RDDC Valcatier. Cette étude de cas modélise etvérifie un système constitué de documents hautement sécurisés. Des tests de comparaisons ont étés effectués sur plusieurs exemples et ont démontré une réduction
viidu temps de calcul de l’ordre de 30% comparé à la version précédente.
viiiABSTRACTThe Socle tool, conceived at CRAC laboratory, allows the validation of objectoriented software, by model-checking the extended OCL constraints on UML models,during the phase of design. Those constraints have fixed points operators that adda temporal consideration.The early version of the tool’s verification requires the construction of the explicitspace states of the analyzed system which limits the size of the graph to explore.Moreover the dynamic creation of UML objects may generate infinite state spacesthat are not supported by model-checking.The objective of this thesis is to improve the Socle tool by integrating an on-the-flyverification algorithm. This approach, doubled by a judicious management of thememory space, offers the advantage of having, at every instant, only one part of themodel in memory. This part of the graph is built and conducted on the verificationneeds. Thus, in many circumstances, it offers the advantage of overcoming theproblem of combinatorial explosion, a major problem in model-checking. Indeed,it stops the verification once an error is detected.The application of such a technique requires the definition of a formal model ofthe system to verify and the definition of a temporal logic to express its properties.The formal model we defined is an extended Kripke structure able to specify theobject-oriented notions of UML. Our logic is an extension of OCL that allows to stateon one hand, the object oriented notions that bind it with UML, and on the otherhand, the properties of the execution path.Finally, we validate this technique by an important case study proposed by RDDCValcartier collaborators. This case study models and verifies a highly secureddocuments system named Caveats.Comparison tests that have been done on many examples showed a reduction ofabout 30% in the computation time compared to the previous version.
ixTABLE DES MATIÈRESDÉDICACE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .ivREMERCIEMENTS . . . . . . . . . . . . . . . . . . . . . . . . . . . . .vRÉSUMÉ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .viABSTRACT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . viiiTABLE DES MATIÈRES . . . . . . . . . . . . . . . . . . . . . . . . . . .ixLISTE DES FIGURES . . . . . . . . . . . . . . . . . . . . . . . . . . . . xivLISTE DES ABRÉVIATIONS . . . . . . . . . . . . . . . . . . . . . . . . xviiINDEX DES NOTATIONS . . . . . . . . . . . . . . . . . . . . . . . . . . xviiiLISTE DES TABLEAUX . . . . . . . . . . . . . . . . . . . . . . . . . . . xixLISTE DES ANNEXES . . . . . . . . . . . . . . . . . . . . . . . . . . . . xxiCHAPITRE 1INTRODUCTION . . . . . . . . . . . . . . . . . . . . .11.1Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . .11.2À propos de Socle . . . . . . . . . . . . . . . . . . . . . . . . .31.2.1Concepts employés par Socle . . . . . . . . . . . . . . . .31.2.2Vue d’ensemble de l’outil SOCLe . . . . . . . . . . . . . .91.3Objectifs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .131.4Méthodologie . . . . . . . . . . . . . . . . . . . . . . . . . . . .131.5Structure du mémoire . . . . . . . . . . . . . . . . . . . . . . . .15CHAPITRE 22.1ÉTAT DE L’ART . . . . . . . . . . . . . . . . . . . . .Outils - À la volée. . . . . . . . . . . . . . . . . . . . . . . . .1717
x2.22.32.42.52.1.1RuleBase2.1.2SPIN2.1.3. . . . . . . . . . . . . . . . . . . . . . . . . . . .18CADP . . . . . . . . . . . . . . . . . . . . . . . . . . . .19. . . . . . . . . . . . . . . . . . . . . .212.2.1IF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .212.2.2vUML . . . . . . . . . . . . . . . . . . . . . . . . . . . .232.2.3HUGO . . . . . . . . . . . . . . . . . . . . . . . . . . . .242.2.4JACK . . . . . . . . . . . . . . . . . . . . . . . . . . . .24Outils - UML avec OCL. . . . . . . . . . . . . . . . . . . . . .272.3.1USE . . . . . . . . . . . . . . . . . . . . . . . . . . . . .272.3.2OCLE . . . . . . . . . . . . . . . . . . . . . . . . . . . .28Logiques. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .282.4.1Regular alternation-free µ-calculus (RAFµ ) . . . . . . . . .292.4.2Observation µ-calcul d’OCL - Oµ (OCL). . . . . . . . . .312.4.3BOTL . . . . . . . . . . . . . . . . . . . . . . . . . . . .33Synthèse comparatrice des approches . . . . . . . . . . . . . . . .36STRUCTURE À BASE D’OBJETS ORIENTÉE UML . .38Fragment UML de Socle . . . . . . . . . . . . . . . . . . . . . .383.1.1Diagramme de classes . . . . . . . . . . . . . . . . . . . .393.1.2Diagramme d’objets . . . . . . . . . . . . . . . . . . . . .423.1.3Diagramme d’états-transitions . . . . . . . . . . . . . . . .433.1.3.1État . . . . . . . . . . . . . . . . . . . . . . . .433.1.3.2Transition . . . . . . . . . . . . . . . . . . . . .44Conclusion sur la modélisation . . . . . . . . . . . . . . .47Modèle formel proposé . . . . . . . . . . . . . . . . . . . . . . .483.2.1Types et valeurs . . . . . . . . . . . . . . . . . . . . . . .483.2.2Composantes du modèle . . . . . . . . . . . . . . . . . . .513.2.3Structure à base d’objets orientée UML . . . . . . . . . . .543.1.43.217Outils - UML sans OCLCHAPITRE 33.1. . . . . . . . . . . . . . . . . . . . . . . . . .
xiCHAPITRE 44.14.24.34.44.54.63.2.3.1État . . . . . . . . . . . . . . . . . . . . . . . .553.2.3.2Relation de transitions . . . . . . . . . . . . . . .593.2.3.3Fonction historique59. . . . . . . . . . . . . . . .EXTENSION OCL . . . . . . . . . . . . . . . . . . . . . 62Vue d’ensemble sur OCL . . . . . . . . . . . . . . . . . . . . . .624.1.1Motivation de la formalisation d’OCL . . . . . . . . . . . .624.1.2OCL en exemples . . . . . . . . . . . . . . . . . . . . . .63Types en OCL. . . . . . . . . . . . . . . . . . . . . . . . . . .694.2.1Types OCL standard . . . . . . . . . . . . . . . . . . . .694.2.2Types OCL dans Socle . . . . . . . . . . . . . . . . . . .70Expressions OCL . . . . . . . . . . . . . . . . . . . . . . . . . .734.3.1Syntaxe des expressions OCL . . . . . . . . . . . . . . . .734.3.2Sémantique des expressions OCL . . . . . . . . . . . . . .74Extension temporelle d’OCL - OCLEXT . . . . . . . . . . . . . . .784.4.1Syntaxe d’OCLEXT . . . . . . . . . . . . . . . . . . . . . .794.4.2Sémantique d’OCLEXT . . . . . . . . . . . . . . . . . . . .814.4.2.1Chemin. . . . . . . . . . . . . . . . . . . . . .814.4.2.2Sémantique de Pexp . . . . . . . . . . . . . . . .824.4.2.3Sémantique de Fexp . . . . . . . . . . . . . . . .834.4.2.4Abréviations et équivalences . . . . . . . . . . . .84Contraintes . . . . . . . . . . . . . . . . . . . . . . . . . . . . .864.5.1Invariant . . . . . . . . . . . . . . . . . . . . . . . . . . .864.5.2Pré/post-condition. . . . . . . . . . . . . . . . . . . . .874.5.3Autres contraintes . . . . . . . . . . . . . . . . . . . . . .88Vérification à la volée . . . . . . . . . . . . . . . . . . . . . . . .884.6.1Algorithme LMCO. . . . . . . . . . . . . . . . . . . . .884.6.2Procédure CheckEU naive . . . . . . . . . . . . . . . . . .914.6.3Procédure CheckAU . . . . . . . . . . . . . . . . . . . . .94
xii4.6.4Linéarisation de l’algorithme naı̈f . . . . . . . . . . . . . .95ÉTUDE DE CAS . . . . . . . . . . . . . . . . . . . . .975.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . .975.2Survol sur la modélisation. . . . . . . . . . . . . . . . . . . . .985.3Modélisation des tables . . . . . . . . . . . . . . . . . . . . . . .99CHAPITRE 55.45.55.3.1Étape 1 - Tableau Classification . . . . . . . . . . . . . . . 1005.3.2Étape 2 - Tableau Cavéats5.3.3Étape 3 - Tableau Projet . . . . . . . . . . . . . . . . . . 1075.3.4Étape 4 - Héritage . . . . . . . . . . . . . . . . . . . . . . 1105.3.5Simulation des objets dynamiques . . . . . . . . . . . . . . 1115.3.6Résultats de vérification . . . . . . . . . . . . . . . . . . . 111. . . . . . . . . . . . . . . . . 105Modélisation du comportement . . . . . . . . . . . . . . . . . . . 1135.4.1Diagramme de classes, diagramme d’objets . . . . . . . . . 1135.4.2Diagrammes d’états-transitions . . . . . . . . . . . . . . . 1185.4.2.1Diagramme d’états-transitions Sender . . . . . . . 1185.4.2.2Diagramme états-transitions Controller . . . . . 1215.4.2.3Diagramme d’états-transitions Table . . . . . . . 1235.4.2.4Diagramme d’états-transitions TableSecret. . . 1245.4.2.5Diagramme d’états-transitions TableCaveat. . . 1255.4.2.6Diagramme d’états-transitions TableProject . . . 1265.4.2.7Diagramme d’états-transitions Cell . . . . . . . . 1285.4.2.8Diagramme d’états-transitions Receiver . . . . . 128Vérification des contraintes . . . . . . . . . . . . . . . . . . . . . 1305.5.1Vérification des droits d’accès . . . . . . . . . . . . . . . . 1305.5.2Analyse d’erreur . . . . . . . . . . . . . . . . . . . . . . . 1335.5.3Un objet de plus . . . . . . . . . . . . . . . . . . . . . . . 135
xiiiCHAPITRE 6CONCLUSION . . . . . . . . . . . . . . . . . . . . . . . 1376.1Réalisations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1386.2Travaux futurs . . . . . . . . . . . . . . . . . . . . . . . . . . . 140RÉFÉRENCES . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142ANNEXES . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 148
xivLISTE DES FIGURESFigure 1.1Syntaxe concrète d’un diagramme d’états-transitions . . . .4Figure 1.2Syntaxe abstraite d’un diagramme d’états-transitions . . . .5Figure 1.3Model-checker . . . . . . . . . . . . . . . . . . . . . . . .8Figure 1.4Architecture de Socle . . . . . . . . . . . . . . . . . . . .9Figure 1.5Diagramme de classes . . . . . . . . . . . . . . . . . . . .11Figure 2.1Environnement CADP . . . . . . . . . . . . . . . . . . . .20Figure 2.2Outil IFx . . . . . . . . . . . . . . . . . . . . . . . . . .22Figure 2.3Outil vUML . . . . . . . . . . . . . . . . . . . . . . . . .23Figure 2.4Projet JACK . . . . . . . . . . . . . . . . . . . . . . . .26Figure 2.5Outil USE . . . . . . . . . . . . . . . . . . . . . . . . . .27Figure 2.6Logique BOTL. . . . . . . . . . . . . . . . . . . . . . .35Figure 3.1Diagramme de classes - ATM . . . . . . . . . . . . . . . .40Figure 3.2Diagramme de classes - Héritage . . . . . . . . . . . . . .41Figure 3.3Diagramme d’objets . . . . . . . . . . . . . . . . . . . . .43Figure 3.4Diagramme d’états-transitions (OR). . . . . . . . . . . .44Figure 3.5Diagramme d’états-transitions (AND) . . . . . . . . . . . .45Figure 3.6Diagramme d’états-transitions - BLC . . . . . . . . . . . .46Figure 3.7Évolution du système . . . . . . . . . . . . . . . . . . . .57Figure 3.8Exemple: Fonction historique . . . . . . . . . . . . . . . .61Figure 4.1Diagramme de classes - Archives . . . . . . . . . . . . . .64Figure 4.2Diagramme d’objets - Archives . . . . . . . . . . . . . . .65Figure 4.3Diagramme d’états-transitions - Archives . . . . . . . . . .68Figure 4.4Hiérarchie de types en OCL . . . . . . . . . . . . . . . . .70Figure 4.5Opérateurs ω . . . . . . . . . . . . . . . . . . . . . . . .72Figure 4.6Opérateurs de collections . . . . . . . . . . . . . . . . . .74Figure 4.7Règles de typage d’OCL . . . . . . . . . . . . . . . . . . .76
xvFigure 4.8Exemple: graphe et dépliage. . . . . . . . . . . . . . . .82Figure 4.9Sémantique des opérateurs: AG, AF, EF, AX et EG . . . .85Figure 4.10Algorithme à la volée . . . . . . . . . . . . . . . . . . . .90Figure 4.11Procédure CheckEU naı̈ve . . . . . . . . . . . . . . . . . .91Figure 4.12Vérification de E[ϕ1 Uϕ2 ] . . . . . . . . . . . . . . . . . .92Figure 4.13Procédure CheckAU . . . . . . . . . . . . . . . . . . . . .94Figure 4.14Procédure CheckEU linéaire . . . . . . . . . . . . . . . . .96Figure 5.1Modélisation des tables . . . . . . . . . . . . . . . . . . .98Figure 5.2Modélisation du comportement . . . . . . . . . . . . . . .99Figure 5.3Diagramme de classes - Étape 1 . . . . . . . . . . . . . . . 101Figure 5.4Diagramme d’objets - Étape 1 . . . . . . . . . . . . . . . . 102Figure 5.5Diagramme d’objets réduit - Étape 1 . . . . . . . . . . . . 105Figure 5.6Diagramme de classes - Étape 2 . . . . . . . . . . . . . . . 106Figure 5.7Diagramme d’objets - Étape 2 . . . . . . . . . . . . . . . . 107Figure 5.8Diagramme d’objets - Étapes 3 et 4 . . . . . . . . . . . . . 109Figure 5.9Diagramme de classes - Étape 3 et 4 . . . . . . . . . . . . 110Figure 5.10Diagramme d’états-transitions User - Étape 4 . . . . . . . . 112Figure 5.11Diagramme des classesFigure 5.12Diagramme d’objets . . . . . . . . . . . . . . . . . . . . . 117Figure 5.13Diagramme d’états-transitions - Sender . . . . . . . . . . . 118Figure 5.14Diagramme d’états-transitions - Controller . . . . . . . . 121Figure 5.15Diagramme états-transitions - Table . . . . . . . . . . . . 124Figure 5.16Diagramme états-transitions - TableSecret. . . . . . . . 124Figure 5.17Diagramme états-transitions - TableCaveat. . . . . . . . 125Figure 5.18Diagramme états-transitions - TableProject . . . . . . . . 127Figure 5.19Diagramme états-transitions - Cell . . . . . . . . . . . . . 129Figure 5.20Diagramme états-transitions - Receiver . . . . . . . . . . 129Figure 5.21Diagramme de séquences - Erreur . . . . . . . . . . . . . . 134. . . . . . . . . . . . . . . . . . . 114
xviFigure 5.22Diagramme d’objets - Deux Senders . . . . . . . . . . . . . 136Figure I.1GrapheFigure I.2Linéarisation - Étape 1 . . . . . . . . . . . . . . . . . . . 152. . . . . . . . . . . . . . . . . . . . . . . . . . . 150
xviiLISTE DES ABRÉVIATIONSASMAbstract State MachineCRACConception et Réalisation des Applications ComplexesCTLComputation Tree LogicLMCOLocal Model Checking for OCLEXTLTLLinear Temporal LogicOCLObject Constrant LanguageOCLEXTExtension temporelle d’OCLOMGObjects Management GroupRDDCRecherche et Développement pour la Défense du CanadaSocleSecur OCL environnementUMLUnified Modeling Languageµ-calculLogique temporelle de points fixes
xviiiINDEX DES NOTATIONS%Msigretour méthode . . . . . . . . . . . . . . . . . . . . . .45τtype UML, OCL . . . . . . . . . . . . . . . . . . . . . . .49OIdCensemble des instances de la classe C . . . . . . . . . . .50MIdC,Mensemble des instances de la méthode M de la classe C . .50 valeur non définie . . . . . . . . . . . . . . . . . . . . .50#hrelation d’héritage . . . . . . . . . . . . . . . . . . . . .52#orelation de redéfinition de méthode . . . . . . . . . . . .52(C, i)instance i de la classe C . . . . . . . . . . . . . . . . . .53(o, M, i)instance i de la méthode M exécutée par l’objet o. . . .53Sensemble des états du système. . . . . . . . . . . . . .54(σ, γ)un état dans le graphe d’exécution . . . . . . . . . . . .55σfonction qui décrit les objets actifs . . . . . . . . . . . .55γfonction qui décrit les méthodes actives . . . . . . . . . .55εfonction historique . . . . . . . . . . . . . . . . . . . . .60KΥstructure de Kripke orientée-objet . . . . . . . . . . . . .60RΥrelation de transitions du système . . . . . . . . . . . . .60Eexpensemble des expressions OCL . . . . . . . . . . . . . . .73 opérateur de typage pour les expression OCL. . . . . . .74[[ ]]fonction d’évaluation des expressions OCL . . . . . . . . .76Pexpensemble des propriétés d’état de la logique OCLEXT . . .79Fexpensemble des formules temporelles de la logique OCLEXT .79!relation de satisfaction pour la sémantique de Fexp . . . .83Cexpensemble des contraintes OCL . . . . . . . . . . . . . . .86φformule OCLEXT . . . . . . . . . . . . . . . . . . . . . .89
xixLISTE DES TABLEAUXTableau 2.1Exemples de propriétés . . . . . . . . . . . . . . . . . . .30Tableau 3.1Syntaxe des déclencheurs . . . . . . . . . . . . . . . . . .45Tableau 3.2Syntaxe des actions . . . . . . . . . . . . . . . . . . . . .47Tableau 3.3Éléments de la classe Bank52Tableau 5.1Tableau Classification . . . . . . . . . . . . . . . . . . . . 100Tableau 5.2Visibilité, Pays, Rang . . . . . . . . . . . . . . . . . . . . 103Tableau 5.3Niveau, Cavéat, Projet . . . . . . . . . . . . . . . . . . . 103Tableau 5.4Expressions OCL de navigation . . . . . . . . . . . . . . . 104Tableau 5.5Tableau Caveats . . . . . . . . . . . . . . . . . . . . . . . 106Tableau 5.6Tableau ProjetTableau 5.7Résultants pour les étapes 1, 2, 3 et 4 . . . . . . . . . . . . 112Tableau 5.8Transitions Sender - AccessRead . . . . . . . . . . . . . . 120Tableau 5.9Garde d’accès Table Caveats . . . . . . . . . . . . . . . . 125Tableau 5.10Objets: uS et d . . . . . . . . . . . . . . . . . . . . . . . 126Tableau 5.11Garde d’accès Table Caveats - Exemple . . . . . . . . . . . 126Tableau 5.12Garde d’accès Table Projet - ExempleTableau 5.13Transitions Cell . . . . . . . . . . . . . . . . . . . . . . . 129Tableau 5.14Transitions Receiver . . . . . . . . . . . . . . . . . . . . 130Tableau 5.15Invariants - Conditions d’accès . . . . . . . . . . . . . . . 132Tableau 5.16Invariant falsifié . . . . . . . . . . . . . . . . . . . . . . . 134Tableau 5.17Résultants d’invariant - trois usagers . . . . . . . . . . . . 136Tableau II.1Symboles formels sur une transition . . . . . . . . . . . . . 158Tableau II.2Transitions Sender - AskSend . . . . . . . . . . . . . . . . 158Tableau II.3Transitions Controller - AskAccessTableau II.4Transitions Controller - AskSend et ChangeTable . . . . . 160Tableau II.5Transitions TableSecret - TabSecretStatechart. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108. . . . . . . . . . . 128. . . . . . . . . . . . 159. . . . . . 161
xxTableau II.6Transitions TableCaveat - TableCaveatStatechart . . . . . . 161Tableau II.7Transitions TableProject - TableProjectStatechart . . . . . 162Tableau II.8Résultats de vérifications . . . . . . . . . . . . . . . . . . 163
xxiLISTE DES ANNEXESANNEXE IDÉTAILS SUPPLÉMENTAIRES SUR L’ALGORITHME ÀLA VOLÉE . . . . . . . . . . . . . . . . . . . . . . . . 148I.1Linéarisation de la procédure CheckEU . . . . . . . . . . . . . . . 148ANNEXE IIDÉTAILS DE L’ÉTUDE DE CAS . . . . . . . . . . . . . 157II.1 Les transitions formelles. . . . . . . . . . . . . . . . . . . . . . 157II.2 Résultats sur l’étude de cas d’ATM . . . . . . . . . . . . . . . . . 163
1CHAPITRE 1INTRODUCTION1.1MotivationLes ordinateurs représentent une part intégrante dans notre société et dans notreéconomie, et leurs logiciels deviennent de plus en plus gros et complexes. Ledéveloppement de logiciels de qualité est une activité difficile, et passe par le renforcement des activités de conception, de validation et de test. La plupart du temps,le comportement d’un logiciel est validé après l’implantation. Cette technique estcoûteuse et parfois peu réalisable.Pour réduire la complexité du développement de logiciel, la construction du modèlelogiciel dès la phase de conception, est envisagée. Un modèle représente une simplification de la réalité qui ne retient que les éléments pertinents du problème. Lemodèle logiciel ne se soucie pas du détail, il ne représente que les besoins les plusimportants de la conception. Par analogie, on peut penser à la conception d’unplan de maison. On ne se demande pas comment les briques seront placées dansun mur, mais plutôt si les murs ne s’écrouleront pas, une fois montés.La description d’un modèle logiciel requiert l’utilisation d’un langage de modélisation. Parmi les langages de modélisation existants, le Unified Modeling Language(UML) (OMG, 2003a) est devenu un standard de facto dans l’industrie actuelle.UML est un langage graphique et les logiciels sont représentés visuellement par desdiagrammes. Le modèle sous cette forme est assez intuitif, mais il peut porterà confusion entre la phase de conception et d’implantation, car il est possibled’interpréter de plusieurs façons un même diagramme, et il y a aussi le problème de
2cohérence entre les différents diagrammes. Pour éliminer les ambiguı̈tés dans cettephase de développement, un modèle formel (mathématique) s’avère nécessaire.Un modèle formel suppose une sémantique formelle pour UML. Malheureusement,UML dans son entité présente seulement une sémantique en langue naturelle.Chaque développeur d’outil d’aide à la conception prend en compte un fragmentd’UML et en donne une sémantique formelle.Le modèle formel ajoute un autre avantage; il permet l’application de méthodesformelles de vérification qui permettent de découvrir des erreurs à ce stade dudéveloppement, et donc de réduire le coût de production. Parmi les méthodesformelles, une de plus employée à l’heure actuelle c’est le model-checking. L’idéeest d’explorer exhaustivement l’espace d’états du système et de vérifier si une propriété est vérifiée ou non. L’utilisation de cette technique d’analyse automatiquenécessite des modèles finis en entrée et son plus grand handicap est le problèmed’explosion combinatoire. On nomme explosion combinatoire le fait qu’un petitchangement du nombre de données à considérer dans un problème provoque uneexplosion du nombre d’états à considérer. Cela peut suffire à rendre sa solution trèsdifficile, voire impossible dans certains cas avec les ordinateurs actuels. Or, dansla modélisation orienté-objet (UML notamment) où les objets peuvent être créés etdétruits dynamiquement, l’explosion combinatoire peut provoquer un espace infinid’états, donc créer un réel problème pour l’application du model-checking.L’outil Socle (Secure OCL environnement) développé au laboratoire CRAC (Conception et Réalisation des Applications Complexes), permet de valider des logiciels dès la phase de conception, par le model-checking de contraintes OCL (ObjectConstraint Language)(OCL 1.1, 1997; OMG, 2002), le langage de spécification depropriétés, sur des modèles UML, le langage de spécification du système.Dans le but d’améliorer l’outil Socle, l’équipe du CRAC, explore présentement
3plusieurs méthodes d’abstraction et de réduction de modèles UML. Parmi les méthodes de réduction en vue, la plus avancée est l’analyse statique par slicing qui consiste à éliminer toute partie du calcul qui n’influence pas la vérification recherchée.Une façon de combattre le problème d’explosion combinatoire est d’appliquer unetechnique alternative, qui combine la simulation avec la vérification et qui permetd’explorer un espace d’états plus volumineux en ne gardant en mémoire qu’une partie du graphe d’exécution piloté par la propriété à vérifier. De plus, une vérifications’arrête dès que la propriété est vérifiée ou falsifiée. Si cette propriété est trouvéefause, un contre-exemple est produit pour aider le concepteur à corriger les erreurs.Elle permet également de réduire le temps de calcul dans plusieurs cas significatifs.Il s’agit de la vérification à la volée (on-the-fly), technique adoptée et analysée dansce mémoire qui vise en grande partie l’amélioration de l’outil Socle au niveau dela vérification. Une telle technique requiert un modèle formel orienté UML et unelogique temporelle qui intègre la spécification d’OCL. La validation de Socle aveccette technique est réalisée par des études de cas.1.21.2.1À propos de SocleConcepts employés par SocleLe projet Socle a développé une sémantique formelle pour un fragment significatif d’UML qui intègre les expressions OCL, la création d’objets et l’héritagecomportemental.De plus, l’approche permet la vérification des contraintesOCL, via les techniques de model-checking. Les trois paragraphes suivants donnent une synthèse succincte des trois concepts utilisés par l’outil Socle: UML, OCL etmodel-checking.
4UML Unified Modeling Language est né de la fusion de trois méthodes qui ontinfluencé la modélisation orientée-objet au milieu des années 90: OMT (Rumbaughet al., 1991), Booch (Booch, 1994) et OOSE (Jacobsen et al., 1992). En l’espacede quelques années seulement (1997), UML est devenu une norme incontournablede l’OMG (Object Management Group). Le langage UML comble une lacune importante des technologies orientées-objet. Il permet d’exprimer et d’élaborer desmodèles orientés-objet, indépendamment de tout langage de programmation. Ila été conçu pour servir de support à une analyse basée sur les concepts orientésobjet. Sa notation graphique permet d’exprimer visuellement une solution orientéeobjet, ce qui facilite la comparaison et l’évaluation de plusieurs solutions. Finalement, la véritable force d’UML est qu’il repose sur un métamodèle, ce qui permet declasser les différents concepts du langage (selon leur niveau d’abstraction ou leurdomaine d’application) et d’exposer ainsi clairement sa structure. Un métamodèledécrit d’une manière très précise tous les éléments de la modélisation (les conceptsvéhiculés et manipulés par le langage) et la syntaxe de ces éléments (leur définitionet le sens de leur utilisation). Donc, au niveau du métamodèle, UML possède unesyntaxe formelle. On peut noter que le métamodèle d’UML est lui-même décritde manière standardisée par un méta-métamodèle, à l’aide de MOF (Meta Object Facility), une norme OMG (Object Management Group) de description desmétamodèles. Par contre, une faiblesse d’UML est qu’il ne définit pas le processusd’élaboration des modèles.Figure 1.1 Syn
universitedemontr eal ecole polytechnique de montr eal ce m emoire intitul e: verification alavol ee de contraintes ocl etendues sur
Mobil DTE PM 220 Mobil EAL Arctic 15 Mobil EAL Arctic 22 Mobil EAL Arctic 32 Mobil EAL Arctic 46 Mobil EAL Arctic 68 Mobil EAL Arctic 100 . Mobil Glygoyle 11 Mobil Glygoyle 22 Mobil Glygoyle 30 Mobil Glygoyle 220 Mobil Glygoyle 320 Mobil Glygoyle 460 Mobil Glygoyle 680 Mobil Jet Oil 254 Mobil Jet Oil II Mobil Multigrade 10W-40 Mobil .
Foreword v Transliterations xi Abbreviations xii The Principles of the Naqshbandi Way 13 The conduct of the murid with his Shaykh 15 The conduct of the murid with his brothers 15 The Daily êal ¿hs: 1. êal ¿tul-Maghrib 18 2. êal ¿tul-Ish ¿' 36 3. Fajr: i. Pre-Fajr Programme 52 ii. êal ¿tun Naj ¿h (The Prayer of Salvation). 54 iii.
22491VIC Certificate III in EAL (Further Study) 22492VIC Certificate IV in EAL (Further Study) These courses hav e been accredited under Part 4.4 of the Education and Training Reform Act
HCGS EAL Comparison Matrix (115 Pages) Hope Creek Generating Station NEI 99-01 Revision 6 EAL Comparison Matrix . EAL Comparison Matrix i of i Table of Contents Section Page Introduction ----- 1 Comparison Matrix Format ----- 1 .
Use Identifying Children who are Learning English as an Additional Language(EAL) and who may also have Learning Difficulties and/or Disabilities (LDD) to plan adult support for each stage. Track children’s English language development and use to inform planning. Develop systematic monitoring and rigorous tracking of EAL children using EAL observation sheets, tracking sheets and assessment .
VCE English implementation briefings — participant workbook Unit 3 — Sample course plan In many schools it is the practice that English classes contain small numbers of EAL students. EAL students in combined English/EAL classes may require additional teaching time to work on
mobil dte pm 150 35 mobil dte pm 220 35 mobil eal arctic 22 23 mobil eal arctic 32 23 mobil eal arctic 46 23 . mobil extra hecla super cylinder oil 19 mobil glygoyle 11 21 mobil glygoyle 22 21 mobil glygoyle 30 21 mobil glygoyle 220 21 mobil glygoyle 320 21 mobil glygoyle 460 21 mobil glygoyle 680 21 mobil jet oil 254 50 mobil jet oil ii 50
Small Group Work Sessions . Part 1: Group Discussion . 30-45 Minutes . Part 2: Group Report Out . 30 Minutes . Title: PowerPoint Presentation Author: Pawling, Neil Created Date: 9/19/2014 3:56:30 PM .
