doc. Dipl.-Ing. Dr. techn. Stefan Ratschan

Závěrečné práce

Dizertační práce

Proveditelné specifikace

Stupeň
Téma dizertační práce
Popis tématu

Jeden z nedostatků klasických metod pro specifikaci softwarových požadavků je obtížnost ověření konzistence a adekvátnosti specifikací. Softwarové inženýrství reagovalo na tuto skutečnost různými metodami (např. model based software engineering, agile software development, executable algebraic specification), které umožňují vidět praktické chování specifikací ve vývojovém procesu co nejdříve. Tyto metody ale dělají kompromisy ohledně jiných aspektů, týkajících se např. expresivity anebo preciznosti. V rámci tohoto tématu student navrhne formální jazyk, který splní dva na první pohled protichůdné cíle:

• Jazyk má expresivitu tak vysokou, aby mohl sloužit k pohodlnému psaní specifikací

• Specifikace v tomto jazyku se dají provést podobně jako programy v obvyklém programovacím jazyku

Klíčem pro současné splnění obou cílů budou anotace, kterými uživatel jazyku poskytuje informaci o vykonávání specifikace tak, aby zvýšená snaha o psaní anotací měla za důsledek zvýšenou účinnost vykonávání. Prvním krokem bude vývoj nástroje pro výuku, který dovoluje studentům, kteří píšou specifikace jako úkol ve cvičení, jejich řešení hned i spustit a otestovat.

Řešení omezujících podmínek

Stupeň
Téma dizertační práce
Popis tématu

Vyvíjíme software, teorii a algoritmy, které umí řešit matematické formule obsahující nelineární rovnice a nerovnice, konjunkce, disjunkce, a logické kvantifikátory. Aplikujeme výslednou technologii v několika oblastech (např. verifikace složitých systémů, výpočet Lyapunových funkcí). Nabízíme velké množství témat v této oblasti.

Více informací:

Verifikace složitých systémů

Stupeň
Téma dizertační práce
Popis tématu

Vlak Pendolino z Prahy do Ostravy měl na začátku vážné problémy: občas zastavoval během jízdy kvůli chybě v softwaru. Podobné chyby způsobovaly vážná neštěstí, například havárii raketoplánu Ariane 5 v roce 1996. Náš výzkum je zaměřen na pomoc s tím, aby se v budoucnosti bylo možné takovým problémům vyhýbat. Nabízíme velké množství témat v této oblasti.

Více informací:

Bakalářské práce

Vliv druhu aritmetiky na Korovin/Tsiskaridz/Voronkovův algoritmus pro řešení lineárních nerovnic

Autor
Tomáš Makara
Rok
2013
Typ
Bakalářská práce
Vedoucí
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Oponenti
prof. Ing. Róbert Lórencz, CSc.
Anotace
Táto práca sa zaoberá Korovin/Tsiskaridz/Voronkovým algoritmom určeným k riešeniu lineárnych nerovníc. Skúma možnosti použitia aritmetiky s pohyblivou desatinnou čiarkou pre výpočet riešenia sústavy lineárnych nerovníc využitím uvedeného algoritmu. Práca obsahuje popis algoritmu a popis úprav algoritmu, ktoré by umožňovali použitie aritmetiky s pohyblivou desatinnou čiarkou. Súčasťou práce je implementácia algoritmu a meranie jej časovej zložitosti.

Heuristiky pro propagaci intervalů

Autor
Jakub Kottnauer
Rok
2016
Typ
Bakalářská práce
Vedoucí
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Oponenti
doc. Ing. Ivan Šimeček, Ph.D.
Anotace
Omezující podmínka je relace mezi proměnnými omezující množiny hodnot, kterých mohou proměnné nabývat. Problém splnitelnosti omezujících podmínek (CSP) je problém, jehož řešení spočívá v nalezení hodnot proměnných tak, aby byly splněny všechny zadané omezující podmínky. Hlavním cílem práce je otestování vlivu heuristik na efektivitu řešení numerických CSP pomocí propagací intervalů. Součástí práce byl napsán řešič v jazyce F# implementující algoritmy HC3 a branch-and-prune s podporou pro podmínky s operacemi sčítání, odčítání a násobení. Byly nalezeny podstatné parametry algoritmu ovlivňující jeho účinnost a následně byly s třinácti heuristikami provedeny výpočetní experimenty a jejich výsledky porovnány. Výstup práce bude možno využít při rozvažování, kterou heuristiku použít při řešení soustav omezujících podmínek převeditelných na podmínky s výše uvedenými operacemi.

