Podpora výuky pro formální verifikaci hardwaru

grant

Formální analýza a verifikace v poslední době patří mezi moderní a rychle postupující metody v oblasti ověřování správnosti systémů. Tento přístup začíná být přijímán průmyslovými partnery zejména v oblasti hardwaru, zajímají se o něj i v české firmy, společnosti a konzorcia (například Cesnet prostřednictvím projektu Liberouter). I přes nesčetné množství publikací na téma formální verifikace je třeba mít hluboké znalosti v dané oblasti. Tento projekt se snaží o snížení obtížnosti přístupu k dané problematice, zabývá se přípravou praktické výuky formální verifikace, aplikací teorie formální verifikace na vzorových příkladech i na příkladech z praxe. Projekt nabízí přehled dostupných verifikačních nástrojů, ukazuje jejich výhody i omezení a prezentuje práci s s nástroji SMV a Uppaal. Součástí projektu jsou vypracované postupy procesu formální verifikace, úkoly na procvičení, jednoduché příklady i ukázky složitých problémů z projektu Liberouter.

Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT) , hlavní řešitel
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT) , spoluřešitel