Informace o projektu

Formální metody pro analýzu a verifikaci komplexních systémů

Kód projektu
GAP202/10/1469
Období řešení
1/2010 - 12/2014
Investor/Program
Grantová agentura ČR
Programový rámec / typ projektu
Standardní projekty
Fakulta/Pracoviště MU
Fakulta informatiky
Klíčová slova
formální verifikace; stochastické systémy; teorie automatů; temporální logiky

Ve formální verifikaci se pomocí matematických metod dokazuje, že daný systém splňuje požadované vlastnosti. Verifikační a analytické metody jsou obvykle tvořeny na míru dané třídě systémů, která je charakterizována nějakou specifickou vlastností jako například náhodnost, závislost na reálném čase, počet stavů, apod. Reálné systémy jsou ale obvykle komplexní a kombinují více těchto charakteristických vlastností. Naším cílem je studovat verifikační a analytické metody pro systémy, které kombinují náhodnost s dalšími aspekty chování, jako je nedeterministická volba, reálný čas, interakce, apod. Speciální pozornost bude věnována systémům s nekonečně mnoha stavy. Studovány budou vlastnosti formálních modelů těchto systémů, například stochastických her s reálným časem, pravděpodobnostních zásobníkových automatů, systémů s čítači, popisných jazyků komunikačních protokolů, apod. Mezi cíle výzkumu patří také návrh nových formalismů vhodných pro specifikaci vlastností takových systémů a analýza rozhodnutelnosti a složitosti příslušných verifikačních problémů.

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info