Verifikace vestavěných systémů se složitou Booleovskou strukturou
Pro modelování složitých technických systémů (např. vlaky, letadla) se může
používat formalismus hybridních dynamických systémů. Jsme autoři znamého
softwarového balíku pro ověřování správnosti takových systémů.
Ale výsledek modelování složitých technických systémů většinou obsahuje
složitou Booleovskou strukturu. Náš algoritmus sice umí poměrně dobře
zacházet se spojitou strukturou, která modeluje fyzikální okolí daného
systému, ale ještě není schopen zacházet se složitou Booleovskou
strukturou. Cílem této práce je návrh a implementace algoritmu, který
odstraňuje tento nedostatek.