Przewodnik po weryfikacji oprogramowania za pomocą Frama-C: Podstawowe komponenty, zastosowania i aplikacje

Oryginalny tytuł:

Guide to Software Verification with Frama-C: Core Components, Usages, and Applications

Zawartość książki:

Frama-C to popularny zestaw narzędzi open-source do analizy i weryfikacji programów w języku C, wykorzystywany głównie do nauczania, badań eksperymentalnych i zastosowań przemysłowych.

Wraz z rosnącą złożonością i wszechobecnością nowoczesnego oprogramowania, rośnie zainteresowanie narzędziami do analizy kodu na różnych poziomach formalizacji, aby zapewnić bezpieczeństwo produktów programistycznych. Uznając fakt, że żadna pojedyncza technika nigdy nie będzie w stanie zaspokoić wszystkich potrzeb związanych z weryfikacją oprogramowania, platforma Frama-C oferuje szeroki zestaw wtyczek, które można wykorzystać lub połączyć w celu rozwiązania określonych zadań weryfikacyjnych.

Niniejszy przewodnik przedstawia szeroką panoramę podstawowych zastosowań, wyników badań i konkretnych aplikacji Frama-C od czasu pierwszego wydania platformy open-source w 2008 roku. Obejmuje on język specyfikacji ACSL, podstawowe wtyczki weryfikacyjne, zaawansowane analizy i ich kombinacje, kluczowe składniki do opracowywania nowych wtyczek, a także udane studia przypadków przemysłowych, w których Frama-C pomogła inżynierom zweryfikować kluczowe właściwości bezpieczeństwa lub ochrony.

Tematy i funkcje:

* Łagodne, oparte na przykładach wprowadzenie do specyfikacji i weryfikacji oprogramowania * Szeroka panorama najnowocześniejszych technik specyfikacji i analizy * Przewodnik krok po kroku umożliwiający opracowanie własnej, dostosowanej do potrzeb analizy na platformie * Inspirujące historie sukcesu wdrożenia Frama-C w kodzie przemysłowym * Ponad 15 lat badań i rozwoju w zakresie analizy i weryfikacji kodu C

Ta książka jest mocno zakorzeniona w praktyce analizy oprogramowania, z licznymi przykładami, ćwiczeniami i wskazówkami dotyczącymi zastosowań. Jako taka, jest szczególnie odpowiednia dla praktyków weryfikacji oprogramowania, którzy chcą wdrożyć weryfikację w swoim kodzie, a także dla studentów studiów licencjackich z niewielkim lub żadnym doświadczeniem w technikach analizy kodu. Bardziej zaawansowane sekcje dotyczące teoretycznych podstaw analizatorów będą interesujące dla absolwentów i naukowców.

Nikolai Kosmatov jest starszym pracownikiem naukowym w Thales Research & Technology we Francji. Virgile Prevosto jest starszym badaczem, a Julien Signoles jest dyrektorem ds. badań, oboje na Université Paris-Saclay, CEA, List, Francja.