Formální metody pro analýzu a verifikaci komplexních systémů
Cíle projektu
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ů.
Klíčová slova
formalverificationstochasticsystemsautomatatheorytemporallogics
Veřejná podpora
Poskytovatel
Grantová agentura České republiky
Program
Standardní projekty
Veřejná soutěž
Standardní projekty 13 (SGA02010GA-ST)
Hlavní účastníci
—
Druh soutěže
VS - Veřejná soutěž
Číslo smlouvy
P202-10-1469
Alternativní jazyk
Název projektu anglicky
Formal methods for analysis and verification of complex systems
Anotace anglicky
Formal verification utilizes mathematical methods for proving that a system satisfies desired properties. Verification methods are usually tailored for a specific class of systems characterized by some inherent property such as randomness, non-deterministic choice, real-time constraints, etc. However, real-world systems are usually complex and these features must be taken into account simultaneously. The project aims at designing new verification and analytical methods for systems that combine randomization with other behavioural aspects, such as non-deterministic choice, real-time, interaction, etc. A special emphasis is put on infinite-state systems. Various formal models of such systems will be investigated, including stochastic games with real-time, probabilistic pushdown automata, counter systems, description languages for communication protocols, etc. The project also aims at designing new specification formalism for such systems, and establishing the decidability and complexity results for thecorresponding verification problems.
Vědní obory
Kategorie VaV
ZV - Základní výzkum
CEP - hlavní obor
IN - Informatika
CEP - vedlejší obor
—
CEP - další vedlejší obor
—
OECD FORD - odpovídající obory
(dle převodníku)10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Hodnocení dokončeného projektu
Hodnocení poskytovatelem
V - Vynikající výsledky projektu (s mezinárodním významem atd.)
Zhodnocení výsledků projektu
Daný projekt se zabýval formálními vlastnostmi stochastických systémů se spojitým časem a nekonečně stavových stochastických procesů a her. Projekt se podařilo plnit podle plánu a všechny cíle byly splněny. Projekt vyprodukoval úctyhodné množství a kval?
Termíny řešení
Zahájení řešení
1. 1. 2010
Ukončení řešení
31. 12. 2014
Poslední stav řešení
U - Ukončený projekt
Poslední uvolnění podpory
31. 3. 2014
Dodání dat do CEP
Důvěrnost údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Systémové označení dodávky dat
CEP15-GA0-GA-U/01:1
Datum dodání záznamu
22. 5. 2015
Finance
Celkové uznané náklady
7 332 tis. Kč
Výše podpory ze státního rozpočtu
7 332 tis. Kč
Ostatní veřejné zdroje financování
0 tis. Kč
Neveřejné tuz. a zahr. zdroje finan.
0 tis. Kč
Základní informace
Uznané náklady
7 332 tis. Kč
Statní podpora
7 332 tis. Kč
100%
Poskytovatel
Grantová agentura České republiky
CEP
IN - Informatika
Doba řešení
01. 01. 2010 - 31. 12. 2014