Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

UNIVERSITE DE MAROUA ANNEE 2018-2019 Les méthodes formelles dans le génie logic

UNIVERSITE DE MAROUA ANNEE 2018-2019 Les méthodes formelles dans le génie logiciel+ Fiche TD Chapitre : Les techniques de spécification. ............................................................................................ 6 1. Introduction .................................................................................................................................................. 6 2. Les styles de spécification .................................................................................................................... 6 3. Des techniques de spécification pour les phases d’analyse ................................................ 7 3.1. Les spécifications en langue naturelle ................................................................................... 7 3.2. Les spécifications techniques dans des langages spécialisés ou des langages informatiques de haut niveau ............................................................................................................... 7 3.3. Les diagrammes de flots de données (DFD) ...................................................................... 7 3.4. Les machines à états finis ............................................................................................................ 9 3.5. Les réseaux de Petri (RdP) ...................................................................................................... 11 3.6. Les schémas entités associations EA (ou entités relations ER)............................. 16 3.7. Les spécifications formelles ..................................................................................................... 18 4. Conclusion ................................................................................................................................................. 18 EXERCICES .................................................................................................................................................. 18 Exercice 1 Diagramme de contexte et diagramme de flots de données (DfD). ........ 18 Exercice 2 Machine à état finis. ....................................................................................................... 18 Exercice 3 Réseau de Petri. .............................................................................................................. 19 Exercice 4 Diagrammes entités associations. .......................................................................... 19 Exercice 5 Modélisation de la dynamique (automate et réseau de Petri). ................... 19 Exercice 7 : Location de cassettes (DfD) .................................................................................... 20 Exercice 8 Modélisations diverses par Réseaux de Petri ................................................... 20 Exercice 9 Appels d'offres (modèle EA, DfD et Réseau de Petri)................................... 21 Exercice 10 Automate à états finis ................................................................................................. 22 Exercice 11 Diagramme de flots de données ........................................................................... 22 Chapitre : La spécification formelle en Z .............................................................................................. 23 1. Introduction ............................................................................................................................................... 23 2. Les ensembles ........................................................................................................................................ 23 3. Les fonctions ............................................................................................................................................ 26 EXERCICES .................................................................................................................................................. 28 Exercice 3.1 : ensembles .................................................................................................................... 28 Exercice 3.2 : ensembles .................................................................................................................... 28 Exercice 3.3 : fonctions ........................................................................................................................ 29 Exercice 3.4 : fonctions ........................................................................................................................ 29 Chapitre Les bases du langage de la méthode B ............................................................................ 31 2.1 Les expressions ................................................................................................. 31 2.1.1 Expressions de base ................................................................................... 31 2.1.2 Combiner deux expressions ........................................................................ 31 2.1.3 Les ensembles ............................................................................................ 32 2.1.4 Autres constructions .................................................................................... 32 2.2 Les formules ...................................................................................................... 32 2.2.1 Formules de base ........................................................................................ 32 2.2.2 Formules ensemblistes ................................................................................ 33 2.2.3 Formules composées .................................................................................. 33 2.2.4 Les formules bien typées ............................................................................. 34 2.3 Substitution élémentaire .................................................................................... 35 2.3.1 Variables liées et substitution ...................................................................... 35 2.3.2 Substitutions multiples ................................................................................. 36 2.3.3 Substitutions généralisées .......................................................................... 36 2.4 Les relations et fonctions ................................................................................... 36 2.4.1 Relations ..................................................................................................... 36 2.4.2 Fonctions ..................................................................................................... 37 2.4.3 Séquences................................................................................................... 37 2.4.4 Exemple ...................................................................................................... 38 2.5 Méthodes de preuve .......................................................................................... 39 2.5.1 Raisonner sur les objets .............................................................................. 39 2.5.2 Raisonner sur les programmes.................................................................... 39 2.5.3 Logique de Hoare ........................................................................................ 40 Exercices ................................................................................................................... 41 Chapitre Machines abstraites ..................................................................................... 42 3.1 Introduction ........................................................................................................ 42 3.2 Les substitutions ................................................................................................ 42 3.2.1 Substitutions de base .................................................................................. 42 3.2.2 Q|S versus Q==> S ..................................................................................... 43 3.2.3 Construction de programmes ...................................................................... 43 3.2.4 Opérations ................................................................................................... 45 3.3 Structure d'une machine abstraite ...................................................................... 46 3.3.1 Machine de base ......................................................................................... 46 3.3.2 Ensembles et constantes ............................................................................ 48 3.3.3 Machine paramétrée ................................................................................... 51 3.3.4 Autres champs............................................................................................. 52 3.4 Combiner des machines abstraites .................................................................... 52 3.4.1 Substitution multiple généralisée ................................................................ 52 3.4.2 INCLUDES .................................................................................................. 52 3.4.3 USES ........................................................................................................... 55 3.4.4 SEES ........................................................................................................... 57 Exercices ................................................................................................................... 57 Exercice 1 : Modélisation de carnet d’anniversaire ................................................ 57 Chapitre : Raffinement ................................................................................................. 57 4.1 Introduction ........................................................................................................ 57 4.2 Substitution et programme ................................................................................. 58 4.2.1 Terminaison ................................................................................................. 58 4.2.2 Substitutions comme des relations .............................................................. 58 4.3 Raffiner une substitution .................................................................................... 59 4.3.1 Définition du raffinement .............................................................................. 59 4.3.2 Propriétés du raffinement ........................................................................... 59 4.4 Raffiner une machine abstraite .......................................................................... 60 4.4.1 Exemple ...................................................................................................... 60 4.4.2 Cas général ................................................................................................ 62 Exercices ................................................................................................................... 63 Exercice 1 : Modélisation et raffinage de carnet d’anniversaire .............................. 63 Chapitre : Implantation................................................................................................. 65 5.1 Principes ............................................................................................................ 65 5.2 Restrictions ........................................................................................................ 66 5.2.1 Substitutions autorisées .............................................................................. 66 5.2.2 Expressions autorisées ............................................................................... 66 5.3 La clause IMPORTS .......................................................................................... 67 5.4 La clause VALUES ............................................................................................. 67 5.4.1 Valuation d'un ensemble abstrait ................................................................. 67 5.4.2 Valuation d'une constante scalaire .............................................................. 68 5.4.3 Valuation d'une constante de tableau .......................................................... 68 5.5 Substitution WHILE .......................................................................................................................... 68 5.6 Exemple ................................................................................................................................................. 69 Exercices ......................................................................................................................................................... 72 Exercice 1 : Modélisation et raffinage de carnet d’anniversaire ....................................... 72 6 Conclusion ................................................................................................................................................ 75 Annexe : Eléments du langage de la méthode B ............................................................................. 76 Atelier B ................................................................................................................................................................ 82 Chapitre : Les techniques de spécification. 1. Introduction Tout produit complexe à construire doit d’abord êtr e spécifié ; par exemple un pont de 30 mètres de long, supportant au moins 1000 tonnes, construit en béton, etc. Ces spécifications peuvent être considérées comme un contrat entre un client (la collectivité qui veut réaliser le pont) et un producteur (l’entreprise de génie civil). En informatique, le client et le producteur peuvent être différents selon les phases du cycle de vie.  La spécification des besoins ou spécification des exigences (‘requirements’) est un contrat entre les futurs utilisateurs et les concepteurs. Elle concerne les caractéristiques attendues (exigences fonctionnelles et non fonctionnelles : efficacité, taille, sûreté, sécurité, portabilité, etc.). Elle intervient pendant la phase d’Analyse des besoins et se rédige en langue naturelle.   La spécification d’un système est un contrat entre les futurs utilisateurs et les concepteurs. Elle concerne la nature des fonctions offertes, les comportements souhaités, les données nécessaires, etc. Elle intervient pendant la phase d’Analyse du système.   La spécification d’une architecture de système est un contrat entre les concepteurs et les réalisateurs. Elle intervient pendant la phase de Conception générale. Elle définit l’architecture en modules de l’application à réaliser.   La spécification technique d’un module, d’un programme, d’une structure de données ou d’un type de données est un contrat entre le programmeur qui l’implante et les programmeurs qui l’utilisent. Elle intervient pendant la phase de Conception détaillée.  De manière générale une spécification décrit les caractéristiques attendues (le quoi) d’une implantation (le comment).  Dans cette partie nous traitons essentiellement de la spécification d’un système en termes de fonctions, de données, de comportement.  Il est souhaitable qu’une spécification soit claire, non ambiguë et compréhensible. Les descriptions en langue naturelle manquent souvent de précision.  Les spécifications doivent aussi être cohérentes (pas de contradictions) et complètes. La complétude peut prendre deux formes :   ‘interne’, c’est à dire que tous les concepts utilisés sont clairement spécifiés,   et ‘externe’, par rapport à la réalité décrite. Cette seconde forme est quelque peu illusoire dans la pratique. On ne peut pas en général spécifier tous les détails ou tout le ‘monde’ qui entoure un système. 2. Les styles de spécification Il y a deux critères de classification orthogonaux :  la formalité : on distingue des spécifications informelles (en langue naturelle), semi formelles (souvent graphiques, dont la sémantique est plus ou moins précise), formelles (quand la syntaxe et la sémantiques sont définies formellement par des outils mathématiques).  le caractères opérationnel ou déclaratif :les spécifications opérationnelles décrivent le comportement désirépar un modèle qui permet d’une certaine manière de le simuler; par opposition, les spécifications déclaratives décrivent seulement les propriétés désirées. 3. Des techniques de spécification pour les phases d’analyse 3.1. Les spécifications en langue naturelle Elles sont très souples, conviennent pour tous les aspects, sont très facilement communicables à des non spécialistes. Mais elles manquent de structuration, de précision et sont difficiles à analyser. Des efforts peuvent être faits pour les structurer (spécifications standardisées) : chapitres, sections, items, justifications (‘rationale’), etc. 3.2. Les spécifications techniques dans des langages spécialisés ou des langages informatiques de haut niveau Des langages semi formels spécialisés pour spécifier des systèmes ont été proposés. Ils comportent des sections et champs prédéfinis, ce qui force à une certaine structuration. Certains utilisent aussi des langages de haut niveau comme des ‘pseudo codes’ pour décrire les fonctionnalités attendues. 3.3. Les diagrammes de flots de données (DFD) Il s’agit d’une technique semi-formelle et opérationnelle. Les DFD décrivent des collections de données manipulées par des fonctions. Les données peuvent être persistantes (dans des stockages) ou circulantes (flots de données). La représentation graphique classique distingue :   les fonctions par des cercles   les stockages par des boîtes ouvertes   les flots par des flèches   les entités externes par des rectangles Au niveau le plus abstrait, on peut se contenter des entités à l’interface (‘acteurs’) et des flots qu’ils s’échangent, sans décomposition en fonctions. On parle alors de ‘diagramme de contexte’. En faisant apparaître les fonctions et en lesraffinant de plus en plus, on obtient des DFD à différents niveaux d’abstraction. La figure 1 donne un exemple de DFD, concernant la sélection des réponses à un appel d'offre. Il s'agit du diagramme de contexte. Le diagramme suivant (Fig. 2) est un premier raffinement du diagramme de contexte. Les DFD sont une notation semi formelle, car la sémantique des fonctions n’est pas spécifiée précisément (que signifie exactement ‘Evaluation’ ?), ni les aspects liés au contrôle (ou séquencement des opérations). Exemple : plusieurs interprétations sont possibles pour le DFD élémentaire suivant A produit une donnée et attend que B la traite pour en produire une autre, ou A et B sont des processus autonomes avec un tampon entre eux. Les DFD peuvent être analysés à le recherche de for mes ‘pathologiques’, comme le ‘trou noir’, le ‘générateur uploads/s3/ supportcoursgl-1.pdf