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é | Editeur : | Paris : Vuibert | Année de publication : | impr. 2010 | Importance : | 1 vol. (VIII-264 p.) | Présentation : | ill., couv. ill. en coul. | Format : | 24 cm | ISBN/ISSN/EAN : | 978-2-311-00020-7 | Note générale : | Bibliogr. p. 260-261. Index | Langues : | Français | Tags : | Ordinateurs Programmation Problèmes et exercices Algorithmes Informatique | Index. décimale : | | 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 validait": (JAVA/JML, C#ISPEC#, 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. A 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 Iogico-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 y 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 à des questions pratiques liées à la mise en œuvre 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és. | Note de contenu : | Sommaire
Traverser Paris par des ruelles tranquilles, des jardins et des squares, en se jouant des artères encombrées et bruyantes..
lmpossible? Tel est pourtant le programme de ces promenades buissonnières et piétonnes qui donnent à découvrir la ville sous un visage qu'on lui avait (presque) oublié
Des anciens villages aux nouveaux quartiers, le promeneur pourra choisir à sa guise et selon son humeur le type de panorama urbain qu'il souhaite arpenter
Chaque promenade, longue de 3 à 7 kilomètres, est figurée clairement, étape par étape, sur des plans aquarellés qui épargnent aux amateurs de balades citadines les difficultés de repérage, pour privilégier le bonheur simple de marcher dans Paris. |
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é] . - Paris : Vuibert, impr. 2010 . - 1 vol. (VIII-264 p.) : ill., couv. ill. en coul. ; 24 cm. ISBN : 978-2-311-00020-7 Bibliogr. p. 260-261. Index Langues : Français Tags : | Ordinateurs Programmation Problèmes et exercices Algorithmes Informatique | Index. décimale : | | 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 validait": (JAVA/JML, C#ISPEC#, 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. A 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 Iogico-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 y 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 à des questions pratiques liées à la mise en œuvre 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és. | Note de contenu : | Sommaire
Traverser Paris par des ruelles tranquilles, des jardins et des squares, en se jouant des artères encombrées et bruyantes..
lmpossible? Tel est pourtant le programme de ces promenades buissonnières et piétonnes qui donnent à découvrir la ville sous un visage qu'on lui avait (presque) oublié
Des anciens villages aux nouveaux quartiers, le promeneur pourra choisir à sa guise et selon son humeur le type de panorama urbain qu'il souhaite arpenter
Chaque promenade, longue de 3 à 7 kilomètres, est figurée clairement, étape par étape, sur des plans aquarellés qui épargnent aux amateurs de balades citadines les difficultés de repérage, pour privilégier le bonheur simple de marcher dans Paris. |
| |