Detail projektu

Framework for the deductive analysis of embedded software

Období řešení: 1. 1. 2007 – 31. 12. 2008

Typ projektu: grant

Kód: GP201/07/P544

Agentura: Grantová agentura České republiky

Program: Postdoktorandské granty

Název česky
Rámec pro deduktivní analýzu softwarových aplikací vestavěných systémů
Typ
grant
Klíčová slova

Vestavěné systémy, Doménově specifické jazyky, Formální vývoj programů, Formální
specifikace, Formální verifikace

Abstrakt

Navrhovaný projekt představuje základní výzkum v problematice integrace
formálních metod a doménově specifikačních jazyků pro návrh vestavěných systémů.
Uvažované řešení bude založeno na definici formálního rámce disponujícího
deduktivním odvozovacím aparátem pro interpretaci a ověřování vlastností
doménově
specifických modelů. Formální rámec poskytne také prostředí pro integraci
automatických verifikačních method pro ověřování vlastností modelovaných systémů.
Cílem uvažovaného řešení je navržení doménově specifického modelovacího jazyka
s definovanou formální sémantiku a demonstrace možnosti kombinace deduktivní
a automatické verifikace pro ověřování takto specifikovaných systémů. Použití
formálního rámce přináší možnost ověření korektnosti extrakce specifikace
z doménového specifického modelovacího jazyka a transformace pro jednotlivé
verifikační nástroje.

Řešitelé
Ryšavý Ondřej, doc. Ing., Ph.D. (UIFS) – hlavní řešitel
Publikace

2009

2008

2007

Nahoru