Automatická syntéza funkcí pomocí řešičů splnitelnosti modulo teorií

Autor
Petr Nagy
Rok
2023
Typ
Bakalářská práce
Vedoucí
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Oponenti
Ing. Josef Vogel, CSc.
Anotace
Bakalářská práce se věnuje řešiči modulo teorií cvc5. Jejím prvotním cílem je výzkum možností řešiče pro automatickou syntézu funkcí a použití tohoto řešiče v praxi. Prozkoumává jeho chování pomocí existujících benchmarkových problémů cvc5 a jazyka SyGuS, včetně vlastních příkladů, a dochází k závěru, že cvc5 má velice dobrý potenciál pro využití v praxi. Zároveň však nachází omezení, například to, že cvc5 zatím nepodporuje rekurzi. V současné době se cvc5 používá pro statickou kontrolu kódu, ale třeba i generování testovacích příkladů. Dalším cílem práce bylo vytvoření grafického rozhraní, které usnadní používání cvc5 pro syntézu funkcí. Grafické rozhraní bylo vytvořeno po analýze současných řešení tak, aby podporovalo všechny funkce řešiče a zároveň i samotnou tvorbu a úpravu kódu.

Řešení omezujících podmínek s prefixem kvantifikátorů exists-forall

Autor
Pavel Frumert
Rok
2016
Typ
Bakalářská práce
Vedoucí
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Oponenti
Mgr. Jan Starý, Ph.D.
Anotace
Cílem této práce je experimentální ověření metody na řešení omezujících pod- mínek. Účinnost metody je zkoumána na speciálním typu příkladů spadají- cích do třídy QCSP. V těchto příkladech existenční kvantifikátory předchá- zejí obecné. Další charakteristikou jsou spojité domény proměnných. Kromě samotné splnitelnosti nás zajímá i konkrétní ohodnocení existenčně kvantifi- kovaných proměnných. Dále tato práce pojednává o implementaci metody v programu wolfram mathematica.

Diplomové práce

Deadline Verification Using Model Checking

Autor
Jan Onderka
Rok
2020
Typ
Diplomová práce
Vedoucí
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Oponenti
doc. Ing. Jan Schmidt, Ph.D.
Anotace
V této práci je představena nová aplikace pro formální verifikaci splnění nejzazších termínů (deadlines) v jednoduchých programech pro mikrokontroléry, pracující na úrovni strojového kódu. V práci jsou studovány dosavadní techniky a nástroje pro formální verifikaci. Jsou identifikovány jejich slabé stránky. Nevýhodou verifikačních technik pracujících na úrovni zdrojového kódu je zejména jejich neschopnost zaručit časy provádění na úrovni cyklů procesoru. Současných nástrojů pro verifikaci na úrovni strojového kódu je málo, nejsou široce dostupné a většinou jsou specificky navrženy pro konkrétní procesor, což velmi snižuje jejich užitečnost. Aby nová aplikace nevykazovala nedostatky stávajících řešení, je navržen a implementován nový hybridní verifikační přístup. Techniky ověřování modelu na úrovni strojového kódu jsou použity pro reprezentaci stavového prostoru a verifikaci dodržení specifikace. Paměť mikrokontroléru a chování v rámci kroku jsou specifikovány pomocí jednoduchého imperativního jazyka, s kterým je možné manipulovat pomocí standardních technik na úrovni zdrojového kódu. Tím je umožněna kontrola splnění nejzazších termínů na úrovni cyklů procesoru, rozšiřitelnost na další mikrokontroléry vedle již implementovaného ATmega328P a implementace pokročilých technik bez závislosti na konkrétním použitém procesoru. Vedle základní funkcionality programu jsou implementovány pokročilé techniky pro zacházení s nedeterminismem, generování řídícího toku a redukci cest pro jednoduché cykly. Aplikace je testována pro prokázání její užitečnosti pro verifikaci splnění nejzazších termínů pro jednoduché programy. Je diskutován dopad použitých technik a jsou identifikovány slibné cesty pro další zlepšení.

