|
|
Unit checking for Java IDE
Kebrt, Michal ; Parízek, Pavel (oponent) ; Šerý, Ondřej (vedoucí práce)
Code model checking is a rapidly advancing research topic. However, apart from very constrained scenarios (e.g., veri cation of device drivers by SLAM), the code model checking tools are not widely used in general software development process. We believe that this could be changed if the developers could use the tools in the same way they already use testing tools. In this work, we present the UnitCheck tool, which enhances the standard unit testing of Java code with model checking. A developer familiar with unit testing can apply the tool on standard unit test scenarios and bene t from the exhaustive traversal performed by a code model checker, which is employed inside UnitCheck. Two well-known Java tools are integrated in UnitCheck. JUnit is used as a testing framework and Java PathFinder provides the model checking capability. The UnitCheck plugin for Eclipse presents the checking results in a convenient way known from unit testing, while providing also a verbose output for the expert users. The UnitCheck Ant task allows to incorporate unit checking in the standard Java development and build process.
|
|
|
Interpretr stavových automatů popsaných jazykem SCXML
Baláž, Ján ; Bulej, Lubomír (oponent) ; Šerý, Ondřej (vedoucí práce)
V súčasnosti vzniká potreba pristupovať ku rôznym programátorským úlohám alternatívnymi postupmi. Jedným z takýchto postupov je zápis pomocou stavových automatov. Ako riešenie sa ukazuje novo vznikajúci štandard W3 Consorcia, nazvaný SCXML. V súčasnosti už existuje niekolko rôznych implementácii, ktoré však kvôli svojej rozsiahlosti nemusia byť vhodné pre jednotlivcov, alebo malé a stredné rmy. Tieto spoločnosti potrebujú nástroje, ktoré si môžu jednoducho prispôsobovať na svoje vlastné projekty. Cielom práce je vytvoriť interpreter stavových automatov popísaných jazykom SCXML, ktorý bude splňať popísané podmienky. Snahou je implementovať maximálnu časť špecikácie SCXML. Práca bude vytvorená v jazyku Perl a bude podporovať operačné systémy Windows a Linux.
|
|
|
Grafický editor 3D scén pro projekt AGE
Herceg, Tomáš ; Šerý, Ondřej (oponent) ; Ježek, Pavel (vedoucí práce)
Název práce: Grafický editor 3D scén pro projekt AGE Autor: Tomáš Herceg Katedra (ústav): Katedra distribuovaných a spolehlivých systémů Vedoucí bakalářské práce: Mgr. Pavel Ježek, Katedra distribuovaných a spolehlivých systémů E-mail vedoucího: pavel.jezek@dsrg.mff.cuni.cz Abstrakt: Cílem práce je vytvořit grafický editor, který umožní tvorbu a editaci grafických scén ve 3D prostoru. Editor by měl být realizován jako rozšiřující modul do projektu AGE. Jelikož je projekt AGE teprve ve fázi vývoje, měla by jako součást této bakalářské práce vzniknout i jeho první verze. Samotný editor vytvořený v rámci práce by měl podporovat vytváření základních primitivních objektů, manipulaci s jednotlivými vrcholy, stěnami a částmi těchto objektů, a dále pak implementovat základní nástroje pro mapování textur. Jako cílová platforma bude použito prostředí .NET Framework a pro zobrazování grafických výstupů je doporučeno použít technologie Windows Presentation Foundation a DirectX. Klíčová slova: Počítačová grafika, Windows Presentation Foundation, DirectX, 3D
|
|
|
Ekonomická tahová strategická hra
Hermann, Lukáš ; Šerý, Ondřej (oponent) ; Lánský, Jan (vedoucí práce)
V předložené práci se zabýváme návrhem a implementací ekonomické tahové strategie. Po popsání a analýze základních pravidel hry vytváříme objektový model, skládající se ze základního rozhraní, konkrétních tříd a jejich propojení mezi sebou. Dále podrobně rozebíráme ekonomické modely a další související algoritmy použité v jejich metodách včetně jejich zapsání v pseudokódu. Nakonec tvoříme editory vlastností a chování herních objekt a zabýváme se tvorbou originálního gra fického interface s konkrétními vizuálními komponentami, z nichž sestavujeme uživatelské prostředí.
|
|
|
Sewing pattern editor
Černý, Martin ; Poch, Tomáš (oponent) ; Šerý, Ondřej (vedoucí práce)
Konstrukce střihů je základní součástí oděvního návrhářství. Předmětem této práce je implementace editoru textilních střihů, který by vyhovoval potřebám nezávislých oděvních návrhářů a výrobců zakázkového šatstva. Práce v editoru je velmi blízká ručnímu navrhování střihu a program je tedy pro návrháře snadno použitelný. Implementace pokrývá nejdůležitější oblasti navrhování střihů. Střihy v programu vytvořené mohou být použity pro různé zákazníky, protože se automaticky přizpůsobují zadaným tělesným mírám.
|
|
|
Frontend pro matematicky vyhledavac
Klíma, Jaroslav ; Mišutka, Jozef (vedoucí práce) ; Šerý, Ondřej (oponent)
Elektronický zápis matematických výrazů získává na důležitosti se stoupající tendencí využití softwaru v každodenním živote. Školy začnají podporovat e-learning, studenti i vědci prezentují své práce na internetu a vyhledávače se dokáží vypořádat se stále komplexnějšími dotazy. V předložené práci shrnu stav dostupných aplikací které podporují vkládání matematických výrazů a které by bylo možno využít jako uživatelské rozhraní pro matematický vyhledávač EgoMath. Protože žádná z nich nesplňuje naše požadavky, prezentuji zde návrh a implementaci nového matematického uživatelského rozhraní zaměřeného na zjištené nedostatky existujících řešení. Cílem nového rozhraní je umožnit uživateli zadání matematického výrazu ve formátu který dokáže zpracovat cílová aplikace. Výraz obsahující symboly z velké množiny je nutno zadávat pomocí omezeného počtu kláves. Toto musí být intuitivní a aplikace by měla uživateli aktivně pomáhat grafickou nápovědou založenou na rozpoznávání vkládaného výrazu v reálném čase.
|
|
|
Vizualiazace algoritmů pomocí uživatelských scriptů
Šebesta, Jiří ; Šerý, Ondřej (oponent) ; Ježek, Pavel (vedoucí práce)
Cílem této práce bylo vytvoření programu AlgoShow sloužícího pro názornou ukázku fungování algoritmů. Algoritmy se zapisují jako skripty, ve kterých je možno využívat různých funkcí pro grafické znázornění běhu algoritmu. Práce se zabývá programem AlgoShow jak z uživatelského, tak i z programátorského hlediska. Součástí je krátký úvod do problematiky vizualizace algoritmů, srovnání programu AlgoShow s podobnými existujícími nástroji, popis návrhu a implementace programu včetně způsobu interpretace skriptu. Dále práce obsahuje charakteristiku základních funkcí programu a zejména podrobný popis skriptovacího jazyka.
|
|
|
Interpretr stavových automatů popsaných jazykem SCXML
Baláž, Ján ; Parízek, Pavel (oponent) ; Šerý, Ondřej (vedoucí práce)
V súčasnosti vzniká potreba pristupovať ku roznym programátorským úlohám alternatívnymi postupmi. Jedným z takýchto postupov je zápis pomocou stavových automatov. Ako riešenie sa ukazuje novo vznikajúci štandard W3 Consorcia, nazvaný SCXML. V súčasnosti už existuje niekolko roznych implementácii, ktoré však kvoli svojej rozsiahlosti nemusia byť vhodné pre jednotlivcov, alebo malé a stredné fi rmy. Tieto spoločnosti potrebujú nástroje, ktoré si možu jednoducho prisposobovať na svoje vlastné projekty. Cielom práce je vytvoriť interpreter stavových automatov popísaných jazykom SCXML, ktorý bude splňať popísané podmienky. Snahou je implementovať maximálnu časť špecifikácie SCXML. Práca bude vytvorená v jazyku Perl a bude podporovať operačné systémy Windows a Linux.
|
|
|
Model Checking and Reduction of Behavior Protocols
Šerý, Ondřej ; Bednárek, David (oponent) ; Plášil, František (vedoucí práce)
Behavior protokol je formalismus pro specifikaci chování softwarových komponent. V syntaxi podobné regulárním výrazům jsou definovány přípustné sekvence volání metod, přičemž se abstrahuje od vnitřních dat komponent. Jde sice o rozumnou úroven abstrakce pro ověření bezchybnosti komunikace softwarových komponent, nicméne pro člověka může být jeho přečtení a pochopení obtížné. Tato práce se snaží pomoci softwarovému návrháři pochopit specifikaci chování komponent. Předkládá způsob automatického ověřování platnosti obecných časových vlastností vyjádřených v lineární temporální logice spolu s dvěmi technikami redukce behavior protokolu. Redukce vzhledem ke kompozici odstraní ty části protokolu, které nejsou použity v dané kompozici komponent, a zdůrazní tak skutečné role všech komponent. Redukce vzhledem k vlastnosti vypustí ty části protokolu, které nejsou podstatné pro danou vlastnost. Takto redukovaný protokol by měl zdůraznit části, které zapříčiňují platnost dané vlastnosti.
|
|
|
Influence of inhaled manganese oxides nanoparticles on mass of internal organs in mice
Zeman, T. ; Dočekal, Bohumil ; Mikuška, Pavel ; Buchtová, Marcela ; Míšek, Ivan ; Šerý, Omar ; Večeřa, Zbyněk
Results of the statistical analysis of a long-term inhalation experiment on laboratory mice are presented. During 17 weeks of the experiment, the experimental group was exposed to inhaled manganese oxides nanoparticles. Manganese oxides (MnO center dot Mn2O3) nanoparticles (MnONPs) were synthesized continuously via aerosol route in a hot wall tube flow reactor using a thermal decomposition of metal organic precursor manganese(II) acetylacetonate in the flow tube reactor (in vertical position) at temperature 750 degrees C in the presence of 30 vol% of oxygen. The concentration of produced MnONPs at the reactor output was in the range 1-3 x 10(7) particles/cm(3) and the size of generated nanoparticles MnO center dot Mn2O3 was in the range 7-50 nm. Before entering the inhalation chamber, MnONPs in the mixture of N-2, O-2 and air (at total flow rate of 3 L/min) were further diluted using filtrated humidified air (20 L/min) at temperature 21 degrees C resulting in the MnONPs concentration 2 x 10(6) particles/cm(3). At regular time intervals the mass of selected internal organs of mice from both experimental and control group was assessed. It has been proven that inhaled nanoparticles are able to influence the mass of internal organs of mice. Statistically significantly lower mass of kidneys, liver and spleen and higher mass of pancreas have been found in the experimental group compared to the control group.
|
host ::
RSS.