Number of found documents: 1972
Published from to

Forenzní analýza anonymizačních principů kryptoměnových sítí
Hromada, Denis; Zavřel, Jan; Veselý, Vladimír
2024 - English
Při diskusích o kryptoměnách je častým tématem anonymita. Tato práce se věnuje stavebním blokům kryptoměny Bitcoin a jak na ni navazují kryptoměny jako Ethereum a Dash. Dále popisuje, jak a kde se v minulosti i přítomnosti v kryptoměnových sítích ztrácí soukromí a anonymita. Prvně se zaměřuje na anonymitu, respektive její nedostatky v samotném distribuovaném bloko-řetězu. Práce popisuje efekt znovu-využívání adres a shlukovací heuristiku založenou na společných vstupech transakce. Analyzuje je a popisuje nedokonalé aktuální řešení. Dále se práce zaměřuje na anonymitu mimo bloko-řetěz. Tedy na podpůrné služby, které jsou nedílnou součástí funkce kryptoměnových sítí jako jsou kryptoměnové peněženky. Práce diskutuje úschovu klíčů, různé druhy peněženek a jak komunikují s kryptoměnovými sítěmi. Následuje návrh modelu útočníka, jež je schopen odposlouchávat komunikaci uživatele kryptoměnové peněženky. Avšak nedokáže ji měnit. Jsou popsány vlastnosti, schopnosti a očekávaná úskalí takového útočníka. Poté práce věnuje pozornost třem kryptoměnovým peněženkám: Trezor Suite, Ledger Live a Electrum Wallet. Na těchto peněženkách demonstruje výše zmiňované vlastnosti kryptoměnových peněženek v praxi. Na základě všech těchto informací je navržena a implementována aplikace, jež je schopna napomoci uživateli určit, zda zachycený síťový provoz obsahuje komunikaci generovanou kryptoměnovou peněženkou. Nakonec je implementovaná aplikace podrobena testům. Výstupem těchto testů je, že za pomoci implementované aplikace je možné určit, jaká kryptoměnová peněženka byla použita. A to za předpokladu, že zachycený provoz obsahuje komunikaci, jež peněženky generují při jejich prvotním zapnutí. Následuje vyhodnocení práce a její další možné rozšíření. Anonymity is often a key talking point when presenting the concept of cryptocurrencies. This work first focuses on the building blocks of the Bitcoin cryptocurrency and its relationship cryptocurrencies with Ethereum and Dash. Then it looks at known past and present privacy pitfalls. First it focuses on on-chain anonymity and its shortcomings. Namely address reuse and common input clustering. The work then analyzes these shortcomings and their imperfect existing solutions. The work then shifts focus to off-chain anonymity. That is, the supporting services without which cryptocurrency networks could not function like cryptocurrency wallets. It takes a look at key storage, different types of cryptocurrency wallets and how they communicate with cryptocurrency networks. This is followed by the introduction of an attacker model. The attacker is an eavesdropper that can listen to, but cannot manipulate traffic between a cryptocurrency wallet user and a cryptocurrency node. Properties and capabilities of such an attacker follow. The work then takes a look at three cryptocurrency wallets: Trezor Suite, Ledger Live a Electrum Wallet on which it demonstrates the properties described above in practice. An application in designed and implemented based on all the learned knowledge. The goal of this application is to aid a user in determining, whether captured network traffic contains communication generated by a cryptocurrency wallet. Finally the implemented application is subjugated to testing. The result of these tests is, that it is indeed possible to use the application to determine if and which cryptocurrency wallet was used. If the captured traffic contains traffic generated on the initial launch of the cryptocurrency wallet. This is followed by a conclusion and proposition of future work. Keywords: Cryptocurrency; Bitcoin; Anonymity; Deanonymization; Computer Networks; Metadata; Eavesdropping; TOR; TLS/SSL; Kryptoměna; Bitcoin; Anonymita; Deanonymizace; Počítačové Sítě; Metadata; Odposlech; TOR; TLS/SSL Available in a digital repository NRGL
Forenzní analýza anonymizačních principů kryptoměnových sítí

