Formal Verification of Stochastic Real-Time Systems
Public support
Provider
Czech Science Foundation
Programme
Post-graduate (doctorate) grants
Call for proposals
Postdoktorandské granty 12 (SGA02012GA1PD)
Main participants
—
Contest type
VS - Public tender
Contract ID
P202-12-P612
Alternative language
Project name in Czech
Formální verifikace stochastických systémů s reálným časem
Annotation in Czech
Předmětem našeho výzkumu je formální verifikace systémů, které vykazují náhodné chování a zároveň musí splňovat různá časová omezení (stochastic real-time systems, SRTS). Náhodné aspekty systémů se obvykle modelují pomocí stochastických procesů. Systémypracující v reálném čase jsou typicky modelovány pomocí časových automatů. Abychom byli schopni modelovat SRTS, musíme tyto formalismy vhodně spojit. Koncentrujeme se zejména na strukturální vlastnosti takových systémů a výpočetní složitost základních verifikačních problémů. Další obvyklou vlastností reálných systémů je nedeterminismus, tedy nejistota v chování bez jakékoliv statistické znalosti. Nedeterminismus se také objevuje v problémech, v nichž je třeba syntetizovat řídící jednotku systému. SRTS snedeterminismem lze modelovat pomocí rozhodovacích procesů se spojitým časem, jejichž cílové podmínky lze vyjádřit pomocí časových automatů. V této oblasti se zabýváme zejména existencí řídící jednotky, která splňuje cílovou podmínku a zároveň ji lze algoritmicky konstruovat.
Scientific branches
R&D category
ZV - Basic research
CEP classification - main branch
IN - Informatics
CEP - secondary branch
—
CEP - another secondary branch
—
OECD FORD - equivalent branches <br>(according to the <a href="http://www.vyzkum.cz/storage/att/E6EF7938F0E854BAE520AC119FB22E8D/Prevodnik_oboru_Frascati.pdf">converter</a>)
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Completed project evaluation
Provider evaluation
U - Uspěl podle zadání (s publikovanými či patentovanými výsledky atd.)
Project results evaluation
The project has brought new high-quality results in the area of analysis and verification of stochastic systems. Several papers have been accepted and presented at premier publication venues (like conferences ICALP or LICS) and some results also have a potential of being quickly applicable, which has already been shown experimentally.
Solution timeline
Realization period - beginning
Jan 1, 2012
Realization period - end
Dec 31, 2014
Project status
U - Finished project
Latest support payment
Mar 19, 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-GP-U/02:2
Data delivery date
May 6, 2016
Finance
Total approved costs
827 thou. CZK
Public financial support
827 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK