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ý 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.

Grantor dc:publisher

Vysoké učení technické v Brně. Fakulta informačních technologií

Author dc:creator

• Alexaj, Ondrej

Advisor dc:contributor.advisor

• Lengál, Ondřej

• formálna verifikácia
• model checking
• HyperLTL
• TGBA
• jazyková inklúzia
• prázdnosť jazyka
• formal verification
• language inclusion
• on-the-fly
• language emptiness

Statement dc:rights

• Standardní licenční smlouva - přístup k plnému textu bez omezení

Language dc:language.iso

en

Dc Identifier Other

154514

OAI identifier oai:identifier

oai:dspace.vut.cz:11012/246576