Při diskusích o kryptoměnách je častým tématem anonymita. Tato práce se věnuje stavebním blokům kryptoměny Bitcoin a jak na ni navazují kryptoměny jako Ethereum a Dash. Dále popisuje, jak a kde se v ...

Hromada, Denis; Zavřel, Jan; Veselý, Vladimír
Vysoké učení technické v Brně, 2024

Analýza osteolytických nádorů páteře u pacientů s mnohočetným myelomem na datech z CT
Čurillová, Miriam; Mézl, Martin; Nohel, Michal
2024 - English
Táto bakalárska práca sa zameriava na analýzu osteolytických lézií u pacientov s mnohopočetným myelómom. Prvým krokom k dosiahnutiu nášho cieľa bolo štúdium tohto ochorenia, jeho diagnostických kritérií, možných komplikácií a dostupnej liečby. Praktická časť pozostávala z niekoľkých samostatných úloh. Štatistická analýza bola vykonaná na súbore údajov pozostávajúcom z CT skenov pacientov s diagnostikovaným mnohopočetným myelómom, ako aj osôb bez akejkoľvek patológie chrbtice. Po extrakcii a redukcii počtu príznakov sme dokončili analýzu získaných dát. Dospeli sme k záveru, že existujú príznaky, ktoré sa medzi týmito dvoma skupinami výrazne líšia. Po analýze celých tiel stavcov bola vykonaná analýza lézií na kontrolných snímkach, kde bol analyzovaný ich objem. This bachelor’s thesis focuses on analysis of osteolytic lesions in patients with multiple myeloma. The first step in achieving our goal was to research this disease, its diagnostic criteria, possible complications and available treatment. The practical part consisted of a few individual tasks. A statistical analysis was done on a dataset consisting of CT scans of patients with diagnosed multiple myeloma as well as individuals with no spinal pathologies. After extracting and reducing the number of features, we completed an analysis of obtained data. We came to a conclusion that there are features that vary significantly among the two groups. After analyzing the whole vertebral bodies, analysis of lesions in follow-up scans was completed, where their volume was analyzed. Keywords: multiple myeloma; computed tomography; osteolytic lesions; feature extraction; radiomics; statistical analysis; mnohopočetný myelóm; počítačová tomografia; osteolytické lézie; extrakcia príznakov; rádiomika; štatistická analýza Available in a digital repository NRGL
Analýza osteolytických nádorů páteře u pacientů s mnohočetným myelomem na datech z CT

Táto bakalárska práca sa zameriava na analýzu osteolytických lézií u pacientov s mnohopočetným myelómom. Prvým krokom k dosiahnutiu nášho cieľa bolo štúdium tohto ochorenia, jeho diagnostických ...

Čurillová, Miriam; Mézl, Martin; Nohel, Michal
Vysoké učení technické v Brně, 2024

