Útmutató a Frama-C-vel végzett szoftverellenőrzéshez: Core Components, Usages, and Applications

Eredeti címe:

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

Könyv tartalma:

A Frama-C egy népszerű nyílt forráskódú eszközkészlet C programok elemzésére és verifikálására, amelyet nagyrészt oktatásban, kísérleti kutatásban és ipari alkalmazásokban használnak.

A modern szoftverek növekvő komplexitásával és mindenütt jelenlétével egyre nagyobb az érdeklődés a különböző formalizáltsági szintű kódelemző eszközök iránt a szoftvertermékek biztonságának és védelmének biztosítása érdekében. Elismerve azt a tényt, hogy egyetlen technika sem lesz képes kielégíteni az összes szoftverellenőrzési igényt, a Frama-C platform számos bővítményt tartalmaz, amelyek felhasználhatók vagy kombinálhatók az egyes ellenőrzési feladatok megoldására.

Ez az útmutató a Frama-C alapvető felhasználási módjait, kutatási eredményeit és konkrét alkalmazásait mutatja be a platform 2008-as első nyílt forráskódú kiadása óta. Kitér az ACSL specifikációs nyelvre, az alapvető verifikációs bővítményekre, a fejlett elemzésekre és azok kombinációira, az új bővítmények fejlesztésének legfontosabb összetevőire, valamint olyan sikeres ipari esettanulmányokra, amelyekben a Frama-C segített a mérnököknek a létfontosságú biztonsági vagy védelmi tulajdonságok verifikálásában.

Témák és jellemzők:

* Kíméletes, példákon alapuló bevezetés a szoftver specifikációba és verifikációba * A legmodernebb specifikációs és elemzési technikák széleskörű bemutatása * Lépésről lépésre útmutató saját, testre szabott elemzés kifejlesztéséhez a platformon* Inspiráló sikertörténetek a Frama-C ipari kódokon való alkalmazásáról* Több mint 15 év K+F a C kód elemzésével és verifikációjával kapcsolatban

Ez a könyv szilárdan a szoftverelemzés gyakorlatában gyökerezik, számos példával, gyakorlattal és alkalmazási útmutatóval. Mint ilyen, különösen alkalmas azon szoftververifikációs szakemberek számára, akik a verifikációt a kódjukon kívánják alkalmazni, valamint a kódelemzési technikákban kevés vagy semmilyen tapasztalattal nem rendelkező egyetemi hallgatók számára. Az elemzők elméleti alapjairól szóló haladóbb fejezetek a végzős hallgatók és kutatók számára lesznek érdekesek.

Nikolai Kosmatov a franciaországi Thales Research & Technology vezető kutatója. Virgile Prevosto vezető kutató és Julien Signoles kutatási igazgató, mindketten az Université Paris-Saclay, CEA, List, Franciaország.