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

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.

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í:

• http://www.cs.cas.cz/~ratschan/theses/en/constraint_solving.html

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í:

• http://www.cs.cas.cz/~ratschan/theses/cz/verification.html

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

prof. Ing. Róbert Lórencz, CSc.

Katedra teoretické informatiky

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.

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

doc. Ing. Ivan Šimeček, Ph.D.

Katedra teoretické informatiky

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.

Práce na DSpace

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

Ing. Josef Vogel, CSc.

Katedra softwarového inženýrství

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.

Práce na DSpace

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

Mgr. Jan Starý, Ph.D.

Katedra teoretické informatiky

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.

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

doc. Ing. Jan Schmidt, Ph.D.

Katedra číslicového návrhu

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

Práce na DSpace

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

Katedra softwarového inženýrství

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

Ing. Jiří Daněček

Katedra softwarového inženýrství

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.

Práce na DSpace

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

Ing. Lukáš Bařinka

Katedra softwarového inženýrství

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.

Práce na DSpace

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

doc. Ing. Ivan Šimeček, Ph.D.

Katedra teoretické informatiky

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.

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

Ing. Martin Kohlík, Ph.D.

Katedra číslicového návrhu

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

Mgr. Jan Starý, Ph.D.

Katedra teoretické informatiky

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.

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

prof. Ing. Pavel Tvrdík, CSc.

Katedra softwarového inženýrství

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.

Práce na DSpace

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

doc. RNDr. Pavel Surynek, Ph.D.

Katedra číslicového návrhu

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.

Práce na DSpace