Název: Verifikace za běhu systémů s vlastnostmi v MTL logice
Překlad názvu: Runtime Verification of Systems with MTL Properties
Autoři: Olšák, Ondřej ; Hruška, Martin (oponent) ; Smrčka, Aleš (vedoucí práce)
Typ dokumentu: Diplomové práce
Rok: 2021
Jazyk: cze
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [cze] [eng]
 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ů. This work is focused on the design of an algorithm for run-time verification over requirements given as formulas in metric temporal logic (MTL). Tree structure is used for verification of these requirements, which is similar to run of alternating timed automata from which the final algorithm is derivated. Designed algorithm is able to verify given MTL formulas over the runs of a program without a need to remember the whole program's trace. This allows to monitor a given program on potentially infinite runs.
Klíčová slova: metrická temporální logika; verifikace programů za běhu; metric temporal logic; run-time verification

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/201135

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-548539


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Vysoké učení technické v Brně
Vysokoškolské kvalifikační práce > Diplomové práce