Guide to Software Verification with Frama-C: Componente de bază, utilizări și aplicații

Titlul original:

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

Conținutul cărții:

Frama-C este un set popular de instrumente open-source pentru analiza și verificarea programelor C, utilizat în mare măsură pentru predare, cercetare experimentală și aplicații industriale.

Odată cu creșterea complexității și ubicuitatea software-ului modern, există un interes crescut pentru instrumentele de analiză a codului la diferite niveluri de formalizare pentru a asigura siguranța și securitatea produselor software. Recunoscând faptul că nicio tehnică unică nu va putea vreodată să satisfacă toate nevoile de verificare a software-ului, platforma Frama-C oferă un set larg de plug-in-uri care pot fi utilizate sau combinate pentru rezolvarea unor sarcini specifice de verificare.

Acest ghid prezintă o vastă panoramă a utilizărilor de bază, a rezultatelor cercetării și a aplicațiilor concrete ale Frama-C de la prima versiune open-source a platformei în 2008. Acesta acoperă limbajul de specificații ACSL, plug-in-urile de verificare de bază, analizele avansate și combinațiile acestora, ingredientele cheie pentru dezvoltarea de noi plug-in-uri, precum și studii de caz industriale de succes în care Frama-C a ajutat inginerii să verifice proprietăți esențiale de siguranță sau securitate.

Subiecte și caracteristici:

* Introducere blândă, bazată pe exemple, în specificarea și verificarea software-ului * Vastă panoramă a tehnicilor de specificare și analiză de ultimă oră * Ghid pas cu pas pentru a dezvolta propria analiză personalizată pe baza platformei * Povești inspirate de succes ale implementării Frama-C pe cod industrial * Peste 15 ani de cercetare și dezvoltare în analiza și verificarea codului C

Această carte este ferm înrădăcinată pe practica analizei software, cu numeroase exemple, exerciții și ghiduri de aplicare. Ca atare, este deosebit de potrivită pentru practicienii verificării software care doresc să implementeze verificarea pe codul lor, precum și pentru studenții universitari cu puțină sau nicio experiență în tehnicile de analiză a codului. Secțiunile mai avansate privind fundamentele teoretice ale analizoarelor vor fi de interes pentru studenții absolvenți și cercetători.

Nikolai Kosmatov este cercetător principal la Thales Research & Technology, Franța. Virgile Prevosto este cercetător principal și Julien Signoles este director de cercetare, ambii la Universitatea Paris-Saclay, CEA, List, Franța.