| | |
|---|
| Údaje o projektu |
| Identifikační kód | GAP202/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 jazyce | Modelování a verifikace paralelních systémů |
| Poskytovatel | GA0 - Grantová agentura České republiky (GA ČR) |
| Program | GA - Standardní projekty (1993-…) |
| Kategorie VaV | ZV - Základní výzkum |
| Hlavní obor | IN - Informatika |
| Zahájení řešení | 1.1.2011 |
| Ukončení řešení | 31.12.2014 |
| Datum posledního uvolnění účelové podpory | 30.3.2012 |
| Číslo smlouvy | P202/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í | 2011 | 2012 | 2013 | 2014 | celkem |
|---|
| Výše podpory ze státního rozpočtu | 797 tis. Kč | 962 tis. Kč | 1 109 tis. Kč | 1 109 tis. Kč | 3 977 tis. Kč |
| Celkové uznané náklady | 797 tis. Kč | 962 tis. Kč | 1 109 tis. Kč | 1 109 tis. Kč | 3 977 tis. Kč |
| Typ | skutečně čerpané | skutečně čerpané | přidělené | plánované |
|
| Druh soutěže | VS - Veřejná soutěž ve výzkumu a vývoji |
| Veřejná soutěž ve výzkumu, vývoji a inovacích | SGA02011GA-ST - Veřejná soutěž (GA0/GA) |
| Cíle řešení v původním jazyce | Pro 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 jazyce | verification; modelling; parallel system; distributed system |
| Rok dodání údajů do CEP | 2013 |
| Systémové označení dodávky dat | CEP13-GA0-GA-R/03:4 |
| Datum dodání záznamu | 7.6.2013 |
| Účastníci projektu |
| Počet příjemců | 1 |
| Počet dalších účastníků projektu | 0 |
| Příjemce / Organizační jednotka garantující řešení | Vysoká škola báňská - Technická univerzita Ostrava / Fakulta elektrotechniky a informatiky |
| Řešitel | Prof. 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ík | 2011 | 2012 | 2013 | 2014 |
|---|
| Vysoká škola báňská - Technická univerzita Ostrava / Fakulta elektrotechniky a informatiky | 797 tis. Kč | 962 tis. Kč | 1 109 tis. Kč | 1 109 tis. Kč |
|
| Celkové uznané náklady | |
| Účastník | 2011 | 2012 | 2013 | 2014 |
|---|
| Vysoká škola báňská - Technická univerzita Ostrava / Fakulta elektrotechniky a informatiky | 797 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ýsledku | 1 |
| Počet výsledků v RIV | 10 |
| Výsledek druhu D | RIV/61989100:27240/12:86084986 - Bisimilarity of Probabilistic Pushdown Automata (2012) |
| Výsledek druhu D | RIV/61989100:27740/12:86084450 - Decidability of DPDA Language Equivalence via First-Order Grammars (2012) |
| Výsledek druhu J | RIV/61989100:27740/12:86084410 - Generating parallel applications from models based on Petri nets (2012) |
| Výsledek druhu D | RIV/61989100:27740/12:86084876 - Unidirectional channel systems can be tested (2012) |
| Výsledek druhu D | RIV/61989100:27740/12:86084661 - Usage of petri nets for high performance computing (2012) |
| Výsledek druhu J | RIV/61989100:27240/11:86080888 - Developing parallel applications using Kaira (2011) |
| Výsledek druhu D | RIV/61989100:27240/11:86081257 - Kaira: Modelling and Generation Tool Based on Petri Nets for Parallel Applications (2011) |
| Výsledek druhu J | RIV/61989100:27240/11:86080910 - Language Equivalence of Deterministic Real-Time One-Counter Automata Is NL-Complete (2011) |
| Výsledek druhu D | RIV/61989100:27240/11:86081255 - Parallelization of ant colony optimization algorithm using Kaira (2011) |
| Výsledek druhu J | RIV/61989100:27240/11:86080823 - Using Uppaal for Verification of Priority Assignment in Real-Time Databases (2011) |