|
|
Ověřování temporálních vlastností konečných běhů programů
Sečkařová, Petra ; Češka, Milan (oponent) ; Smrčka, Aleš (vedoucí práce)
Temporální vlastnosti programů jsou používány ke specifikaci korektního průběhu jejich vykonávání. Jedním z nejčastějších způsobů formálního popisu těchto vlastností je lineární temporální logika - LTL , případně její varianty. Tato práce se zabývá návrhem a implementací nástroje pro automatizované ověřování temporálních vlastností běhů programů specifikovaných pomocí LTL minulého času (past-time LTL). Výsledný program na základě dané specifikace vygeneruje statickou knihovnu, která dokáže spolehlivě ověřit, zda jsou její formule v každém okamžiku běhu kontrolovaného programu splněny, a případné neočekávané nebo nesprávné chování hlásí společně s podrobnou zprávou o okolnostech tohoto chybového stavu, která má napomáhat k nalezení chyby v konkrétním místě kódu.
|
|
|
Verifikace za běhu systémů s vlastnostmi v MTL logice
Olšák, Ondřej ; Hruška, Martin (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá návrhem algoritmu pro ověřování splnitelnosti omezení programu zapsaných pomocí metrické temporální logiky (MTL), kdy sledování splnitelnosti těchto formulí probíhá za běhu daného programu. K ověřování těchto vlastností využívá navržený algoritmus stromové struktury, která je podobná chování alternujícího časového automatu, ze kterého je výsledný postup sledování programu odvozen. Navržený algoritmus, je schopen za běhu daného programu ověřovat jeho vlastnosti vůči definovaným MTL formulím a to bez potřeby pamatovat si stavy, ve kterých se sledovaný program nacházel. To umožňuje ověřit vlastnosti daného programu u potenciálně nekonečných běhů.
|
|
|
Verifikace za běhu systémů s vlastnostmi v MTL logice
Olšák, Ondřej ; Hruška, Martin (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá návrhem algoritmu pro ověřování splnitelnosti omezení programu zapsaných pomocí metrické temporální logiky (MTL), kdy sledování splnitelnosti těchto formulí probíhá za běhu daného programu. K ověřování těchto vlastností využívá navržený algoritmus stromové struktury, která je podobná chování alternujícího časového automatu, ze kterého je výsledný postup sledování programu odvozen. Navržený algoritmus, je schopen za běhu daného programu ověřovat jeho vlastnosti vůči definovaným MTL formulím a to bez potřeby pamatovat si stavy, ve kterých se sledovaný program nacházel. To umožňuje ověřit vlastnosti daného programu u potenciálně nekonečných běhů.
|
|
|
Ověřování temporálních vlastností konečných běhů programů
Sečkařová, Petra ; Češka, Milan (oponent) ; Smrčka, Aleš (vedoucí práce)
Temporální vlastnosti programů jsou používány ke specifikaci korektního průběhu jejich vykonávání. Jedním z nejčastějších způsobů formálního popisu těchto vlastností je lineární temporální logika - LTL , případně její varianty. Tato práce se zabývá návrhem a implementací nástroje pro automatizované ověřování temporálních vlastností běhů programů specifikovaných pomocí LTL minulého času (past-time LTL). Výsledný program na základě dané specifikace vygeneruje statickou knihovnu, která dokáže spolehlivě ověřit, zda jsou její formule v každém okamžiku běhu kontrolovaného programu splněny, a případné neočekávané nebo nesprávné chování hlásí společně s podrobnou zprávou o okolnostech tohoto chybového stavu, která má napomáhat k nalezení chyby v konkrétním místě kódu.
|
host ::
RSS.