Sprievodca verifikáciou softvéru pomocou Frama-C: Základné komponenty, použitie a aplikácie

Pôvodný názov:

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

Obsah knihy:

Frama-C je populárna open-source sada nástrojov na analýzu a verifikáciu programov v jazyku C, ktorá sa zväčša používa na výučbu, experimentálny výskum a priemyselné aplikácie.

S rastúcou zložitosťou a všadeprítomnosťou moderného softvéru rastie záujem o nástroje na analýzu kódu na rôznych úrovniach formalizácie s cieľom zabezpečiť bezpečnosť a ochranu softvérových produktov. Vzhľadom na skutočnosť, že žiadna technika nikdy nebude schopná vyhovieť všetkým potrebám verifikácie softvéru, platforma Frama-C obsahuje široký súbor zásuvných modulov, ktoré možno použiť alebo kombinovať na riešenie konkrétnych úloh verifikácie.

Táto príručka predstavuje rozsiahlu panorámu základných spôsobov použitia, výsledkov výskumu a konkrétnych aplikácií platformy Frama-C od prvého vydania platformy s otvoreným zdrojovým kódom v roku 2008. Zahŕňa jazyk špecifikácie ACSL, základné verifikačné zásuvné moduly, pokročilé analýzy a ich kombinácie, kľúčové zložky pre vývoj nových zásuvných modulov, ako aj úspešné priemyselné prípadové štúdie, v ktorých Frama-C pomohla inžinierom overiť kľúčové bezpečnostné alebo ochranné vlastnosti.

Témy a vlastnosti:

* Jemný, na príkladoch založený úvod do špecifikácie a verifikácie softvéru * Široká panoráma najmodernejších techník špecifikácie a analýzy * Sprievodca krok za krokom na vývoj vlastnej, na mieru šitej analýzy na platforme * Inšpiratívne príbehy úspešného nasadenia Frama-C na priemyselný kód * Viac ako 15 rokov výskumu a vývoja v oblasti analýzy a verifikácie kódu jazyka C

Táto kniha je pevne zakotvená v praxi softvérovej analýzy, s množstvom príkladov, cvičení a návodov na použitie. Ako taká je obzvlášť vhodná pre odborníkov z praxe, ktorí chcú nasadiť verifikáciu na svojom kóde, ako aj pre vysokoškolských študentov, ktorí majú len malé alebo žiadne skúsenosti s technikami analýzy kódu. Pokročilejšie časti o teoretických základoch analyzátorov budú zaujímavé pre postgraduálnych študentov a výskumníkov.

Nikolaj Kosmatov je vedúci výskumný pracovník v spoločnosti Thales Research & Technology, Francúzsko. Virgile Prevosto je vedúca výskumná pracovníčka a Julien Signoles je riaditeľ výskumu, obaja na Université Paris-Saclay, CEA, List, Francúzsko.