Remerciez-le!

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

Developpemen et validation de logiciels methodes formelles pdf

Développement et validation de logiciels Méthodes formelles par Patrick BELLOT Département informatique École Nationale Supérieure des Télécommunications Jean-Philippe COTTIN Département informatique École Nationale Supérieure des Télécommunications et Jean-François MONIN France Télécom Centre National d ? Études des Télécommunications Lannion Généralités Bref historique Niveaux d ? utilisation des méthodes formelles Méthodes formelles et cycle de vie du logiciel Bases mathématiques Logique du premier ordre Théorie des ensembles Notions sur les systèmes de types Méthodes ensemblistes Méthode VDM Méthode Z Méthode B Types abstraits algébriques Domaine des protocoles Estelle Logique temporelle Approche synchrone Logiques d ? ordre supérieur logiques constructives Ordre supérieur Introduction du typage Modes d ? utilisation des logiques typées Conclusion Pour en savoir plus H - ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? ?? Doc H A lors que les ingénieurs électroniciens savent concevoir des matériels qui fonctionnent et que les ingénieurs du b? timent savent construire des ouvrages qui tiennent l ? ingénieur informaticien semble incapable de produire des applications répondant parfaitement aux besoins qu ? elles doivent satisfaire Quiconque a connu l ? industrie de l ? informatique sait que lorsqu ? une application est produite il y a un nombre très élevé d ? allers et retours entre l ? équipe de développement et les utilisateurs de l ? application a ?n que celle-ci soit modi ?ée Et même lorsque tout semble satisfaisant on peut être certain que des problèmes surgiront encore Les raisons souvent avancées sont le manque de précision ou l ? incohérence dans l ? expression des besoins des utilisateurs ce que l ? on appelle Toute reproduction sans autorisation du Centre français d ? exploitation du droit de copie est strictement interdite ? Techniques de l ? Ingénieur traité Informatique H ?? CDÉVELOPPEMENT ET VALIDATION DE LOGICIELS MÉTHODES FORMELLES les spéci ?cations Ces raisons peuvent être aussi la non-conformité de l ? application par rapport aux spéci ?cations ou bien encore de simples problèmes de fonctionnement de l ? application La spéci ?cation en langage dit naturel permet au spéci ?cateur d ? utiliser les moyens qui lui semblent les plus appropriés à ce qu ? il veut décrire le français ou l ? anglais un exemple de comportement une table un programme une référence etc Ces moyens sont de plus accessibles au plus grand nombre d ? informaticiens En revanche ils peuvent favoriser l ? apparition d ? ambigu? tés dissimulées dans un verbiage excessif ou peu structuré Ils ne permettent aucune analyse sérieuse de détection des incohérences ou des incomplétudes dans les spéci ?cations Ils ne permettent ni d ? obtenir une application certi ?ée conforme aux spéci ?cations ni de véri ?er a posteriori qu ? une application est conforme à ces mêmes spéci ?cations Les techniques formelles et leurs langages favorisent la ma? trise du cycle de vie du logiciel ?? ils permettent une expression formelle des spéci ?cations se prêtant à une interprétation précise