Název:
Ověřování temporálních vlastností konečných běhů programů
Překlad názvu:
Checking of Temporal Properties of Finite Traces of Programs
Autoři:
Sečkařová, Petra ; Češka, Milan (oponent) ; Smrčka, Aleš (vedoucí práce) Typ dokumentu: Diplomové práce
Rok:
2019
Jazyk:
cze
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [cze][eng]
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.
Correct behavior of programs can be defined by their temporal properties. One of the options for formal specification of such properties is linear temporal logic - LTL . This master's thesis describes design and implementation of a tool for automatic checking of temporal properties of programs, that are specified using Past-Time LTL formulae. The trace of a given program is analyzed in run-time and any violation of given formulae is reported in details to help to find the code location with a root cause of the bug.
Klíčová slova:
lineární temporální logika; temporální vlastnosti programů; verifikace programů za běhu; linear temporal logic; run-time verification; temporal properties of programs
Instituce: Vysoké učení technické v Brně
(web)
Informace o dostupnosti dokumentu:
Plný text je dostupný v Digitální knihovně VUT. Původní záznam: http://hdl.handle.net/11012/180387