Cognitive Game Battery: Assessing and Identifying Deficits in Memory, Attention, Problem-Solving, and Decision-Making Skills
Češka, Ondřej; Malik, Aamir Saeed; Hussain, Yasir
2024 - English
Cílem této práce je neinvazivní posouzení vybraných kognitivních domén (pozornost, paměť, rozhodování) pomocí nové mobilní aplikace vyvinuté za tímto účelem. Posuzování kognitivních nedostatků je důležité pro prevenci neurokognitivních poruch. Byly analyzovány existující posuzovací úlohy a na jejich základě byla navržena a úspěšně implementována kognitivní herní baterii sestávající ze 3 mobilních her. Aplikace je určena pro platformu Android a byla vyvinuta v Unity engine. Byl vytvořen systém pro sběr a uchovávání herních dat a jejich následné zhodnocení za pomoci cloudové dostupnosti. Jeho spolehlivost byla posouzena na základě vlastního sběru dat a poznatků existujících studií. Vyvinutá aplikace přináší jiný pohled na posuzování kognitivních nedostatků, porovnává uživatelem dosažené skóre s ostatními hráči a poskytuje mu detailní zpětnou vazbu. The goal of this work is the non-invasive assessment of selected cognitive domains (attention, memory, decision-making) using a new mobile application developed for this purpose. Assessment of cognitive deficits is important for the prevention of neurocognitive disorders. Existing assessment tasks were analyzed and based on them a cognitive game battery consisting of 3 mobile games was successfully designed and implemented. The application is made for the Android platform and was developed in the Unity engine. A system for collecting and storing game data and their subsequent evaluation with the help of cloud availability was created and evaluated using data collection and findings of existing studies. The presented application brings a different perspective to the assessment of cognitive deficits, compares the user's achieved score with other players, and provides them with detailed feedback. Keywords: cognitive domains; cognitive games; memory; attention; problem-solving; decision-making; brain; Android; Unity; battery; cloud; identifying deficits; kognitivní domény; kognitivní hry; paměť; pozornost; řešení problémů; rozhodování; mozek; Android; Unity; baterie; cloud; identifikace nedostatků Available in a digital repository NRGL
Cognitive Game Battery: Assessing and Identifying Deficits in Memory, Attention, Problem-Solving, and Decision-Making Skills

Cílem této práce je neinvazivní posouzení vybraných kognitivních domén (pozornost, paměť, rozhodování) pomocí nové mobilní aplikace vyvinuté za tímto účelem. Posuzování kognitivních nedostatků je ...

Češka, Ondřej; Malik, Aamir Saeed; Hussain, Yasir
Vysoké učení technické v Brně, 2024

Rozšiřitelná knihovna v jazyce Rust pro podporu vývoje vestavěných senzorických aplikací na platformě ESP32
Mikhailov, Kirill; Tinka, Jan; Šimek, Václav
2024 - English
Tato práce představuje rozšiřitelnou knihovnu jazyka Rust určenou pro vestavěné senzorové aplikace na platformě ESP32, která řeší potřebu zjednodušeného vývoje reálných vestavěných systémů v prostředí jazyka Rust na této platformě. Významným přínosem této práce je vývoj uživatelsky přívětivého rozhraní pro správu senzorů. Toto rozhraní umožňuje jednoduchou instalaci, aktivaci a monitorování senzorů, což vyhovuje aplikacím, jako jsou inteligentní domy a automatizace, aniž by vyžadovalo hluboké technické znalosti periferií. Architektura knihovny je pečlivě navržena s ohledem na modularitu a rozšiřitelnost a dodržuje zásady bezpečnosti a efektivity Rustu. Projekt je doprovázen rozsáhlou dokumentací a je zveřejněn na platformě GitHub pod open-source licencí Apache, doplněn unit-testy a příklady použití. V závěru práce je zhodnocena funkčnost knihovny a její případná budoucí vylepšení, která ukazují její praktičnost pro vývojáře vestavných systémů. This thesis introduces an extensible Rust library designed for embedded sensor applications on the ESP32 platform, addressing the need for simplified development of real embedded systems in a Rust language environment on this platform. A significant contribution of this thesis is the development of a user-friendly interface for sensor management. This interface allows for straightforward sensor installation, activation, and monitoring, catering to applications like smart homes and automation without requiring in-depth technical knowledge of peripherals. The library's architecture is carefully designed for modularity and extensibility, adhering to Rust's safety and efficiency principles. Accompanied by comprehensive documentation, the project is released on GitHub under an open-source Apache License, complete with unit tests and use-case examples. The thesis concludes with an evaluation of the library's functionality and potential future enhancements, demonstrating its practicality for embedded system developers. Keywords: Rust; ESP32; IoT; SoC; embedded systems; embedded applications; user-friendly development; sensors; microcontroller; embedded Rust; Rust library; Rust crate; Smart Home; MQTT; Rust; ESP32; IoT; SoC; vestavěné systémy; vestavěné aplikace; uživatelsky přívětivý vývoj; senzory; mikrokontrolér; vestavěný Rust; knihovna Rust; Rust crate; chytrá domacnost; MQTT Available in a digital repository NRGL
Rozšiřitelná knihovna v jazyce Rust pro podporu vývoje vestavěných senzorických aplikací na platformě ESP32

