|
|
Testování platformy JBoss Drools založené na modelu
Široký, Petr ; Holík, Lukáš (oponent) ; Letko, Zdeněk (vedoucí práce)
Technika testování založeného na modelu (MBT) využívá model chování systému k automatickému generování sady testů, čímž snižuje nákladnost testování oproti konvenčnímu manuálnímu vývoji a udržbě testů. Tato práce se zaměřuje na využití zvoleného MBT nástroje OSMO při testování reálného softwarového produktu. Konkrétně se o jedná kompilátor podnikových pravidel využívaný v systému Drools, který je spoluvyvíjený společností Red Hat. V práci je popsán způsob zavedení MBT přístupu s ohledem na jeho dobré přijetí komunitou vývojářů, dále pak vytvoření modelu možných vstupů testovaného kompilátoru a zhodnocení vytvořené testovací sady. Využití MBT přístupu vedlo k odhalení pěti nahlášených a tří potencionálních a dosud nehlášených chyb v testovaném kódu. Práce na příkladu shrnuje hlavní přednosti i praktické nedostatky využití MBT technik v praxi.
|
|
|
Verifikovaná knihovna datových struktur
Rychnovský, Jan ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Tato bakalářská práce se zabývá metodikou psaní verifikovaných programů pomocí nástroje VCC. Zmíněná metodika je založena na principu doplnění kódu programu o anotace, jež poskytují specifikaci požadované funkcionality. Nástroj VCC pak prostřednictvím formálních metod určí zda zdrojový kód splňuje danou specifikaci či ne. V první části práce je popsána formální verifikace a zmíněny tři základní přístupy k ní. Následně jsou popsány problémy splnitelnosti výrokových formulí (SAT) a splnitelnosti formulí v teoriích predikátové logiky (SMT). Práce se dále věnuje popisu verifikačního nástroje VCC, jeho funkčnosti, metodice, syntaxi a sémantice příkazů jeho anotačního jazyka BoogiePL. Druhá část textu je zaměřena na popis návrhu a implementace verifikované knihovny datových struktur obsahující jednosměrný, dvousměrný a kruhový seznam, binární vyhledávací strom a Treiberův zásobník. Závěr práce diskutuje získané poznatky o programovací metodice založené na psaní verifikovaného kódu.
|
|
|
Slučování úloh s nekolizními požadavky pro systém Beaker
Kovařík, Michal ; Fiedor, Jan (oponent) ; Holík, Lukáš (vedoucí práce)
Obsahem práce je návrh formátu pro zápis parametrů a požadavků jednotlivých úloh určených pro systém Beaker a návrh a implementace programu, který na základě vyloučení možných kolizních požadavků sloučí úlohy definované na vstupu do souboru úloh, jež je možné spouštět společně. Výstupem je formát spustitelný v systému Beaker. Práce popisuje instalaci operačního systému, na kterém definuje kolizní požadavky. V práci je popsán způsob zadávání a spouštění úloh v systému Beaker. V závěru je provedeno testování vytvořeného programu.
|
|
|
Praktická efektivita kontejnerů
Halámka, Jan ; Letko, Zdeněk (oponent) ; Holík, Lukáš (vedoucí práce)
Práce se zabývá teoretickým a praktickým porovnáním následujících kontejnerů: vector, deque, list, hash table, avl-tree, red black tree, splay tree, sg-tree, treap, B-tree, binomiální halda, fibonacciho halda, rope, skiplist při práci s množinami. U každé z nich jsou v práci zmíněny jejich asymptotické třídy složitosti, amortizované složitosti a složitosti v průměrném případě. U každé struktury je rovněž zmíněn způsob jakým se dá implementovat a jak vypadá v paměti počítače. Pro porovnání byla v práci rovněž navržena a implementována sada testů jejíž výsledky jsou k dispozici.
|
|
|
Knihovna pro binární rozhodovací diagramy
Janků, Petr ; Hrubý, Martin (oponent) ; Holík, Lukáš (vedoucí práce)
Efektivní manipulace Booleovských funkcí je důležitou součástí mnoha počítačových návrhů. Jako datová struktura pro reprezentaci a manipulaci s Booleovskými funkcemi se běžně používají binární rozhodovací diagramy. Tyto diagramy se běžně používají v mnoha odvětvích, jako je například ověřování modelů, verifikace systému, návrh obvodů apod. V této práci jsou popsány tyto diagramy a jsou zde uvedeny i jejich modifikace. Dále jsou v této práci uvedeny a popsány techniky pro efektivní manipulaci a reprezentaci binárních rozhodovacích diagramů. Mimoto tato práce popisuje návrh a implementaci knihovny, která bude s těmito diagramy pracovat. Dále je diskutována potenciální aplikace vyvinuté knihovny v knihovně VATA pro manipulaci se stromovými automaty. Na závěr je tato knihovna porovnána s dobře známou a silně optimalizovanou knihovnou CUDD, která je volně dostupná a s knihovnou CacBDD. Výsledky experimentů ukázaly, že navrhovaná knihovna je poměrně blízká CUDD a CacBDD (dosahuje srovnatelného a většinou i lehce lepšího výkonu).
|
|
|
Optimalizace testování pomocí algoritmů prohledávání prostoru
Starigazda, Michal ; Holík, Lukáš (oponent) ; Letko, Zdeněk (vedoucí práce)
Testování vícevláknových programů je náročný proces kvůli velkému množství možných interakcí mezi vlákny, které je třeba otestovat. Technika vkládání šumu umožňuje zvýšit počet otestovaných proložení (interakcí) konkurenčních vláken generováním šumu. Tato práce optimalizuje techniky prohledávání prostoru v oblasti testování vícevláknových programů, a to s využitím deterministických heuristik použitých při aplikací genetických algoritmů na prostor míst v běhu programu, do kterých je možné umístit šum. V práci je navrženo několik nových heuristik vkládání šumu, které jsou deterministické, narozdíl od většiny současných heuristik pracujících s generátorem náhodných čísel. Motivací odstranění náhodnosti je informovanější prohledávání a získávání optimálnějších výsledků pomoci zvýšení stability výsledku poskytovaných novými heuristikami. Součástí práce je i základní sada testovacích programů, která bude použita k vyhodnocení výsledků nových heuristik vkládání šumu.
|
|
|
Pokrytelnosti pro paralelní programy
Turoňová, Lenka ; Vojnar, Tomáš (oponent) ; Holík, Lukáš (vedoucí práce)
Tato diplomová práce se zabývá automatickou verifikací systémů s paralelně běžícími procesy. Práce diskutuje existující metody a možnosti jejich optimalizace. Stávající techniky jsou založeny na hledání induktivního invariantu (například pomocí techniky zjemňování abstrakce řízené protipříklady (CEGAR)). Efektivnost metod závisí na velikosti nalezeného invariantu. V rámci této diplomové práce jsme nalezli možnost zlepšení metod díky zaměření se na hledání invariantů minimální velikosti. Naimplementovali jsme nástroj, který zajišťuje prohledávání prostoru invariantů systému. Naše experimentální výsledky ukazují, že mnoho existujících systémů užívaných v praxi má skutečně mnohem menší invarianty než ty, které lze nalézt stávajícími metodami. Závěry a výsledky této práce budou sloužit jako základ budoucího výzkumu, jehož cílem bude navržení optimální metody pro vypočítání malých invariantů paralelních systémů.
|
|
|
Verifikace ukazatelových programů pomocí lesních automatů
Hruška, Martin ; Rogalewicz, Adam (oponent) ; Holík, Lukáš (vedoucí práce)
V této práci je rozvíjena existující metoda pro shape analýzu programů založená na lesních automatech. Dále je také vylepšována implementace této metody, nástroj Forester. Lesní automaty jsou založeny na stromových automatech, jejichž jednoduchou implementaci Forester obsahuje. Prvním přínosem této práce je nahrazení této implementace knihovnou VATA, která obsahuje efektivní algoritmy pro reprezentaci a manipulaci stromových automatů. Verze nástroje Forester používající knihovnu VATA se zúčastnila mezinárodní soutěže SV-COMP 2015. Dále je verifikace založená na lesních automatech v této práci rozšířena o predikátovou abstrakci a analýzu nalezených protipříkladů. Výsledek této analýzy je možné využít následujícími způsoby. Prvním je určení toho, zda je nalezené chyba reálná nebo naopak nepravá. Druhým je pak zjemnění predikátové abstrakce pomocí predikátů odvozených při zpětném běhu. Obě techniky byly také implementovány v nástroji Forester. Na závěr je zhodnoceno zlepšení, které tyto techniky přinesly oproti původní verzi nástroje Forester.
|
|
|
Studie optimalizace výrobních procesů
Holík, Lukáš ; tesař, Rostislav (oponent) ; Jurová, Marie (vedoucí práce)
Diplomová práce nesoucí název: „Studie optimalizace výrobních procesů“ je zaměřena na optimalizaci materiálových toků plynoucích do výroby. Nejdříve se zaměříme na teoretické přístupy, které ovlivňují danou problematiku a představíme výrobní systém a výrobní program ve zkoumané společnosti. Následně pomocí analýzy konkrétního projektu nadefinujeme nedostatky zkoumaného systému a pomocí teoretických přístupů se budeme snažit zjištěné nedostatky odstranit. V závěrečné části shrneme přínosy nalezeného řešení
|
|
|
Podnikatelský záměr
Holík, Lukáš ; Novák, Zdeněk (oponent) ; Rompotl, Jaroslav (vedoucí práce)
Cílem diplomové práce je vytvořit podnikatelský plán pro pana Davida Mokrého, majitele kavárny s názvem Blue Queen v Boskovicích, který v blízké době chce rozšířit svoji podnikatelskou činnost o další podnik - Black King. Pomocí četných analýz trhu a analýz vnějšího i vnitřního okolí získám data potřebná k vytvoření projektu na vybudování úspěšné nové restaurace, která by se měla stát nejvyhledávanějším podnikem v okolí.
|
host ::
RSS.