Remerciez-le!

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

Génie Logiciel Avancé|M1-STW Année Univ : 2019/2020 1 Chapitre 2 : Introduction

Génie Logiciel Avancé|M1-STW Année Univ : 2019/2020 1 Chapitre 2 : Introduction à la spécification formelle du logiciel Partie I. Introduction 1. Spécification formelle Une spécification est formelle si des méthodes formelles sont utilisées pour modéliser le comportement d’un système (le quoi ? et non pas le comment ?) et pour vérifier de façon mathématique que la conception et la mise en œuvre du système satisfont bien les fonctionnalités ainsi que diverses propriétés de sûreté. Ainsi, les mathématiques requises pour l’écriture des spécifications sont faciles. 2. Méthode formelle Les méthodes formelles sont des techniques basées sur les mathématiques pour décrire les propriétés d’un système. Elles fournissent un cadre systématique pour développer un système et, pour valider et vérifier ce dernier. Il y a deux grandes écoles de spécification formelle et de méthodes formelles : - Les données d’un système permettent de décrire les états du système - les opérations du système permettent de décrire son fonctionnement ou son comportement par des axiomes => Paradigme des données et paradigme des opérations. - Il y a un troisième paradigme qui semble être transversal. C’est le paradigme des processus (les algèbres de processus). Dans ce paradigme, les systèmes sont décrits par les équations exprimant leur comportement ou leur états. Les principales algèbres de processus sont : CSP (Hoare, 1987), CCS (Milner, 1989), ACP (Bergstra) Remarque. Il convient de distinguer entre : – les opérations exprimant le comportement d’un système. Ces dernières opèrent sur les données du système et celles ; – des opérations caractérisant les données du système qui permettent de construire et exploiter les données du système. 3. Langage formel de spécification C’est un langage qui a une syntaxe et une sémantique bien définies (c'est-à-dire pas de flou possible). Il permet une description abstraite, claire et précise du comportement attendu d’un système . Remarque : - La syntaxe décrit les mots, les phrases et les énoncés acceptables et biens formés. - La sémantique définit le sens et la signification des énoncés du langage. Génie Logiciel Avancé|M1-STW Année Univ : 2019/2020 2 4. Quelques avantages des méthodes formelles - Obtenir des spécifications claires, précises, non-ambiguës, plus explicites ; - Plus concises et compactes que la langue naturelle (mais plus difficile à comprendre) ; - Fournit une base précise pour le développement des tests et des jeux d’essais ; - Peut s’analyser automatiquement pour effectuer une vérification formelle. 5. Qui peut et à quelles étapes utiliser une méthode formelle ? 5.1. Essentiellement pour l’industrie de pointe et des applications sensibles: nucléaire, avionique, médical, finances, électronique... Quelques exemples de projets qui utilisent des méthodes formelles : - NASA: Contrôle de satellites, navettes - RATP: Contrôle du métro de Paris - SNCF: Limitations de vitesse des trains - FAA: Prévention des collisions en vol - Darlington, Ontario: Extinction de réacteurs nucléaires 5.2. À différentes étapes du cycle de vie d’un logiciel : - analyse et spécification ; - conception architecturale ; - vérification ; - implémentation: génération de code. Partie II. OCL (Object Constraint Language) : Langage de contraintes orienté-objet 1. UML et l’expression des contraintes UML permet d’exprimer certaines formes de contraintes : les contraintes structurelles (les attributs dans les classes, les différents types de relations entre classes (généralisation, association, agrégation, composition, dépendance), la cardinalité et la navigabilité des propriétés structurelles, etc. ), les contraintes de type (typage des propriétés) et les contraintes diverses (les contraintes de visibilité, les méthodes et classes abstraites (contrainte abstract)). 2. Quelques exemples : représentation des contraintes et contraintes prédéfinies en UML Exemple 1. Etant donné le diagramme de classe suivant : 1. Donner une spécification informelle à ce diagramme. 2. Peut-on exprimer, dans ce diagramme, tout ce qui est défini dans la spécification informelle ? 3. Le diagramme de classe permet-il de détailler toutes les contraintes sur les relations entre les classes ? Manque de précision à cause du manque de spécification de contraintes. Génie Logiciel Avancé|M1-STW Année Univ : 2019/2020 3 Diagramme de classe Diagramme d’objets 1 Diagramme d’objets 2 UML permet d'associer une contrainte à un, ou plusieurs, élément(s) de modèle de différentes façons: • en plaçant directement la contrainte à côté d'une propriété ou d'une opération dans un classeur ; • en ajoutant une note associée à l'élément à contraindre ; • en plaçant la contrainte à proximité de l'élément à contraindre, comme une extrémité d'association par exemple ; • en plaçant la contrainte sur une flèche en pointillés joignant les deux éléments de modèle à contraindre ensemble, la direction de la flèche constituant une information pertinente au sein de la contrainte ; • en plaçant la contrainte sur un trait en pointillés joignant les deux éléments de modèle à contraindre ensemble dans le cas où la contrainte est bijective ; • en utilisant une note reliée, par des traits en pointillés, à chacun des éléments de modèle, subissant la contrainte commune, quand cette contrainte s'applique sur plus de deux éléments de modèle. Exemple 2. Génie Logiciel Avancé|M1-STW Année Univ : 2019/2020 4 Sur les deux diagrammes du haut, la contrainte porte sur un attribut qui doit être positif. En bas : - la contrainte {frozen} précise que le nombre de roues d'un véhicule ne peut pas varier. - Au milieu, la contrainte {subset} précise que le président est également un membre du comité. - la contrainte {xor} précise que les employés de l'hôtel n'ont pas le droit de prendre une chambre dans ce même hôtel. Exemple 3. - Dans la pratique, toutes ces contraintes sont très utiles, mais se révèlent insuffisantes. Donc, les diagrammes UML seuls sont généralement insuffisants pour spécifier complètement une application => Nécessité de rajouter des contraintes. - Donc, on représente une contrainte sous la forme d'une chaîne de texte placée entre accolades ({}). La chaîne constitue le corps écrit dans un langage de contrainte qui peut être : • naturel ; • formel avec sémantique précise, comme OCL ; • ou encore directement issu d'un langage de programmation. N.B. Si une contrainte possède un nom, on présente celui-ci sous forme d'une chaîne suivie d'un double point (:), le tout précédant le texte de la contrainte. 3. OCL 3.1. définition OCL est un langage formel (mais simple à utiliser) d'expression de contraintes bien adapté aux diagrammes d'UML, et en particulier au diagramme de classes. OCL peut s'appliquer sur la plupart des diagrammes d'UML et permet de spécifier des contraintes sur l'état d'un objet ou d'un ensemble d'objets comme : • des invariants sur des classes ; • des pré-conditions et des post-conditions à l'exécution d'opérations ; • des gardes sur des transitions de diagrammes d'états-transitions ou des messages de diagrammes d'interaction ; • des ensembles d'objets destinataires pour un envoi de message ; • des attributs dérivés ; • des stéréotypes, etc. 3.2. OCL vs Langage naturel et langage de programmation Génie Logiciel Avancé|M1-STW Année Univ : 2019/2020 5 Langage naturel OCL (langage forrmel) - Accessible - Imprécis - Ambigu - Interprétable par des outils - Précis - Non ambigu Langage de programmation OCL - Niveau d’abstraction faible - Mode opérationnel (COMMENT ?) - abstrait - mode descriptif (QUOI ?) 3.3. Syntaxe d’OCL 3.3.1. Contexte Une contrainte (expression OCL) est toujours définie dans un contexte qui est un élément du modèle : classe, interface, attribut ou opération, relation Syntaxe: context<élément> Exemples de types de contexte. - Sur une classe : context Étudiant - Sur un attribut : context Étudiant::nom - Sur une opération : context Étudiant::setNom(nom: String): void 3.3.2. Invariant Un invariant exprime une contrainte sur un objet ou un groupe d'objets qui doit être respectée en permanence. Syntaxe: inv [<nom>]: <expression_logique> Exemple 1. Soit le diagramme de classe suivant : En OCL : context Étudiant inv: moyenne >= 0.0 Remarque. Pour accéder aux propriétés d’un objet désigné par le contexte, on utilise le mot clé self. Exemple 2. dans le context Étudiant, on utilise : nom self.nom Génie Logiciel Avancé|M1-STW Année Univ : 2019/2020 6 renommer(“nouveau_nom”) self.renommer(“nouveau_nom”) 3.3.3. Pré et post-conditions Pour une opération, on spécifie la contrainte à vérifier avant ou après l’opération :  Précondition : état qui doit être respecté avant l'appel de l'opération Syntaxe : pre[<nom>]: <expression_logique>  Postcondition : état qui doit être respecté après l'appel de l'opération 1. Syntaxe : post[<nom>]: <expression_logique> 2. Dans la postcondition, deux éléments particuliers sont utilisables :  Pseudo-attribut result: référence la valeur retournée par l'opération  mon_attribut@pre: référence la valeur de mon_attribut avant l'appel de l'opération Syntaxe pour préciser la signature de l'opération : context ma_classe::mon_op(liste_param) : type_retour  Body : comportement attendu de l’opération Syntaxe : body : <requête> Exemple 3. Context Compte::débiter(somme : Real) pre: somme > 0.0 post: solde = solde@pre – somme Context Compte::getSolde() : Real post: result = solde body: self.solde Context Compte::créditer(montant: Real) pre: montant > 0.0 post: solde = solde@pre+ montant Exemple 4. Context Compteur::moyenne(): Integer body: somme / valeurs Remarque. On ne décrit pas comment l'opération est réalisée mais des contraintes sur l'état avant et après son exécution. 3.3.4. Notion de conception par contrat pour opération Les pré et postconditions uploads/Voyage/ chapitre-2-gla.pdf