Tato práce představuje rozšiřitelnou knihovnu jazyka Rust určenou pro vestavěné senzorové aplikace na platformě ESP32, která řeší potřebu zjednodušeného vývoje reálných vestavěných systémů v prostředí ...

Mikhailov, Kirill; Tinka, Jan; Šimek, Václav
Vysoké učení technické v Brně, 2024

Vestavné bezdrátové monitorování a řízení fotovoltaického systému
Kovács, Attila; Lojda, Jakub; Strnadel, Josef
2024 - English
Na trhu s obnoviteľnými zdrojmi energie je veľká konkurencia. Najčastejšie sa v domácnostiach využívajú fotovoltaické systémy. Avšak aj napriek ich častému využitiu v domácnostiach im bežný používateľ nerozumie a ponecháva niektoré záležitosti spoločnosti, ktorá vykonáva inštaláciu. Táto bakalárska práca najprv čitateľa oboznámi s rôznymi komponentami, z ktorých fotovoltaický systém pozostáva. Neskôr popisujeme vytvorenie prototypu. Tento prototyp je univerzálnym riešením pre monitorovanie a riadenie výkonu akéhokoľvek fotovoltaického systému. Dosiahneme to meraním výkonu každého fotovoltaického panelu, s týmito údajmi môžeme diagnostikovať chybný panel a porovnaním celkového výkonu fotovoltaických panelov s výstupom meniča včas zistiť poruchu meniča. Pre prístup k údajom bola vytvorená jednoduchá webová aplikácia. Súčasný prototyp je schopný merať prechádzajúcu energiu a prepínať výstupnú energiu. V záverečnej časti práce popisujeme súčasné nedostatky prototypov a možné spôsoby ich zmiernenia, venujeme sa aj problémom, ktoré vznikli pri tvorbe prototypu a aj ich riešeniam. The renewable energy sources market is a highly competitive market. For household use photovoltaic systems have the highest adoption rate. Even with its high adoption rate the general adopter doesn't really understand it and leaves some things to the company which does the installation. This bachelor thesis first introduces the reader to the various components a photovoltaic system consists of. Later the creation of a prototype is described. This prototype is a universal solution for monitoring and controlling the output of any photovoltaic system. This is accomplished by measuring the power output of each photovoltaic panel with this data it is possible to diagnose a faulty panel and by comparing the complete output of the photovoltaic panels with the inverter's output a failing inverter can also be early detected. For accessing the data a simple web application was created. The current prototype is able to measure the power going through it, It's able to toggle the output power. The final part of the thesis describes the current prototypes shortcomings and possible ways on how to mitigate them it also mentions problems which arose during the creation of the prototype and how they were solved. Keywords: wireless monitoring and control; photovoltaic systems; Internet of Things; LoRa; LoRaWAN; embedded systems; bezdrôtové monitorovanie a ovládanie; fotovoltaické systémy; Internet of Things; LoRa; LoRaWAN; vstavané systémy Available in a digital repository NRGL
Vestavné bezdrátové monitorování a řízení fotovoltaického systému

Na trhu s obnoviteľnými zdrojmi energie je veľká konkurencia. Najčastejšie sa v domácnostiach využívajú fotovoltaické systémy. Avšak aj napriek ich častému využitiu v domácnostiach im bežný používateľ ...

Kovács, Attila; Lojda, Jakub; Strnadel, Josef
Vysoké učení technické v Brně, 2024

