Formal Verification of Stochastic Real-Time Systems
Project goals
We investigate formal verification techniques for systems that exhibit random behavior and operate under various real-time constraints (stochastic real-time systems, SRTS). Random aspects of systems are usually modeled using various kinds of stochastic processes. Real-time systems are typically modeled using variants of timed automata. In order to model SRTS, these formalisms have to be combined together. We concentrate on structural properties of such systems and computational complexity of basic verification problems. Another feature that is often present in real-world systems is nondeterminism, i.e. uncertainty without any statistical information. Nondeterminism also naturally occurs in problems where the goal is to synthesize an efficient controller of a system. SRTS with nondeterminism can be modeled using continuous-time decision processes with timed automata objectives. Here we are mainly interested in existence of controllers that achieve the objective and can be efficiently computed.
Keywords
GeneralizedSemi-MarkovProcessesreal-timesystemsformalverification
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
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
Recognised costs
827 CZK thou.
Public support
827 CZK thou.
0%
Provider
Czech Science Foundation
CEP
IN - Informatics
Solution period
01. 01. 2012 - 31. 12. 2014