Název: HyperLTL Model Checking
Překlad názvu: HyperLTL Model Checking
Autoři: Alexaj, Ondrej ; Strejček, Jan (oponent) ; Lengál, Ondřej (vedoucí práce)
Typ dokumentu: Bakalářské práce
Rok: 2024
Jazyk: eng
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [eng] [cze]
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.
Klíčová slova: formal verification; HyperLTL; language emptiness; language inclusion; model checking; on-the-fly; TGBA; formálna verifikácia; HyperLTL; jazyková inklúzia; model checking; prázdnosť jazyka; TGBA

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: https://hdl.handle.net/11012/246576

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


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 > Bakalářské práce