Guida alla verifica del software con Frama-C: Componenti principali, usi e applicazioni

Titolo originale:

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

Contenuto del libro:

Frama-C è un popolare set di strumenti open-source per l'analisi e la verifica dei programmi C, largamente utilizzato per l'insegnamento, la ricerca sperimentale e le applicazioni industriali.

Con la crescente complessità e ubiquità del software moderno, c'è un crescente interesse per gli strumenti di analisi del codice a vari livelli di formalizzazione per garantire la sicurezza dei prodotti software. Riconoscendo il fatto che nessuna singola tecnica sarà mai in grado di soddisfare tutte le esigenze di verifica del software, la piattaforma Frama-C presenta un'ampia serie di plug-in che possono essere utilizzati o combinati per risolvere compiti di verifica specifici.

Questa guida presenta un ampio panorama di usi di base, risultati di ricerca e applicazioni concrete di Frama-C a partire dal primo rilascio open-source della piattaforma nel 2008. Copre il linguaggio di specifica ACSL, i plug-in di verifica principali, le analisi avanzate e le loro combinazioni, gli ingredienti chiave per lo sviluppo di nuovi plug-in, nonché casi di studio industriali di successo in cui Frama-C ha aiutato gli ingegneri a verificare proprietà cruciali di sicurezza o protezione.

Argomenti e caratteristiche:

* Introduzione delicata ed esemplificativa alla specifica e alla verifica del software * Ampio panorama di tecniche di specifica e di analisi all'avanguardia * Guida passo-passo per sviluppare la propria analisi su misura in base alla piattaforma* Storie di successo ispirate dall'impiego di Frama-C su codice industriale* Oltre 15 anni di ricerca e sviluppo sull'analisi e la verifica del codice C

Questo libro è saldamente ancorato alla pratica dell'analisi del software, con numerosi esempi, esercizi e linee guida applicative. Per questo motivo, è particolarmente adatto ai professionisti della verifica del software che desiderano implementare la verifica sul proprio codice, nonché agli studenti universitari con poca o nessuna esperienza nelle tecniche di analisi del codice. Le sezioni più avanzate sui fondamenti teorici degli analizzatori saranno di interesse per gli studenti laureati e i ricercatori.

Nikolai Kosmatov è ricercatore senior presso Thales Research & Technology, Francia. Virgile Prevosto è ricercatore senior e Julien Signoles è direttore di ricerca, entrambi presso l'Université Paris-Saclay, CEA, List, Francia.