Informace o projektu
Formální verifikace: algoritmy, vlastnosti modelovacích formalismů a temporálních logik
| Kód projektu | GP201/08/P375 CEP CORDIS MU WEB INET MU |
|---|---|
| Doba řešení | 01.01.2008–31.12.2010 |
| Stav | ukončený |
| Investor | Grantová agentura ČR |
| Program | Postdoktorské projekty |
| Řešitel za FI |
Anotace
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ů. 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 workshopech.
- 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 workshopech.