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 : Méthode de Spécification et développement formel de logiciel P

Génie Logiciel : Méthode de Spécification et développement formel de logiciel Prof Atsa Etoundi Roger Maître de conférences Développement de logiciels Nature des logiciels : – séquentiels, parallèles, – ﬂot de données, transactionnels, – autonomes, centralisés, – répartis, réactifs, temps-réels – embarqués, protocoles, mobiles, – etc Cycles de vie Ils ont été pendant longtemps le support méthodologique du développement du logiciel. Les plus représentatifs de ces cycles de vie : – Cycle en V, – Cycle en cascade, – Cycle de Balzer Intérêts et limites des méthodes semi- formelles – SADT (Structural Analysis and design technique), – SA-RT (Structiral Analysis and Reuse Technique), – SSADM (Structured Systems Analysis and Design Method), . . . – JSD-JSP (Jackson System Development- Jackson Structured Programming), – Merise, Axial, . . . – OOA (Objet Oriented Analysis), OMT (Object Modelling Technique), . . . – UML (Unified Modelling Language) Ces méthodes permettent de réaliser une analyse parfaite du problème. La contribution de ces méthodes est certes positive même si elle reste insuffisante. Elles permettent de dégrossir le problèmes. La sémantique des modèles conçus reste informelle et mal définie, il y a un manque de rigueur mathématique, analyse profonde du problème très difficile et couteuse. Par conséquent, il est difficile prouver certaines propriétés du système. Elles ne garantissent pas la sécurité du système. En bref, ces méthodes ont une sémantique ou de règles de validation incomplètes. Mais il est impossible de raisonner/analyser formellement sur le système en vue. Il peut ainsi y avoir des ambigüités, . . .; ceci constitue des sources de BUG dans le système. Méthode formelle Une méthode formelle utilise les mathématiques pour laisser moins de place aux intuitions et aux erreurs. Elle dispose des entités suivantes: 1. Un langage qui est un moyen pour exprimer et concevoir un système, la nature de ce langage peut être symbolique, graphique etc. 2. Une sémantique qui donne la signification des éléments du langage 3. Des règles de validation qui permettent d’exprimer les propriétés désirées du système;, et d’utiliser la sémantique du système pour validation. Les règles doivent laisser moins de place aux erreurs et à l’intuition. Spéciﬁcation formelle La spécification formelle est une expression dans un langage formel du quoi d’un système à développer. – Résultat de la phase d’analyse – Plusieurs formes possibles selon la nature du système Cette expression est faite dans un langage ou un formalisme de spéciﬁcation formelle comme la logique, les langages de spéciﬁcation algébriques, algèbres de processus, etc Démarche de spéciﬁcation Dans la mise en place d’un système, l’on peut s’interesser aux aspects données ou bien aux aspects opérations. A ce titre, deux grandes écoles de spéciﬁcation formelle et de méthodes formelles ont vu le jour. – 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 Il convient de distinguer : – les opérations exprimant le comportement d’un système – des opérations caractérisant les données du système. Les premières opèrent sur les données du système, alors que les dernières permettent de construire et exploiter les données du système. Démarche de spéciﬁcation 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 des processus les systèmes sont décrits par les équations exprimant leur comportement ou leurs états. Les principales algèbres de processus à la base des autres formalismes sont : – CSP: Communication Sequetial Processes défini par C.A.R Hoare en 1978 – CCS: Calculus of Communicating Systems defini par Milner en 1980 – ACP: Algebra of Communicating Processes defini par Jan Bergstra en 1984 Eléments de classification La principale classification des approches consiste à distinguer deux principales approches de spécifications formelles et de méthodes formelles : - l'approche opérationnelle : orientée modèle ou état - et l'approche axiomatique : orientée propriétés. D'autres classifications (de bas niveau) sont rencontrées : (a) classification basée sur les paradigmes : - données : (data-oriented) + états, + opérations, - processus : process-oriented - Hybride (b) une classification basée sur les langages : - les langages généraux : Z, spécification algébriques, HOL, PVS, etc - les langages orientés « contrôle‘ »: CCS, CSP, SIGNAL, ESTEREL, LUSTRE, etc Spéciﬁcations orientées états (model-based approach ou state-based approach) Dans cette approche, on privilégie les données du système, on s’intéresse à l’état du système. Principe Une spéciﬁcation permet de construire, à l’aide des concepts de base fournis, un modèle du système (logiciel) à développer. Ce modèle doit avoir les propriétés du système. On peut ensuite raisonner sur le fonctionnement du système en utilisant le modèle. Concepts de base On utilise essentiellement les mathématiques discrètes (Théorie des ensembles), et la Logique. Quelques exemples de formalismes • Z, VDM, B etc pour les systèmes séquentiels, • Réseaux de Pétri, CCS, CSP, Unity, etc pour les systèmes concurrents et distribués, avec CCS et CSP relèvant du paradigme des processus. Spéciﬁcations orientées propriétés ou axiomatiques (axiomatic approach, algebraic approach, operation oriented) Principe La spéciﬁcation permet de construire une axiomatisation qui fournit les propriétés (comportementales) du système à développer en utilisant les concepts de base cités ci-après. Concepts de base Logique, Algèbre, Domaines déﬁnis inductivement. Exemples de formalisme les langages de spéciﬁcation algébriques : LPG, ASL, ACT ONE, CLEAR, OBJ, PLUSS, LARCH, CASL... pour les systèmes séquentiels les algèbres de processus : LOTOS (combine ACT ONE et CCS, CSP) pour les systèmes concurrents. Spéciﬁcations hybrides (hybrid approach) Principe La spéciﬁcation permet de compléter une axiomatisation par un modèle de données ou bien de compléter un modèle de données par une axiomatisation. Concepts de base Concepts de base des approches orientées état et propriétés. Exemples de formalisme – RAISE (Combine VDM et CSP) – VDM-SL et Réseaux de Petri, – Extended LOTOS(combine ACT ONE, CCS et CSP), – ZCCS (combine Z et CCS), – . . . Méthodes de développement formel Pour résumer l’essentiel des idées dans le processus de mise en place d’un logiciel reprenons en cœur le slogan : « Prouver c’est programmer et programmer c’est prouver ! » La deuxième façon de résumer est de considérer l’interprétation suivante de l’isomorphisme de Curry-Howard: Preuve est équivalent à Développement Axiomes Théorèmes Spécifications Programmations Il y a plusieurs approches dans les méthodes formelles : - l'approche opérationnelle : le développement est basé sur la description d'un système par un modèle qui a les propriétés du système. Vérification des propriétés sur le modèle. Des raffinements corrects successifs sont effectués sur le modèle. - l'approche axiomatique : le développement est basé sur l'axiomatisation qui décrit le comportement du système. Des vérifications des propriétés sont effectuées, raffinements possibles. - l'approche hybride Intégration de méthodes formelles Quelques définitions Méthode formelle = (1)Langage formel (syntaxe précise et sémantique précise) et (2) Système de preuve ou de raisonnement formel. Développement formel = transformation systématique des spéciﬁcations en programmes en utilisant des lois préséniles. Modelisation : Hoare : A scientific theory is formalised as a mathematical model of reality, from which can be deduced or calculated the observable properties and of a well-defined class of processes in the physical world. Il y a deux principales notions de modèles (en informatique). 1. Modèle = une approximation de la réalité par une structure mathématique. Un objet O est modèle d'une réalité R, si O permet de répondre aux questions que l'on se pose sur R. En Mathématique, Physique, ... système d’équations portant sur des grandeurs (masses, énergie, ...) ou des lois hypothétiques. Quelques définitions (suiv) 2. (Logique, théorie des modèles) Un modèle d'une théorie T est une structure dans laquelle les axiomes de T sont valides. Une structure S est modèle d'une théorie T, ou bien S satisfait T si toute formule de T est satisfaite dans S. La réalité est un modèle d'une théorie ! Théorie (du 1er ordre) = tout ensemble de formules logiques (du 1er ordre) dans un langage donnée (précisément défini). Modèle comme interprétation d'une spécification cation - une algèbre comme modèle d'une spécification cation algébrique (axiomatisation). Ces deux utilisations de modèle se retrouvent dans les approches orientée modèle (ou état) et orientée propriétés. Dans le langage courant, - modèle = (archétype), ce qui sert ou doit servir d'objet d'imitation pour reproduire quelque chose. - modèle = (paradigme), modèle de déclinaison, de conjugaison, etc - modèle = (référence), . . . Exemples de théories La théorie des ensembles : elle est basée sur un ensemble d'axiomes. Les objets de cette théorie sont appelés ensembles. La classe des ensembles est appelée univers. Les axiomes de la théorie des ensembles (de Zermelo+Fraenkel) sont les suivants : - Axiome de l'ensemble vide : il existe un ensemble qui ne contient aucun élément : c'est l'ensemble vide. - Axiome d'extensionalité : deux ensembles sont égaux si et seulement si ils contiennent exactement les mêmes éléments - Axiome de l'union : l'une union d'ensembles est un ensemble { Axiome de l'ensemble des parties :les parties d'un ensembles forment une partie - Axiome du schéma de remplacement (Fraenkel, 1922) : Lorsqu'on définit une fonction par uploads/s3/ methode-de-specification-et-developpement-formel-de-logiciel.pdf