Formální verifikace systémů

Problém korektnosti, tedy problém ověření (neboli verifikace), že daný počítačový (hardwarový a/nebo softwarový) systém má skutečně vlastnosti, které jsou požadovány jeho specifikací, patří mezi fundamentální praktické i teoretické problémy v oblasti informatiky.

Cílem předmětu je ukázat studentům některé přístupy, které se používají pro verifikaci systémů.
Jedna z prakticky úspěšných metod je tzv. `ověření modelu' (model checking), kde se testovaná vlastnost systému vyjádří pomocí formule některé z tzv. temporálních logik a ověřuje se (polo)automatickými metodami na modelu systému.

Další příkladem metod používaných v praxi je tzv. 'testování ekvivalence' (ekvivalence checking), kde máme na jedné straně model, který
reprezentuje specifikaci chování systému, tj. co očekáváme jako požadované chování systému, a na druhé straně model reprezentující implementaci, tj. způsob, jak je dané chování reálně implementováno. Cílem je ověřit, zda je chování obou těchto modelů v nějakém přesně definovaném smyslu ekvivalentní, a že se tedy daná implementace skutečně chová podle dané specifikace.

Další přístup je založen na vytváření důkazů korektnosti programů v některém systému pro interaktivní a automatizované dokazování (interactive and automated theorem proving). Existuje celá řada softwarových nástrojů, které umožňují interaktivně vytvářet
důkazy, přičemž automaticky kontrolují správnost těchto důkazů a do určité míry umožňují automatizovat některé mechanické kroky důkazu. Tato oblast je také silně propojena s problematikou sémantiky programovacích jazyků a teorie typů, protože aby bylo vůbec možné nějaké formální důkazy korektnosti programů vytvářet, nejprve musí být formálně reprezentována sémantika programů. Část přednášek tedy bude věnovaná této problematice. Dále pak budou studovány logiky používané pro dokazování vlastností programů - Hoarova logika a separační logika (což je modernější a obecnější rozšíření Hoarovy logiky o možnost dokazování korektnosti programů, které pracují s ukazateli a dynamicky alokovanými datovými strukturami).

Účelem kursu je vysvětlení základních principů těchto přístupů k verifikaci a zároveň demonstrace této verifikace na modelech konkrétních praktických problémů, za použití volně dostupných softwarových verifikačních nástrojů.

Výsledky učení:
- Získat základní přehled o některých metodách používaných při verifikací systémů.
Seznámit se s přístupy založenými na ověřování modelu (model checking), ověřování ekvivalence (equivalence checking) a s přístupy využívajícími nástroje pro interaktivní a automatizované dokazování.
- Seznámit se s různými matematickými formalismy používanými při verifikaci. Konkretně např. se způsoby, jak je možné formálně popisovat sémantiku programů a programovacích jazyků, s různými druhy logik používanými pro specifikaci vlastností systémů, jako jsou různé typy temporálních logik či logiky používanými pro verifikaci programů jako jsou Hoarova logika a separační logika. Seznámit se také se základy teorie typů.