Formální modely pro práci s datovými jazyky
Vašák, Jan; Havlena, Vojtěch; Lengál, Ondřej
2024 - English
Datová slova jsou běžně používaná pro formální práci se slovy nad nekonečnými abecedami. V praxi může nekonečná abeceda modelovat skutečně nekonečnou množinu, např. celá čísla nebo množinu řeťezců, nebo velkou konečnou množinu, jako např. znaky sady Unicode. Tato práce se nejprve věnuje teoretickým vlastnostem registrově množinových automatů. Registrově množinové automaty jsou modelem nad datovými slovy, který lze použít pro determinizaci velké třídy registrových automatů (toto např. umožňuje deterministickou automatovou reprezentaci třídy regulárních výrazů se zpětnými odkazy). Dále jsme rozšířili streaming data string převaděče, model určený pro modelování třídy programů pro zpracování lineárních seznamů, o množinové registry. Toto rozšíření umožňuje např. modelovat program, který odstraní duplicitní hodnoty z lineárního seznamu, což není možné modelovat základními streaming data string převaděči. Ukážeme, že problém funkční ekvivalence je pro toto rozšíření rozhodnutelný. Také byl naimplementován prototyp regex matcheru založený na registrově množinových automatech. Ukážeme, že prototyp si vede dobře pod ReDoS (regular expression denial of service) útoky, které jsou efektivní vůči regex matcherům používaným v praxi. Data words are a common way to formally work with words over infinite alphabets. In practice, an infinite alphabet can represent an actually infinite set, such as the integers or a set of strings, or a large finite set, such as the Unicode symbols. We explore some theoretical properties of register set automata, a data word model that, crucially, can be used as a means to determinise a large class of register automata (this allows, e.g., for a deterministic automata representation of a class of regexes with back-references). We also extend streaming data string transducers, a model designed to represent a class of list-processing programs, with set-registers. This extension can, for example, represent a program that removes duplicates from a list, which is not representable using the base model. We then show that this extension’s functional equivalence problem is decidable. Lastly, a prototype regex matcher based on register set automata was implemented, and we experimentally show that it performs well under regular expression denial of service attacks that can cripple other matchers used in practice. Keywords: data words; register set automata; streaming data string transducers; regular expressions with back-references; datová slova; registrově množinové automaty; streaming data string převodníky; regulární výrazy se zpětnými odkazy Available in a digital repository NRGL
Formální modely pro práci s datovými jazyky

Datová slova jsou běžně používaná pro formální práci se slovy nad nekonečnými abecedami. V praxi může nekonečná abeceda modelovat skutečně nekonečnou množinu, např. celá čísla nebo množinu řeťezců, ...

Vašák, Jan; Havlena, Vojtěch; Lengál, Ondřej
Vysoké učení technické v Brně, 2024

Implementace MitM sondy na platforme RPi
Nekula, Štěpán; Holop, Patrik; Tamaškovič, Marek
2024 - English
Cílem této práce je implementovat síťovou sondu pro monitorování šifrovaného síťového provozu. Navržená síťová sonda využívá útoku Man-in-the-Middle (MitM) pro zachycení a získání přístupu k šifrovaným datům. Základem sondy je platforma Raspberry Pi, na které běží software SSLproxy, jež zprostředkovává zachycování a dešifrování dat ze sítě. Tyto data jsou následně prohledávány pomocí detekčního systému hrozeb Suricata. Výkon sondy byl testován detekcí simulovaných útoků, jako je šíření nebezpečných souborů a síťové útoky. Tato práce poskytuje nástroj pro další výzkum v oblasti monitorování šifrovaných sítí a detekci hrozeb v šifrované komunikaci. This work presents a network probe that uses a Man-in-the-Middle (MitM) attack to monitor encrypted network traffic. The proposed probe is based on a Raspberry Pi platform and uses SSLproxy software for intercepting encrypted communication which are then scanned using Suricata intrusion detection system. Probe's performance is tested by detecting various types of simulated threats, such as malware spread and network attacks. This work provides a valuable tool for further studies of encrypted network surveillance by effectively detecting malicious activities within encrypted communications. Keywords: Raspberry Pi; RPI; MITM; probe; proxy; network analysis; network monitoring; realtime threat detection; encrypted communication monitoring; Suricata; SSLproxy; intrusion detection; intrusion detection system; Raspberry Pi; RPI; Man in the middle; MITM; síťovou sonda; analýza sítě; monitorování sítě; detekce hrozeb v reálném čase; monitorování šifrované komunikace; Suricata; SSLproxy; systém detekce hrozeb Available in a digital repository NRGL
Implementace MitM sondy na platforme RPi

