Modelling and verification of parallel systems
Project goals
For scientific and engineering computations, processing of large data structures, etc., various types of parallel and distributed systems are increasingly used, including parallel supercomputers, networks of computers, multicore processors, or graphic chips of desktop computers. Design, implementation and verification of parallel systems is a live research area, with many open theoretical and methodological problems.The general goal of this project is to contribute to this area with new theoretical results and practically oriented methods. One of our concrete subgoals is to concentrate on some open problems of automated verification, e.g. those concerning decidability and complexity of behavioural equivalences. Another concrete subgoal is to explore possibilities of modelling parallel algorithms on a suitable level of abstraction; in particular, we have Petri net based formalisms in mind. As one of concrete outcomes of the project, we plan to develop a software tool, based on solid theoretical foundations, which makes modelling, analysis and verification of parallel systems easier.
Keywords
Public support
Provider
Czech Science Foundation
Programme
Standard projects
Call for proposals
Standardní projekty 14 (SGA02011GA-ST)
Main participants
—
Contest type
VS - Public tender
Contract ID
P202-11-0340
Alternative language
Project name in Czech
Modelování a verifikace paralelních systémů
Annotation in Czech
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 nasolidních teoretických základech, který usnadní modelování, analýzu a verifikaci paralelních systémů.
Scientific branches
Completed project evaluation
Provider evaluation
V - Vynikající výsledky projektu (s mezinárodním významem atd.)
Project results evaluation
Advances parallel program verification. Theoretical results concern pushdown automata equivalence (new proofs for known results and new results for particular classes of automata), practical side includes a software tool for implementing parallel programs over MPI based on models inspired by Petri Nets. The results were published at top tier venues (LICS, STOC, MFCS, ICALP).
Solution timeline
Realization period - beginning
Jan 1, 2011
Realization period - end
Dec 31, 2014
Project status
U - Finished project
Latest support payment
Mar 31, 2014
Data delivery to CEP
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data delivery code
CEP15-GA0-GA-U/01:1
Data delivery date
May 22, 2015
Finance
Total approved costs
3,938 thou. CZK
Public financial support
3,938 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK
Basic information
Recognised costs
3 938 CZK thou.
Public support
3 938 CZK thou.
100%
Provider
Czech Science Foundation
CEP
IN - Informatics
Solution period
01. 01. 2011 - 31. 12. 2014