University Sétif 1 FERHAT ABBAS Faculty of Sciences
Résultat de la recherche
1 résultat(s) recherche sur le mot-clé 'Algorithmes Langages de programmation Programmation système (informatique) Logique informatique Logiciels : Vérification'
Ajouter le résultat dans votre panier Affiner la recherche Générer le flux rss de la recherche
Partager le résultat de cette recherche
Cours et exercices corrigés d'algorithmique / Jacques Julliand
Titre : Cours et exercices corrigés d'algorithmique : Vérifier, tester et concevoir des programmes en les modélisant ; licence et master d'informatique Type de document : texte imprimé Auteurs : Jacques Julliand, Auteur Editeur : Paris : Vuibert Année de publication : 2010 Importance : 1 vol. (264 p.) Présentation : ill., couv. ill. en coul. Format : 24 cm ISBN/ISSN/EAN : 978-2-311-00020-7 Note générale : 978-2-311-00020-7 Langues : Français (fre) Langues originales : Français (fre) Catégories : Informatique Mots-clés : Algorithmes
Langages de programmation
Programmation système (informatique)
Logique informatique
Logiciels : VérificationIndex. décimale : 005.1 Programmation Résumé :
Dans le monde de l'industrie et des services, la validation et la vérification des logiciels sont aujourd'hui des enjeux sécuritaires et économiques majeurs. La sécurité des passagers des véhicules de transport dépend par exemple de la sûreté des logiciels qui en contrôlent les fonctions motrices, tout comme la survie économique des fabricants de produits diffusés à des centaines de milliers d'exemplaires serait remise en cause si le logiciel embarqué se révélait erroné et devait être remplacé. L'utilisation d'environnements de développement de logiciels intégrant des outils d'aide à la vérification et à la validation (JAVA/ _JML, C#/SPEC#, C/ACSL, Atelier B, Scade, Esterel, etc.) va se généraliser et, dans cette perspective, les futurs utilisateurs devront maîtriser ces outils autant que les techniques sous-jacentes. À la base des techniques de vérification, la logique de Hoare est au cœur de cet ouvrage. On trouvera ici comment utiliser cette méthode pour vérifier et concevoir des logiciels sûrs. L'auteur montre également comment modéliser des systèmes informatiques dans le paradigme logico-ensembliste, puis comment les vérifier et les tester en recourant aux outils de la méthode B. Divisé en deux parties, ce manuel contient une introduction didactique des principes fondamentaux de la technique de vérification par application des règles de la logique de Hoare. Les concepts de la méthode de vérification sont introduits en montrant les similitudes et les différences avec la méthode de test fonctionnel boîte noire. On trouvera notamment des éléments de stratégie utilisant ces concepts pour vérifier et pour concevoir des logiciels. La seconde partie est consacrée a des questions pratiques liées à la mise en oeuvre de la méthode avec des outils - Atelier B et Leirios Test Generator - assistant la vérification et la génération de tests. Elle inclut le langage d'entrée de ces outils : la modélisation des logiciels en B. L'ensemble est illustré de nombreux exercices corrigésNote de contenu :
Sommaire
Modéliser pour vérifier et développer des programmes
Test et vérification de programmes
Vérification de programmes par exécution symbolique
Un langage de programmation générique
La logique des prédicats du premier ordre - le langage de modélisation du premier ordre
La logique de Hoare - le système de vérification
Quelques éléments de stratégie de vérification de programmes
Exemple de découverte d'erreurs à la vérification
Etude de cas - modélisation et vérification d'un programme de calcul de la racine carrée entière par division
Développer des programmes corrects par construction à partir de modèles
Automatisation de la vérification et de la génération de tests à partir de modèles
Modélisation de programmes en B
Modéliser en B pour engendrer des tests boîte noire
Modéliser des programmes en B pour les vérifier
Solutions des exercicesCôte titre : Fs/4633,Fs/13096-13099 Cours et exercices corrigés d'algorithmique : Vérifier, tester et concevoir des programmes en les modélisant ; licence et master d'informatique [texte imprimé] / Jacques Julliand, Auteur . - Paris : Vuibert, 2010 . - 1 vol. (264 p.) : ill., couv. ill. en coul. ; 24 cm.
ISBN : 978-2-311-00020-7
978-2-311-00020-7
Langues : Français (fre) Langues originales : Français (fre)
Catégories : Informatique Mots-clés : Algorithmes
Langages de programmation
Programmation système (informatique)
Logique informatique
Logiciels : VérificationIndex. décimale : 005.1 Programmation Résumé :
Dans le monde de l'industrie et des services, la validation et la vérification des logiciels sont aujourd'hui des enjeux sécuritaires et économiques majeurs. La sécurité des passagers des véhicules de transport dépend par exemple de la sûreté des logiciels qui en contrôlent les fonctions motrices, tout comme la survie économique des fabricants de produits diffusés à des centaines de milliers d'exemplaires serait remise en cause si le logiciel embarqué se révélait erroné et devait être remplacé. L'utilisation d'environnements de développement de logiciels intégrant des outils d'aide à la vérification et à la validation (JAVA/ _JML, C#/SPEC#, C/ACSL, Atelier B, Scade, Esterel, etc.) va se généraliser et, dans cette perspective, les futurs utilisateurs devront maîtriser ces outils autant que les techniques sous-jacentes. À la base des techniques de vérification, la logique de Hoare est au cœur de cet ouvrage. On trouvera ici comment utiliser cette méthode pour vérifier et concevoir des logiciels sûrs. L'auteur montre également comment modéliser des systèmes informatiques dans le paradigme logico-ensembliste, puis comment les vérifier et les tester en recourant aux outils de la méthode B. Divisé en deux parties, ce manuel contient une introduction didactique des principes fondamentaux de la technique de vérification par application des règles de la logique de Hoare. Les concepts de la méthode de vérification sont introduits en montrant les similitudes et les différences avec la méthode de test fonctionnel boîte noire. On trouvera notamment des éléments de stratégie utilisant ces concepts pour vérifier et pour concevoir des logiciels. La seconde partie est consacrée a des questions pratiques liées à la mise en oeuvre de la méthode avec des outils - Atelier B et Leirios Test Generator - assistant la vérification et la génération de tests. Elle inclut le langage d'entrée de ces outils : la modélisation des logiciels en B. L'ensemble est illustré de nombreux exercices corrigésNote de contenu :
Sommaire
Modéliser pour vérifier et développer des programmes
Test et vérification de programmes
Vérification de programmes par exécution symbolique
Un langage de programmation générique
La logique des prédicats du premier ordre - le langage de modélisation du premier ordre
La logique de Hoare - le système de vérification
Quelques éléments de stratégie de vérification de programmes
Exemple de découverte d'erreurs à la vérification
Etude de cas - modélisation et vérification d'un programme de calcul de la racine carrée entière par division
Développer des programmes corrects par construction à partir de modèles
Automatisation de la vérification et de la génération de tests à partir de modèles
Modélisation de programmes en B
Modéliser en B pour engendrer des tests boîte noire
Modéliser des programmes en B pour les vérifier
Solutions des exercicesCôte titre : Fs/4633,Fs/13096-13099 Exemplaires (5)
Code-barres Cote Support Localisation Section Disponibilité Fs/13096 Fs/13096-13099 livre Bibliothéque des sciences Français Disponible
DisponibleFs/13097 Fs/13096-13099 livre Bibliothéque des sciences Français Disponible
DisponibleFs/13098 Fs/13096-13099 livre Bibliothéque des sciences Français Disponible
DisponibleFs/13099 Fs/13096-13099 livre Bibliothéque des sciences Français Disponible
DisponibleFs/4633 Fs/4633 livre Bibliothéque des sciences Français Disponible
Disponible