Cílem této práce je implementovat síťovou sondu pro monitorování šifrovaného síťového provozu. Navržená síťová sonda využívá útoku Man-in-the-Middle (MitM) pro zachycení a získání přístupu k ...

Nekula, Štěpán; Holop, Patrik; Tamaškovič, Marek
Vysoké učení technické v Brně, 2024

React komponenty pro webový editor titulkování a anotací audia
Dugovič, Jakub; Herout, Adam; Szőke, Igor
2024 - English
Cieľom tejto práci je implementovať modulárne užívateľské rozhranie na prepis zvukových nahrávok a ich anotáciu. Rozširuje dotrajšiu prácu s cieľom umožniť a zjednodušiť prácu s hodiny dlhými nahrávkami rozhovorov. Riešenie je implementované v TypeScripte pomocou Reactu a ďalších knižníc z reactového ekosystému. Aplikujúc princípy naštudované z literatúry, vyhýbajúc sa chybám identifikovaným počas prieskumu obdobnej platformy a overujúc užívateľské rozhranie počas vývoja pomocou kvalitatívneho testovania, vyvýjané rozhranie sa usiluje dosiahnuť vysokú mieru dobrej užívateľskej skúsenosti. This thesis aims to implement modular user interface for audio transcription and annotation. It expands upon existing work in order to enable and improve working with hours-long conversation recordings. The solution is implemented in TypeScript using React and additional libraries from the React ecosystem. Applying principles from the studied literature, avoiding issues identified during the research a similar platform, and verifying the interface throughout the development using qualitative testing, the interface strives to achieve high degree of good user experience. Keywords: React; Redux; web app; audio player; audio transcripion; phonetic transcription; Wavesurfer; graphical user interface; GUI; UI; usability; user experience; UX; experience desgin; XD; web design; frontend; qualitative testing; interface testing; SUS; long audio files; long recordings; entity grouping; metadata; entity tagging; React; Redux; webová aplikácia; audio prehrávač; prepis audia; fonetický prepis; Wavesurfer; grafické užívateľské rozhranie; GUI; UI; použiteľnosť; užívateľská skúsenosť; UX; dizajn užívateľskej skúsenosti; XD; webový dizajn; frontend; kvalitatívne testovanie; testovanie užívateľských rozhraní; SUS; dlhé zvukové súbory; dlhé nahrávky; zoskupovanie entít; metadáta; značkovanie entít Available in a digital repository NRGL
React komponenty pro webový editor titulkování a anotací audia

Cieľom tejto práci je implementovať modulárne užívateľské rozhranie na prepis zvukových nahrávok a ich anotáciu. Rozširuje dotrajšiu prácu s cieľom umožniť a zjednodušiť prácu s hodiny dlhými ...

Dugovič, Jakub; Herout, Adam; Szőke, Igor
Vysoké učení technické v Brně, 2024

