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/ |
| LEADER | 04975ctm a22008057i 4500 | ||
|---|---|---|---|
| 001 | MUB01006436744 | ||
| 003 | CZ BrMU | ||
| 005 | 20190320110807.0 | ||
| 008 | 190207s2019 xr ||||| |||||||||||eng d | ||
| STA | |a POSLANO DO SKCR |b 2019-06-17 | ||
| 035 | |a (ISMU-VSKP)296188 | ||
| 040 | |a BOD114 |b cze |d BOD004 |e rda | ||
| 072 | 7 | |a 519.1/.8 |x Kombinatorika. Teorie grafů. Matematická statistika. Operační výzkum. Matematické modelování |2 Konspekt |9 13 | |
| 080 | |a 519.713 |2 MRF | ||
| 080 | |a 519.766 |2 MRF | ||
| 080 | |a (043)378.2 |2 MRF | ||
| 100 | 1 | |a Kučera, Tadeáš |% UČO 423907 |* [absolvent FI MU] |4 dis | |
| 242 | 1 | 0 | |a API for monitoring of program behaviour in DIVINE model checker |y eng |
| 245 | 1 | 0 | |a API pro monitorování chování programů v kontextu nástroje DIVINE / |c Tadeáš Kučera |
| 264 | 0 | |c 2019 | |
| 300 | |a xv, 58 stran : |b ilustrace | ||
| 336 | |a text |b txt |2 rdacontent | ||
| 337 | |a bez média |b n |2 rdamedia | ||
| 338 | |a svazek |b nc |2 rdacarrier | ||
| 500 | |a Vedoucí práce: Jiří Barnat | ||
| 502 | |a Diplomová práce (Mgr.)--Masarykova univerzita, Fakulta informatiky, 2019 | ||
| 520 | 2 | |a 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. |% cze | |
| 520 | 2 | 9 | |a 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. |9 eng |
| 650 | 0 | 7 | |a regulární jazyky |7 ph237421 |2 czenas |
| 650 | 0 | 7 | |a teorie automatů |7 ph126547 |2 czenas |
| 650 | 0 | 9 | |a automata theory |2 eczenas |
| 650 | 0 | 9 | |a regular languages |2 eczenas |
| 655 | 7 | |a diplomové práce |7 fd132022 |2 czenas | |
| 655 | 9 | |a master's theses |2 eczenas | |
| 658 | |a Matematika |b Matematika s informatikou |c PřF N-MA MINF (MINF) |2 CZ-BrMU | ||
| 700 | 1 | |a Barnat, Jiří, |d 1977- |7 mub2010575337 |% UČO 3496 |4 ths | |
| 710 | 2 | |a Masarykova univerzita. |b Katedra teorie programování |4 dgg | |
| 710 | 2 | |a Masarykova univerzita. |b Ústav matematiky a statistiky |7 kn20091211007 |4 dgg | |
| 856 | 4 | 1 | |u http://is.muni.cz/th/ay7v9/ |
| CAT | |c 20190207 |l MUB01 |h 0420 | ||
| CAT | |a POSPEL |b 02 |c 20190213 |l MUB01 |h 0800 | ||
| CAT | |a POSPEL |b 02 |c 20190213 |l MUB01 |h 0801 | ||
| CAT | |a HANAV |b 02 |c 20190304 |l MUB01 |h 1653 | ||
| CAT | |a TRENCANSKA |b 02 |c 20190308 |l MUB01 |h 1158 | ||
| CAT | |a TRENCANSKA |b 02 |c 20190308 |l MUB01 |h 1158 | ||
| CAT | |a HANAV |b 02 |c 20190309 |l MUB01 |h 2245 | ||
| CAT | |a JANA |b 02 |c 20190320 |l MUB01 |h 1108 | ||
| CAT | |c 20190617 |l MUB01 |h 1027 | ||
| CAT | |a POSPEL |b 02 |c 20190924 |l MUB01 |h 0745 | ||
| CAT | |a POSPEL |b 02 |c 20200510 |l MUB01 |h 2306 | ||
| CAT | |a POSPEL |b 02 |c 20201212 |l MUB01 |h 2150 | ||
| CAT | |a POSPEL |b 02 |c 20210122 |l MUB01 |h 0054 | ||
| CAT | |a POSPEL |b 02 |c 20210322 |l MUB01 |h 1142 | ||
| CAT | |a POSPEL |b 02 |c 20210327 |l MUB01 |h 0026 | ||
| CAT | |c 20210614 |l MUB01 |h 1032 | ||
| CAT | |c 20210614 |l MUB01 |h 2018 | ||
| CAT | |a BATCH |b 00 |c 20210724 |l MUB01 |h 1308 | ||
| CAT | |a POSPEL |b 02 |c 20210912 |l MUB01 |h 2336 | ||
| CAT | |a POSPEL |b 02 |c 20211010 |l MUB01 |h 2218 | ||
| CAT | |a HANAV |b 02 |c 20211115 |l MUB01 |h 1631 | ||
| CAT | |a POSPEL |b 02 |c 20220629 |l MUB01 |h 0104 | ||
| CAT | |a POSPEL |b 02 |c 20221019 |l MUB01 |h 2326 | ||
| CAT | |a POSPEL |b 02 |c 20221101 |l MUB01 |h 0840 | ||
| CAT | |a POSPEL |b 02 |c 20230629 |l MUB01 |h 0037 | ||
| CAT | |a POSPEL |b 02 |c 20240226 |l MUB01 |h 1300 | ||
| CAT | |a POSPEL |b 02 |c 20240405 |l MUB01 |h 2124 | ||
| LOW | |a POSLANO DO SKCR |b 2019-06-17 | ||
| 994 | - | 1 | |l MUB01 |l MUB01 |m VYSPR |1 PRIF |a Přírodovědecká fakulta |2 PRVMA |b ÚK volný výběr - M |3 K-M-2019-KUČE |5 3145375445 |8 20190308 |f 70 |f Prezenční |r 20190308 |s dar |
| AVA | |a SCI50 |b PRIF |c ÚK volný výběr - M |d K-M-2019-KUČE |e available |t K dispozici |f 1 |g 0 |h N |i 0 |j PRVMA | ||