|
|
Překladač grafu toků dat do logiky bitových vektorů
Sušovský, Tomáš ; Lengál, Ondřej (oponent) ; Smrčka, Aleš (vedoucí práce)
Cílem této bakalářské práce je vytvořit a implementovat nástroj pro překlad modelů grafů toků dat do formátu SMT-LIB. Práce navazuje na projekt HADES výzkumné skupiny VeriFIT Fakulty informačních technologií Vysokého učení technického v Brně. V řešení bylo použito překladače vytvářejícího z původního grafu objektový model. Objektový model je možné převést do zápisu ve formátu SMT-LIB a přidat do něj aserce požadovaných vlastností systému. Pro ověřování vlastností závisejících na změnách systému je použita metoda rozbalování smyček s uživatelem zadanou hranicí maximálního počtu rozbalení. Možnosti vytvořeného nástoje jsou demonstrovány na sadě modelů grafů toků dat pokrývající všechny prvky vstupního jazyka VAM a jejich kombinace. Výsledek této práce představuje nové možnosti pro zpracování grafů toků dat ve formátu VAM a jejich verifikaci.
|
|
|
Generování testovacích vstupů podle stopy programu
Sušovský, Tomáš ; Malík, Viktor (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá návrhem a implementací nástroje pro automatické generování testových vstupů na základě určené stopy programu. Cílem je zjednodušit a zefektivnit proces vytváření testových sad splňující pokročilá kritéria pokrytí (používaných v kritických aplikacích psaných v nízko úrovňových jazycích C/C++ splňující přísná omezení). Na základě modelu programu nástroj zkoumá, jaké přesné podmínky musí nastat pro průchod programu dle zadané stopy. Pro nalezení vhodných hodnot využívá existující pokročilý nástroj řešič SMT specializovaný na řešení problému splnitelnosti. Nástroj využívá knihovny překladačového rámce LLVM pro práci s modelem programu a knihovnu Z3 pro práci s řešičem SMT. Výsledkem této práce je návrh architektury nástroje pro generování testových vstupů, který dokáže vygenerovat vstupy pro vykonání zadané stopy programu díky analýzování modelu programu, a implementace jeho prototypu.
|
|
|
Generování testovacích vstupů podle stopy programu
Sušovský, Tomáš ; Malík, Viktor (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá návrhem a implementací nástroje pro automatické generování testových vstupů na základě určené stopy programu. Cílem je zjednodušit a zefektivnit proces vytváření testových sad splňující pokročilá kritéria pokrytí (používaných v kritických aplikacích psaných v nízko úrovňových jazycích C/C++ splňující přísná omezení). Na základě modelu programu nástroj zkoumá, jaké přesné podmínky musí nastat pro průchod programu dle zadané stopy. Pro nalezení vhodných hodnot využívá existující pokročilý nástroj řešič SMT specializovaný na řešení problému splnitelnosti. Nástroj využívá knihovny překladačového rámce LLVM pro práci s modelem programu a knihovnu Z3 pro práci s řešičem SMT. Výsledkem této práce je návrh architektury nástroje pro generování testových vstupů, který dokáže vygenerovat vstupy pro vykonání zadané stopy programu díky analýzování modelu programu, a implementace jeho prototypu.
|
|
|
Překladač grafu toků dat do logiky bitových vektorů
Sušovský, Tomáš ; Lengál, Ondřej (oponent) ; Smrčka, Aleš (vedoucí práce)
Cílem této bakalářské práce je vytvořit a implementovat nástroj pro překlad modelů grafů toků dat do formátu SMT-LIB. Práce navazuje na projekt HADES výzkumné skupiny VeriFIT Fakulty informačních technologií Vysokého učení technického v Brně. V řešení bylo použito překladače vytvářejícího z původního grafu objektový model. Objektový model je možné převést do zápisu ve formátu SMT-LIB a přidat do něj aserce požadovaných vlastností systému. Pro ověřování vlastností závisejících na změnách systému je použita metoda rozbalování smyček s uživatelem zadanou hranicí maximálního počtu rozbalení. Možnosti vytvořeného nástoje jsou demonstrovány na sadě modelů grafů toků dat pokrývající všechny prvky vstupního jazyka VAM a jejich kombinace. Výsledek této práce představuje nové možnosti pro zpracování grafů toků dat ve formátu VAM a jejich verifikaci.
|
host ::
RSS.