Formální verifikace kombinovaného systému počítačového programu a fyzikálního okolí

Autor
Tomáš Zrůst
Rok
2015
Typ
Diplomová práce
Vedoucí
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan

Interaktivní dokazovací asistent pro výuku formálních metod

Autor
Martin Bedrna
Rok
2024
Typ
Diplomová práce
Vedoucí
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Oponenti
Ing. Jiří Daněček
Anotace
Tato práce se věnuje implementaci dokazovacího asistenta. Odvozovací pravidla dokazovacího kalkulu používaná asistentem jsou verzí přirozené dedukce. V rámci této práce je problém nejdříve představen po teoretické stránce. Následně je provedena analýza a softwarový návrh. Nakonec je popsána implementace vytvořeného softwaru.

Software pro grafickou demonstraci plánování pohybu kvadrokoptér

Autor
Tomáš Mahr
Rok
2018
Typ
Diplomová práce
Vedoucí
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Oponenti
Ing. Lukáš Bařinka
Anotace
Práce se zabývá návrhem a implementací aplikace pro grafickou demonstraci plánování pohybu kvadrokoptér. Je kladen duraz na modulárnost softwaru. Dále je vyložena základní teorie plánování pohybu kvadrokoptér a je implementován jeden z existujících algoritmu pro plánování pohybu.

Spolehlivá charakterizace existence řešení parametrických soustav rovnic

