Original title: Rozšíření nástroje Plogchecker podporující strukturovaná data
Authors: Žalmánek, Matěj ; Rozsíval, Michal (referee) ; Smrčka, Aleš (advisor)
Document type: Master’s theses
Year: 2025
Language: cze
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [cze] [eng]
Tato práce se zaměřuje na problematiku ověřování parametrických vlastností programů nad záznamy jejich běhů. Konkrétně je pak v této práci rozebrán způsob, jakým je možné specifikovat konkrétní záznamy událostí a parametry těchto událostí včetně datových typů parametrů. Tato problematika je nejprve rozebrána teoreticky, včetně zmínění nejrůznějších formátů používaných pro zaznamenávání událostí. Následně jsou v této práci specifikovány požadavky na nástroj, který je výstupem této práce, a jehož hlavním cílem je extrahovat události a jejich parametry z různých formátů záznamů událostí. Posléze je v této práci popsán návrh tohoto nástroje a nakonec je tento nástroj implementován. Výstup tohoto nástroje je poté dále využíván externím programem, který monitoruje splnění či porušení vlastností využívajících tyto události. This thesis focuses on the problem of verifying parametric properties of programs based on logs of their execution. Specifically, this work discusses how to specify specific events and the parameters of these events, including the data types of the parameters. This issue is first discussed theoretically, including mention of the various formats used for event logging. Then, the requirements for the tool that is the output of this work are specified, whose main goal is to extract events and their parameters from various event record formats. Subsequently, the design of this tool is described and finally this tool is implemented. The output of this tool is then further used by an external program that monitors the fulfillment or violation of properties using these events.
Keywords: event definition; event extraction; event log formats; event parameter definition; parameter data type definition; parametric events; Parametric verification of programs at runtime; runtime monitoring; structured data types in events; definice datových typů parametrů; definice parametrů událostí; definice událostí; extrakce událostí; formáty záznamů událostí; monitorování běhů programu; Parametrická verifikace programů za běhu; parametrické události; strukturované datové typy v událostech

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

Permalink: http://www.nusl.cz/ntk/nusl-685285


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Master’s theses