API pro monitorování chování programů v kontextu nástroje DIVINE /
V této práci se zabýváme návrhem a implementací API pro monitorování programů verifikačním nástrojem DIVINE. Implementovaný monitor podporuje monitorování omega-regulárních vlastností programu pomocí zobecněných Buchiho automatů s akceptační podmínkou na hranách (TGBA). Naše rozhraní nabízí specifik...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2019
|
| Témata: | |
| On-line přístup: | http://is.muni.cz/th/ay7v9/ |
| Shrnutí: | V této práci se zabýváme návrhem a implementací API pro monitorování programů verifikačním nástrojem DIVINE. Implementovaný monitor podporuje monitorování omega-regulárních vlastností programu pomocí zobecněných Buchiho automatů s akceptační podmínkou na hranách (TGBA). Naše rozhraní nabízí specifikaci přímo ve formě TGBA nebo ve formě formulí lineární temporální logiky (LTL), a to prostřednicvím vlastního překladu formulí LTL na Buchiho automaty. V první kapitole uvádíme teoretický základ $\omega$-regulárních jazyků a ověřování modelů. V kapitole druhé představujeme architekturu nástroje DIVINE. V dalších dvou kapitolách popisujeme vlastní implementaci a v poslední, páté kapitole ukazujeme funkčnost implementovaného nástroje. In this work, we design and implement the API for program monitoring by the model checker DIVINE. The implemented monitor supports the monitoring of omega-regular properties using generalized transition based Buchi automata. Our implementation enables the specification of required properties in the form of TGBA or via a formula in linear temporal logic (LTL). We implement a custom translation engine of LTL formulas to Buchi automata. In the first chapter, we present a theoretical basis of $\omega$-regular languages and model validation. In Chapter Two we explore DIVINE architecture. In the next two chapters, we describe the implementation of the API, and in the last, fifth chapter we demonstrate the functionality of the implemented tool. |
|---|---|
| Popis jednotky: | Vedoucí práce: Jiří Barnat |
| Fyzický popis: | xv, 58 stran : ilustrace |