Podpora výuky pro formální verifikaci hardwaru

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.