Remerciez-le!

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

Supportcoursgl 1 UNIVERSITE DE MAROUA ANNEE - Les méthodes formelles dans le génie logiciel Fiche TD CChapitre Les techniques de spéci ?cation Introduction Les styles de spéci ?cation Des techniques de spéci ?cation pour les phases d ? analyse Les spéci ?

UNIVERSITE DE MAROUA ANNEE - Les méthodes formelles dans le génie logiciel Fiche TD CChapitre Les techniques de spéci ?cation Introduction Les styles de spéci ?cation Des techniques de spéci ?cation pour les phases d ? analyse Les spéci ?cations en langue naturelle Les spéci ?cations techniques dans des langages spécialisés ou des langages informatiques de haut niveau Les diagrammes de ots de données DFD Les machines à états ?nis Les réseaux de Petri RdP Les schémas entités associations EA ou entités relations ER Les spéci ?cations formelles Conclusion EXERCICES Exercice Diagramme de contexte et diagramme de ots de données DfD Exercice Machine à état ?nis Exercice Réseau de Petri Exercice Diagrammes entités associations Exercice Modélisation de la dynamique automate et réseau de Petri Exercice Location de cassettes DfD Exercice Modélisations diverses par Réseaux de Petri Exercice Appels d'o ?res modèle EA DfD et Réseau de Petri Exercice Automate à états ?nis Exercice Diagramme de ots de données Chapitre La spéci ?cation formelle en Z Introduction Les ensembles Les fonctions EXERCICES Exercice ensembles Exercice ensembles Exercice fonctions Exercice fonctions CChapitre Les bases du langage de la méthode B Les expressions Expressions de base Combiner deux expressions Les ensembles Autres constructions Les formules Formules de base Formules ensemblistes Formules composées Les formules bien typées Substitution élémentaire Variables liées et substitution Substitutions multiples Substitutions généralisées Les relations et fonctions Relations Fonctions Séquences Exemple Méthodes de preuve Raisonner sur les objets Raisonner sur les programmes Logique de Hoare Exercices Chapitre Machines abstraites Introduction Les substitutions Substitutions de base Q S versus Q S Construction de programmes Opérations Structure d'une machine abstraite Machine de base Ensembles et constantes Machine paramétrée Autres champs C Combiner des machines abstraites Substitution multiple généralisée INCLUDES USES SEES Exercices Exercice Modélisation de carnet d ? anniversaire Chapitre Ra ?nement Introduction Substitution et programme Terminaison Substitutions comme des relations Ra ?ner une substitution Dé ?nition du ra ?nement Propriétés du ra ?nement Ra ?ner une machine abstraite Exemple Cas général Exercices Exercice Modélisation et ra ?nage de carnet d ? anniversaire Chapitre Implantation Principes Restrictions Substitutions autorisées Expressions autorisées La clause IMPORTS La clause VALUES Valuation d'un ensemble abstrait Valuation d'une constante scalaire Valuation d'une constante de tableau Substitution WHILE Exemple Exercices Exercice Modélisation et ra ?nage de carnet d ? anniversaire C Conclusion Annexe Eléments du langage de la méthode B Atelier B CChapitre Les techniques de spéci ?cation Introduction Tout produit complexe à construire doit d ? abord êtr e spéci ?é par exemple un pont de mètres de long supportant au moins tonnes construit en béton etc Ces spéci ?cations 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 di ?érents selon les phases du cycle de vie La spéci ?cation des besoins ou spéci ?cation des exigences ? requirements ? est un contrat entre les futurs utilisateurs et les concepteurs Elle