Original title:
Ověřování temporálních vlastností konečných běhů programů
Translated title:
Checking of Temporal Properties of Finite Traces of Programs
Authors:
Sečkařová, Petra ; Češka, Milan (referee) ; Smrčka, Aleš (advisor) Document type: Master’s theses
Year:
2019
Language:
cze Publisher:
Vysoké učení technické v Brně. Fakulta informačních technologií Abstract:
[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.
Keywords:
linear temporal logic; run-time verification; temporal properties of programs; lineární temporální logika; temporální vlastnosti programů; verifikace programů za běhu
Institution: Brno University of Technology
(web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library. Original record: http://hdl.handle.net/11012/180387