Guide to Software Verification with Frama-C: Core Components, Usages, and Applications
Frama-C ist ein populäres Open-Source-Toolset für die Analyse und Verifizierung von C-Programmen, das hauptsächlich in der Lehre, der experimentellen Forschung und bei industriellen Anwendungen eingesetzt wird.
Mit der zunehmenden Komplexität und Allgegenwärtigkeit moderner Software steigt das Interesse an Code-Analyse-Tools auf verschiedenen Formalisierungsebenen, um die Sicherheit von Softwareprodukten zu gewährleisten. In Anerkennung der Tatsache, dass keine einzelne Technik jemals in der Lage sein wird, alle Anforderungen an die Softwareverifikation zu erfüllen, bietet die Frama-C Plattform eine breite Palette von Plug-Ins, die zur Lösung spezifischer Verifikationsaufgaben verwendet oder kombiniert werden können.
Dieser Leitfaden präsentiert ein breites Panorama von grundlegenden Anwendungen, Forschungsergebnissen und konkreten Applikationen von Frama-C seit der ersten Open-Source-Veröffentlichung der Plattform im Jahr 2008. Es behandelt die ACSL-Spezifikationssprache, zentrale Verifikations-Plug-ins, fortgeschrittene Analysen und deren Kombinationen, Schlüsselkomponenten für die Entwicklung neuer Plug-ins sowie erfolgreiche Fallstudien aus der Industrie, in denen Frama-C Ingenieuren bei der Verifikation entscheidender Safety- oder Security-Eigenschaften geholfen hat.
Themen und Merkmale:
* Sanfte, beispielbasierte Einführung in die Softwarespezifikation und -verifikation * Breites Panorama modernster Spezifikations- und Analysetechniken * Schritt-für-Schritt-Anleitung zur Entwicklung eigener, maßgeschneiderter Analysen auf der Plattform* Inspirierende Erfolgsgeschichten des Frama-C-Einsatzes bei industriellem Code* Mehr als 15 Jahre Forschung und Entwicklung zur Analyse und Verifikation von C-Code
Dieses Buch ist fest in der Praxis der Softwareanalyse verwurzelt, mit zahlreichen Beispielen, Übungen und Anwendungsrichtlinien. Es eignet sich daher besonders gut für Praktiker der Softwareverifikation, die ihren Code verifizieren wollen, sowie für Studenten im Grundstudium, die wenig oder keine Erfahrung mit Codeanalysetechniken haben. Fortgeschrittene Abschnitte über die theoretischen Grundlagen der Analysatoren werden für Studenten und Forscher von Interesse sein.
Nikolai Kosmatov ist Senior Researcher bei Thales Research & Technology, Frankreich. Virgile Prevosto ist Senior Researcher und Julien Signoles ist Forschungsdirektor, beide an der Université Paris-Saclay, CEA, List, Frankreich.
| ISBN: | 9783031556074 |
| Autor: | |
| Verlag: | |
| Sprache: | Englisch |
| Einband: | Hardcover |
| Erscheinungsjahr: | 2024 |
| Seitenzahl: | 726 |
Derzeit verfügbar, auf Lager.