Překladové automaty aplikované v umění
Khrystsiuk, Dziyana; Klembara, Radovan; Meduna, Alexandr
2024 - English
Cílem této práce je vytvořit nástroj založený na překladovém automatu, který podporuje umělce poskytnutím strukturovaného přístupu k výtvarnému umění. Výsledkem této práce je webová aplikace dostupná online, která byla vyvinuta s využitím frameworku React. Nástroj implementuje překladové pravidla pomocí celulárního automatu a poskytuje umělcům různé kreativní transformace, které jim umožňují představit si potenciální změny jejich stávajících děl a objevit nové možnosti postprodukčních úprav obrazů. The goal of this work is to create a tool based on a translation automaton that supports artists by offering a structured approach to visual art. As a result of this work, a web based application, now accessible online, was developed with the use of React framework. The tool implements translation rules using cellular automaton, providing artists with variety of creative transformations that enable them to envision potential changes in their existing work and discover new possibilities for post-production image editing. Keywords: cellular automaton; translation automaton; abstract art; image editing; artistic application; celulární automat; translační automat; abstraktní umění; editace obrázků; umělecká aplikace Available in a digital repository NRGL
Překladové automaty aplikované v umění

Cílem této práce je vytvořit nástroj založený na překladovém automatu, který podporuje umělce poskytnutím strukturovaného přístupu k výtvarnému umění. Výsledkem této práce je webová aplikace dostupná ...

Khrystsiuk, Dziyana; Klembara, Radovan; Meduna, Alexandr
Vysoké učení technické v Brně, 2024

HyperLTL Model Checking
Alexaj, Ondrej; Strejček, Jan; Lengál, Ondřej
2024 - English
HyperLTL model checking je technika pre overenie systému voči danej hypervlastnosti vyjadrenej logikou HyperLTL, ktorá dokáže prepojiť viaceré spustenia systému. Hoci bol vytvorený algoritmický prístup založený na automatoch, spolieha sa na štandardné operácie -automatov. Cieľom tejto práce je prekonať kompletný state-of-the-art HyperLTL model checker AutoHyper využitím efektívnejších čiastkových operácií nad automatmi, najmä komplementácie a inklúzie. Implementácia HyperLTL model checkingu v modulárne založenom nástroji pre komplementáciu, Kofola, viedla k výraznému zvýšeniu výkonu v porovnaní s referenčným nástrojom. Napokon, náš prístup ku kontrole jazykovej inklúzie vykazuje výrazné zmenšenie generovaného stavového priestoru. Keďže ide o bežne používanú operáciu nad automatmi, náš prístup by potenciálne mohol prispieť k pokroku aj v iných oblastiach verifikácie. HyperLTL model checking is an approach to verifying a system against a given hyperproperty, which is able to relate multiple executions of a system. The algorithmic approach based on automata which relies on standard -automata operations is well established. The aim of this work is to outperform the complete state-of-the-art HyperLTL model checker AutoHyper by employing more efficient partial automata operations, in particular complementation and inclusion. The implementation of HyperLTL model checking in a novel modular-based complementation tool Kofola resulted in a significant enhancement in performance compared to the reference tool. Finally, our approach to language inclusion checking shows a notable improvement in terms of the generated state space. As a commonly used automata operation, it could potentially contribute to the advancement of other areas of verification. Keywords: formal verification; model checking; HyperLTL; TGBA; language inclusion; on-the-fly; language emptiness; formálna verifikácia; model checking; HyperLTL; TGBA; jazyková inklúzia; prázdnosť jazyka Available in a digital repository NRGL
HyperLTL Model Checking

HyperLTL model checking je technika pre overenie systému voči danej hypervlastnosti vyjadrenej logikou HyperLTL, ktorá dokáže prepojiť viaceré spustenia systému. Hoci bol vytvorený algoritmický ...

Alexaj, Ondrej; Strejček, Jan; Lengál, Ondřej
Vysoké učení technické v Brně, 2024

About project

NRGL provides central access to information on grey literature produced in the Czech Republic in the fields of science, research and education. You can find more information about grey literature and NRGL at service web

Send your suggestions and comments to nusl@techlib.cz

Provider

http://www.techlib.cz

Facebook

Other bases