Titre original :
Guide to Software Verification with Frama-C: Core Components, Usages, and Applications
Contenu du livre :
Frama-C est un ensemble d'outils populaires à code source ouvert pour l'analyse et la vérification des programmes C, largement utilisé pour l'enseignement, la recherche expérimentale et les applications industrielles.
La complexité et l'omniprésence croissantes des logiciels modernes suscitent un intérêt grandissant pour les outils d'analyse de code à différents niveaux de formalisation afin de garantir la sûreté et la sécurité des produits logiciels. Reconnaissant le fait qu'aucune technique unique ne pourra jamais répondre à tous les besoins de vérification des logiciels, la plateforme Frama-C propose un large éventail de plug-ins qui peuvent être utilisés ou combinés pour résoudre des tâches de vérification spécifiques.
Ce guide présente un large panorama des utilisations de base, des résultats de recherche et des applications concrètes de Frama-C depuis la toute première version open-source de la plateforme en 2008. Il couvre le langage de spécification ACSL, les plug-ins de vérification de base, les analyses avancées et leurs combinaisons, les ingrédients clés pour le développement de nouveaux plug-ins, ainsi que des études de cas industrielles réussies dans lesquelles Frama-C a aidé les ingénieurs à vérifier des propriétés de sûreté ou de sécurité cruciales.
Sujets et caractéristiques :
* Introduction douce, basée sur des exemples, à la spécification et à la vérification des logiciels * Large panorama des techniques de spécification et d'analyse de pointe * Guide étape par étape pour développer votre propre analyse sur mesure à partir de la plate-forme* Exemples de réussite inspirants du déploiement de Frama-C sur du code industriel* Plus de 15 ans de R&D sur l'analyse et la vérification du code C
Ce livre est fermement ancré dans la pratique de l'analyse logicielle, avec de nombreux exemples, exercices et directives d'application. En tant que tel, il est particulièrement bien adapté aux praticiens de la vérification de logiciels souhaitant déployer la vérification sur leur code, ainsi qu'aux étudiants de premier cycle ayant peu ou pas d'expérience dans les techniques d'analyse de code. Les sections plus avancées sur les fondements théoriques des analyseurs intéresseront les étudiants de troisième cycle et les chercheurs.
Nikolai Kosmatov est chercheur principal à Thales Research & Technology, France. Virgile Prevosto est chercheur principal et Julien Signoles est directeur de recherche, tous deux à l'Université Paris-Saclay, CEA, List, France.
Autres informations sur le livre :
| ISBN : | 9783031556074 |
| Auteur : | |
| Éditeur : | |
| Langue : | anglais |
| Reliure : | Relié |
| Année de publication : | 2024 |
| Nombre de pages : | 726 |
Achat:
Actuellement disponible, en stock.
