Formal methods for analysis and verification of complex systems
Project goals
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.
Keywords
formalverificationstochasticsystemsautomatatheorytemporallogics
Public support
Provider
Czech Science Foundation
Programme
Standard projects
Call for proposals
Standardní projekty 13 (SGA02010GA-ST)
Main participants
—
Contest type
VS - Public tender
Contract ID
P202-10-1469
Alternative language
Project name in Czech
Formální metody pro analýzu a verifikaci komplexních systémů
Annotation in Czech
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ů.
Scientific branches
Completed project evaluation
Provider evaluation
V - Vynikající výsledky projektu (s mezinárodním významem atd.)
Project results evaluation
Project successfully investigated formal properties of time stochastic systems, infinite-state stochastic processes and games and probabilistic temporal logics. Project accomplished planned goals according to the plan.The project resulted in an impressive number and quality of publications. Project supported involvement of graduate students. No flaws have been identified.
Solution timeline
Realization period - beginning
Jan 1, 2010
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
7,332 thou. CZK
Public financial support
7,332 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK
Basic information
Recognised costs
7 332 CZK thou.
Public support
7 332 CZK thou.
100%
Provider
Czech Science Foundation
CEP
IN - Informatics
Solution period
01. 01. 2010 - 31. 12. 2014