Remerciez-le!

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

Methode de specification et developpement formel de logiciel

Génie Logiciel Méthode de Spéci ?cation et développement formel de logiciel Prof Atsa Etoundi Roger Ma? tre de conférences CDé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 CCycles 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 CInté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 Uni ?ed 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 insu ?sante Elles permettent de dégrossir le problèmes La sémantique des modèles conçus reste informelle et mal dé ?nie il y a un manque de rigueur mathématique analyse profonde du problème très di ?cile et couteuse Par conséquent il est di ?cile 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 CMé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 Un langage qui est un moyen pour exprimer et concevoir un système la nature de ce langage peut être symbolique graphique etc Une sémantique qui donne la signi ?cation des éléments du langage 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 CSpéci ?cation formelle La spéci ?cation 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 CDé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