Autor
Libor Vytlačil
Rok
2018
Typ
Diplomová práce
Vedoucí
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Oponenti
doc. Ing. Ivan Šimeček, Ph.D.
Anotace
Tato práce se zabývá charakterizací množin bodů $p\in P$, pro které exis\-tu\-je reálné řešení $x$ dané parametrické soustavy rovnic $f_P(x,p)=0$, kde ${f_P\colon X\subseteq\Rsetn{n}\to\Rsetn{n}}$ je spojitá funkce zapsaná ve formě aritmetických výrazů a $X$ je box (součin uzavřených reálných intervalů). Je navržen a implementován algoritmus typu branch and bound založený na intervalové aritmetice a testu existence řešení pomocí Brouwerova topologického stupně. Implementace umožňuje několik způsobů manipulace s do\-mé\-nou $X$ a další parametrizace své činnosti. Intervalová aritmetika slouží jednak k výpočtu odhadů obrazů funkcí, jednak k zajištění robustnosti vzhledem k zaokrouhlovacím chybám. Implementace je poskytnuta v podobě samostatné aplikace včetně uživatelského rozhraní (textového i grafického). Na základě výsledků experimentů, které jsou uloženy ve formě skriptů pro snadnou reprodukovatelnost, je naše implementace schopna produkovat kvalitní výsledky a skončit v rozumném čase pro různorodé nelineární soustavy až o třech rovnicích, které mohou obsahovat kombinace elementárních funkcí jako $\exp$, $\log$, $\sin$, $\cos$, $\arcsin$, $\arccos$, $n$-tá odmocnina, $\dots$. Přispíváme také k dosavadní práci týkající se praktického počítání topologického stupně popisem a použitím vlastní spolehlivé metody pro stanovení, zda pro libovolné boxy $X'\subseteq X$, $P'\subseteq P$ je definován stupeň $\tdeg(f_p, X', 0)$ a má pro každý parametr $p\in P'$ stejnou hodnotu.

Inkrementální verifikace bezpečnosti na základě binárních rozhodovacích stromů

Autor
Vojtěch Hovorka
Rok
2013
Typ
Diplomová práce
Vedoucí
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Oponenti
Ing. Martin Kohlík, Ph.D.

Knihovna pro ortogonální mnohostěny

Autor
Ondřej Šmíd
Rok
2016
Typ
Diplomová práce
Vedoucí
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Oponenti
Mgr. Jan Starý, Ph.D.
Anotace
V práci provádíme rešerši reprezentací ortogonálních mnohostěnů libovolné dimenze a existujících efektivních algoritmů, které na reprezentovaných mnohostěnech uskutečnují booleovské operace, výpočet hranice a zjištění membershipu. Implementujeme tyto reprezentace pro mnohostěny, jejichž souřadnice jsou čísla s plovoucí řádovou čárkou.

Zacházení s datovými strukturami na haldě ve zpětné symbolické exekuci

Autor
Robert Husák
Rok
2018
Typ
Diplomová práce
Vedoucí
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Oponenti
prof. Ing. Pavel Tvrdík, CSc.
Anotace
Cílem této práce je významně rozšířit AskTheCode, dříve vytvořený doplněk nástroje Microsoft Visual Studio, který využívá zpětnou symbolickou exekuci pro verifikaci asercí v kódu C#. Jedno z největších omezení našeho doplňku byla neschopnost analyzovat objekty na haldě a operace na nich. Pro doplnění této funkcionality jsme nejdříve začali rešerší existujících postupů, ze kterých jsme vybrali tři nejzajímavější: línou inicializaci, symbolickou inicializaci a využití teorie polí. Tyto techniky jsme důkladně analyzovali s přihlédnutím na specifické požadavky našeho nástroje. Díky jejím očekáváným výkonnostním charakteristikám jsme vybrali použití teorie polí. Tuto techniku jsme transformovali, aby ji bylo možné využít ve zpětné symbolické exekuci, včetně efektivního využití zásobníků podmínek v SMT řešičích. Na řadě příkladů v jazyce C# jsme následně ukázali korektnost této implementace.

SAT s diferenciálními rovnicemi

Autor
Tomáš Kolárik
Rok
2018
Typ
Diplomová práce
Vedoucí
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Oponenti
doc. RNDr. Pavel Surynek, Ph.D.
Anotace
Na mnoho dnešnich systémů, např. vestavných, jsou kladeny vysoké nároky na splněni specifikaci, které často závisi na jevech z fyzikálniho okoli. Pro rozsáhlé systémy se osvědčuje použiti formálni verifikace jako nástroje pro garanci splněni specifikaci. Formálni verifikace exaktně ověřuje matematický model systému; jednim z použivaných postupů je např. SAT. Problém nastává, když potřebujeme v mo- delu použit také diferenciálni rovnice (ODE), které jsou pro popis fyzikálnich jevů zcela přirozené. Práce se zabývá ověřenim konceptu, který kombinuje SAT i ODE a lze použit např. pro formálni verifikaci modelů vestavných systémů. Takové řešiče již existuji (např. dReal), ale jsou v praxi těžko použitelné, jelikož při řešeni ODE vice dbaji na přesnost, ale jsou pomalé. Cilem bylo pro ODE použit klasických numerických metod, které mohou být méně přesné, ale jsou rychlejši. Součásti práce je prototyp nástroje nazvaný SOS (SMT+ODE Solver), který kombinuje SMT (rozšiřeni problému SAT) s diferenciálnimi rovnicemi. SMT a ODE řešiče jsou oba nezávislé od ostatnich komponent. Použit byl řešič odeint, a z SMT řešičů to byly CVC4 a z3. Hlavnimi výstupy jsou zjištěni, že použiti klasických numerických metod urychluje celkový výpočet, a dále, že výpočet úloh s přesnými počátečnimi podminkami (IVP) je mnohem rychlejši, než úloh s intervaly (IIVP). Intervaly lze přitom efektivně aproximovat výčty hodnot v logickém součtu. Tato zjištěni potvrzuji náš zvolený koncept, a byla ověřena v některých přikladech, kdy byl náš postup rychlejši, než u stávajiciho řešiče dReal. Tim bylo dosaženo cile v praxi použitelnějšiho přistupu k formálni verifikaci systémů s diferenciálnimi rovnicemi. Práce by měla sloužit jako zdroj inspirace pro vývojáře průmyslových nástrojů, anebo by také mohla být nadále vyvijena a zefektivňována v rámci stávajiciho projektu s otevřenými zdrojovými kódy.

Dizertační práce

Boolean Satisfiability Modulo Differential Equation Simulations

Autor
Ing. Tomáš Kolárik
Rok
2024
Typ
Dizertační práce
Vedoucí
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Oponenti
Prof. Dr. Martin Fränzle, Prof. Kazunori Ueda,Prof. Étienne André