Informace o projektu

Formální verifikace: algoritmy, vlastnosti modelovacích formalismů a temporálních logik

Logo poskytovatele
Kód projektu
GP201/08/P375
Období řešení
1/2008 - 12/2010
Investor / Programový rámec / typ projektu
Grantová agentura ČR
Fakulta / Pracoviště MU
Fakulta informatiky
Klíčová slova
formální verifikace, ověřování modelu, nekonečné systémy, temporální logiky

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.

Výsledky

Cílem projektu je základní výzkum ve vybraných oblastech automatické formální verifikace a publikace dosažených výsledků na mezinárodní úrovni.

Publikace

Počet publikací: 7


Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info