• česky
  • english

GAP202/11/0340 - Modelování a verifikace paralelních systémů (2011-2014, GA0/GA)

Údaje o projektu
Identifikační kódGAP202/11/0340
Důvěrnost údajůS - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
Název v původním jazyceModelování a verifikace paralelních systémů
PoskytovatelGA0 - Grantová agentura České republiky (GA ČR)
ProgramGA - Standardní projekty (1993-…)
Kategorie VaVZV - Základní výzkum
Hlavní oborIN - Informatika
Zahájení řešení1.1.2011
Ukončení řešení31.12.2014
Datum posledního uvolnění účelové podpory30.3.2012
Číslo smlouvyP202/11/0340
Poslední stav řešeníB - Běžící víceletý projekt, tj. takový, že byl řešen již v předcházejícím roce a bude řešen i v následujícím roce a v příslušném roce sběru dat jsou na něj poskytnuty finanční prostředky
Finance projektu
Období2011201220132014celkem
Výše podpory ze státního rozpočtu797 tis. Kč962 tis. Kč1 109 tis. Kč1 109 tis. Kč3 977 tis. Kč
Celkové uznané náklady797 tis. Kč962 tis. Kč1 109 tis. Kč1 109 tis. Kč3 977 tis. Kč
Typskutečně čerpanéskutečně čerpanépřidělenéplánované
Druh soutěžeVS - Veřejná soutěž ve výzkumu a vývoji
Veřejná soutěž ve výzkumu, vývoji a inovacíchSGA02011GA-ST - Veřejná soutěž (GA0/GA)
Cíle řešení v původním jazycePro vědeckotechnické výpočty, zpracování velkých datových struktur apod. jsou stále více využívány různé paralelní a distribuované systémy, ať už jde o různé typy paralelních superpočítačů, sítě počítačů, nebo jen vícejádrové procesory či grafické čipy běžných počítačů. Oblast návrhu, implementace a verifikace algoritmů pro tyto systémy je předmětem živého celosvětového výzkumu, s celou řadou otevřených teoretických a metodologických problémů. Obecným cílem projektu je přispět do této oblasti novými teoretickými výsledky i prakticky orientovanými postupy. Jedním z konkrétních cílů, na které se chceme zaměřit, jsou otevřené otázky automatizované verifikace, např. týkající se algoritmické rozhodnutelnosti a výpočetní složitosti behaviorálních ekvivalencí. Dalším konkrétním cílem je prozkoumání možností modelování paralelních algoritmů na vhodné úrovni abstrakce; speciálně máme na mysli formalizmy vycházející z Petriho sítí. Jedním z plánovaných výsledků je vytvoření softwarového nástroje, založeného na solidních teoretických základech, který usnadní modelování, analýzu a verifikaci paralelních systémů.
Klíčová slova v anglickém jazyceverification; modelling; parallel system; distributed system
Rok dodání údajů do CEP2013
Systémové označení dodávky datCEP13-GA0-GA-R/03:4
Datum dodání záznamu7.6.2013
Účastníci projektu
Počet příjemců1
Počet dalších účastníků projektu0
Příjemce / Organizační jednotka garantující řešeníVysoká škola báňská - Technická univerzita Ostrava / Fakulta elektrotechniky a informatiky
ŘešitelProf. RNDr. Petr Jančar, CSc. (státní příslušnost: CZ - Česká republika; tel.: 597 323 476)
Finance účastníků projektu
Poznámka: Finance účastníků projektu jsou sledovány od roku 2007
Výše podpory ze státního rozpočtu
Účastník2011201220132014
Vysoká škola báňská - Technická univerzita Ostrava / Fakulta elektrotechniky a informatiky797 tis. Kč962 tis. Kč1 109 tis. Kč1 109 tis. Kč
Celkové uznané náklady
Účastník2011201220132014
Vysoká škola báňská - Technická univerzita Ostrava / Fakulta elektrotechniky a informatiky797 tis. Kč962 tis. Kč1 109 tis. Kč1 109 tis. Kč
Výsledky projektu v RIV
Očekávané výsledky projektu
O - Ostatní výsledky nezařaditelné do žádného z výše uvedených druhů výsledku1
Počet výsledků v RIV10
Výsledek druhu DRIV/61989100:27240/12:86084986 - Bisimilarity of Probabilistic Pushdown Automata (2012)
Výsledek druhu DRIV/61989100:27740/12:86084450 - Decidability of DPDA Language Equivalence via First-Order Grammars (2012)
Výsledek druhu JRIV/61989100:27740/12:86084410 - Generating parallel applications from models based on Petri nets (2012)
Výsledek druhu DRIV/61989100:27740/12:86084876 - Unidirectional channel systems can be tested (2012)
Výsledek druhu DRIV/61989100:27740/12:86084661 - Usage of petri nets for high performance computing (2012)
Výsledek druhu JRIV/61989100:27240/11:86080888 - Developing parallel applications using Kaira (2011)
Výsledek druhu DRIV/61989100:27240/11:86081257 - Kaira: Modelling and Generation Tool Based on Petri Nets for Parallel Applications (2011)
Výsledek druhu JRIV/61989100:27240/11:86080910 - Language Equivalence of Deterministic Real-Time One-Counter Automata Is NL-Complete (2011)
Výsledek druhu DRIV/61989100:27240/11:86081255 - Parallelization of ant colony optimization algorithm using Kaira (2011)
Výsledek druhu JRIV/61989100:27240/11:86080823 - Using Uppaal for Verification of Priority Assignment in Real-Time Databases (2011)