Formal verification: algorithms, properties of modelling formalisms and temporal logics
Public support
Provider
Czech Science Foundation
Programme
Post-graduate (doctorate) grants
Call for proposals
Postdoktorandské granty 8 (SGA02008GA1PD)
Main participants
—
Contest type
VS - Public tender
Contract ID
201/08/P375
Alternative language
Project name in Czech
Formální verifikace: algoritmy, vlastnosti modelovacích formalismů a temporálních logik
Annotation in Czech
Procesy ověřování a garance kvality založené převážně na práci lidí nejsou vhodné pro vývoj dnešních rozsáhlých hardwarových a softwarových systémů. Perspektivním řešením je použití automatizovaných nástrojů pro formální verifikaci systémů. A právě výzkum v oblasti automatické formální verifikace je tématem předkládaného projektu. Navrhovatel se chce konkrétně zaměřit na tři oblasti: vlastnosti temporálních logik a využití těchto vlastností při konstrukci nových a vylepšení stávajících verifikačních algoritmů, vlastnosti formalismů pro popis nekonečně stavových systémů - jejich vyjadřovací síla a rozhodnutelnost základních verifikačních problémů pro odpovídající třídy nekonečně stavových systémů, progresivní směry ve verifikaci softwaru - zejména verifikace vlastností souvisejících s dynamicky alokovanou pamětí a aplikace verifikačních technik na běžné programovací jazyky. Výstupem projektu budou publikace v mezinárodních časopisech a na mezinárodních konferencích a
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 aim of the project was to achieve results in three areas: properties of temporal logics, properties of infinite-state systems, and progressive directions in software verification. In the first area, we proved that the LTL fragment with modalities eventually and always can be transformed to LTL formulae of a special form and we presented an algorithm for model checking of such formulae and wP
Solution timeline
Realization period - beginning
Jan 1, 2008
Realization period - end
Dec 31, 2010
Project status
U - Finished project
Latest support payment
Apr 16, 2010
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
CEP11-GA0-GP-U/04:3
Data delivery date
Mar 20, 2015
Finance
Total approved costs
435 thou. CZK
Public financial support
435 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK