Project information

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

Investor logo
Project Identification
GAP202/10/1469
Project Period
1/2010 - 12/2014
Investor / Pogramme / Project type
Czech Science Foundation
MU Faculty or unit
Faculty of Informatics
Keywords
formal verification; stochastic systems; automata theory; temporal logics

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ů.

Publications

Total number of publications: 33


Previous 1 2 3 4 Next