Model checking concurrent software using automated deduction of object ownership patterns
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-P180
Alternative language
Project name in Czech
Model checking paralelního software s využitím automatické dedukce object ownership vzorů
Annotation in Czech
Verifikace vícevláknového softwaru model checkingem je těžký problém, zejména kvůli explozi stavového prostoru. Správnost takového softwaru závisí na dodržení jistých synchronizačních pravidel navržených vývojáři, ale nezachycených v samotném kódu programu. Taková pravidla často popisují object ownership, který přiřazuje objektům pravidla přístupu k nim ve vícevláknovém prostředí (např. datová struktura je vlastněna zámkem). Na jedné straně by znalost této informace mohla být extrémně užitečná při verifikaci vícevláknového softwaru. Na straně druhé se mimo velmi specifické případy nedá realisticky očekávat, že vývojáři tuto informaci zachytí ve formě vhodné k automatickému zpracování. V tomto projektu navrhneme metodu pro automatickou extrakci object ownership vzorů. Dále rozšíříme stávající techniky on-the-fly partial-order-reduction o využití této informace k efektivnějšímu ořezání stavového prostoru během následného model checkingu. Součástí projektu je i prototypová implementace.
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
O - Nesplněno zadání, smlouva však byla dodržena
Project results evaluation
This three-year project finished after the first year due to the end of the work contract of the grant holder. It dealt with extending the techniques used in verification of concurrent software. A paper leading to the suggested research was published bythe holder with foreign co-authors at the prestigious conference CAV (2012). Further publications show continuing of his research at top level.
Solution timeline
Realization period - beginning
Jan 1, 2012
Realization period - end
Dec 31, 2013
Project status
S - Stopped (prematurely terminated) multi-year project
Latest support payment
Mar 30, 2013
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
672 thou. CZK
Public financial support
672 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK