|
|
Simulace a protiřetězce pro efektivní práci s konečnými automaty
Holík, Lukáš ; Černá, Ivana (referee) ; Jančar, Petr (referee) ; Vojnar, Tomáš (advisor)
Cílem této práce je vývoj technik umožňujících praktické využití nedeterministických konečných automatů, zejména nedeterministických stromových automatů. Jde zvláště o techniky pro redukci velikosti a testování jazykové inkluze, jež hrají zásadní roli v mnoha oblastech aplikace konečných automatů. V oblasti redukce velikosti vycházíme z dobře známých metod pro slovní automaty které jsou založeny na relacích simulace. Navrhli jsme efektivní algoritmy pro výpočet stromových variant simulačních relací a identifikovali jsme nový typ relace založený na kombinaci takzvaných horních a dolních simulací nad stromovými automaty. Tyto kombinované relace jsou zvláště vhodné pro redukci velikosti automatů slučováním stavů. Navržený princip kombinace relací simulace je relevantní i pro slovní automaty. Náš přínos v oblasti testování jazykové inkluze je dvojí. Nejprve jsme zobecnili na stromové automaty takzvané protiřetězcové algoritmy, které byly původně navrženy pro slovními automaty. Dále se nám podařilo použitím simulačních relací výrazně zefektivnit protiřetězcové algoritmy pro testování jazykové inkluze jak pro slovní, tak pro stromové automaty. Relevanci našich technik pro praxi jsme demonstrovali jejich nasazením v rámci regulárního stromového model checkingu, což je verifikační metoda založená na stromových automatech. Použití našich algoritmů zde vedlo k výraznému zrychlení a zvětšení škálovatelnosti celé metody. Základní myšlenky našich algoritmů pro redukci velikosti automatů a testování jazykové inkluze jsou aplikovatelné i na jiné typy automatů. Příkladem jsou naše redukční techniky pro alternující Büchiho automaty prezentované v poslední části práce.
|
|
|
One-Sided Random Context Grammars
Zemek, Petr ; Černá, Ivana (referee) ; Doc. In.g Petr Sosík, Dr. (referee) ; Meduna, Alexandr (advisor)
Tato disertační práce zavádí jednostranné gramatiky s nahodilým kontextem jako řízené gramatiky založené na bezkontextových gramatikách. V těchto gramatikách je ke každému pravidlu přiřazena množina povolujících symbolů a množina zakazujících symbolů a množina pravidel je rozdělena na množinu levých pravidel s nahodilým kontextem a množinu pravých pravidel s nahodilým kontextem . Levým pravidlem s nahodilým kontextem lze přepsat neterminál pokud se všechny povolující symboly vyskytují vlevo od přepisovaného neterminálu a žádný zakazující symbol tam přítomen není. Pravé pravidlo s nahodilým kontextem lze aplikovat analogicky, ale ona kontrola na přítomnost a nepřítomnost symbolů je provedena doprava od přepisovaného neterminálu. Práce je rozdělena na tři části. První část uvádí motivaci za zavedením jednostranných gramatik s nahodilým kontextem a umisťuje materiál pokrytý v této práci do vědeckého kontextu. Poté dává přehled základů teorie formálních jazyků a některých méně známých oblastí, jejichž znalost je nutná pro pochopení studovaného tématu. Druhá část tvoří jádro práce. Formálně definuje jednostranné gramatiky s nahodilým kontextem a studuje je z mnoha pohledů. Mezi studovaná témata patří generativní síla, vztah k jiným typům gramatik, redukce, normální formy, nejlevější derivace, zobecněné a LL verze těchto gramatiky. Třetí část této práce zakončuje diskusi několika poznámkami. Mezi ně patří poznámky týkající se aplikovatelnosti zavedených gramatik v praxi, bibliografie a otevřených problémů.
|
|
|
On Parallel Processing in Formal Models: Jumping Automata and Normal Forms
Kocman, Radim ; Černá, Ivana (referee) ; Janoušek, Jan (referee) ; Meduna, Alexandr (advisor)
Tato disertační práce představuje a zkoumá nové možnosti paralelního zpracování ve formálních modelech. Zaměřuje se přitom především na paralelní verze skákajících konečných automatů a na normální formy gramatik se zajímavými paralelními vlastnostmi. První část práce popisuje motivaci pro studium paralelního zpracování ve formálních modelech a stručně představuje skákající modely a normální formy gramatik a gramatických systémů. Jsou zde také upřesněny cíle prezentovaného výzkumu. Druhá část práce je zaměřena na prezentaci nových výsledků v oblasti skákajících konečných automatů. Jako první je zde přestaven n-paralelní skákající konečný automat, který rozšiřuje původní model skákajícího konečného automatu a podporu většího množství čtecích hlav. Práce následně studuje sílu tohoto modelu ve dvou rozdílných skákajících módech. Následuje představení dvojitě skákajících konečných automatů, u kterých jsou zkoumány pokročilé skákající módy využívající dvě čtecí hlavy. Kromě síly těchto modelů jsou zde zkoumány i uzávěrové vlastnosti příslušných tříd jazyků. Jako poslední jsou v této části představeny skákající 5'->3' Watson-Crick konečné automaty, které kombinují skákající chování s biologií inspirovanými Watson-Crick konečnými automaty. Opět je zde zkoumána síla tohoto modelu a to i s uvážením rozličných omezujících podmínek. Třetí část práce je zaměřena na prezentaci nových výsledků v oblasti CD gramatických systémů. Jsou zde prezentovaný dva typy transformací, které dokáží převést libovolnou obecnou gramatiku na dvoukomponentový obecný CD gramatický systém velmi redukované a zjednodušené formy. Kromě této významné redukce a zjednodušení prezentuje práce i několik dalších užitečných vlastností souvisejících s těmito systémy. V poslední části textu jsou pak nastíněny možné oblasti využití představených modelů a normálních forem. Práce je následně uzavřena souhrnem dosažených výsledků a závěrečnými poznámkami k dalšímu směřování výzkumu.
|
|
|
Formal Verfication of Components in Java
Parízek, Pavel ; Plášil, František (advisor) ; Černá, Ivana (referee) ; Pasareanu, Corina (referee)
Formal veri cation of a hierarchical component application involves (i) checking of behavior compliance among sub-components of each composite component, and (ii) checking of implementation of each primitive component against its behavior speci cation and other properties like absence of concurrency errors. In this thesis, we focus on veri cation of primitive components implemented in Java against the properties of obeying a behavior speci cation de ned in behavior protocols (frame protocol) and absence of concurrency errors. We use the Java PathFinder model checker as a core veri cation tool. We propose a set of techniques that address the key issues of formal veri cation of real-life components in Java via model checking: support for high-level property of obeying a behavior speci cation, environment modeling and construction, and state explosion. The techniques include (1) an extension to Java PathFinder that allows checking of Java code against a frame protocol, (2) automated generation of component environment from a model in the form of a behavior protocol, (3) efficient construction of the model of environment's behavior, and (4) addressing state explosion in discovery of concurrency errors via reduction of the level of parallelism in a component environment on the basis of static analysis of Java...
|
|
|
Towards thread aware component behavior specifications
Poch, Tomáš ; Plášil, František (advisor) ; Černá, Ivana (referee) ; Hennicker, Rolf (referee)
The component based development is a well established methodology of software development. The industry, however does not take the advantage of component behavior modeling. Although the analyses of models guarantee notiobn of correctness in form of behavioral compatibility of component composition, the application in practice is limited by the expressiveness of the modeling languages as well as by the fact that the manual preparation of models is demanding and error prone task. To ease the application of behavioral modeling in practice, we propose Threaded Behavior Protocols (TBP) |a modeling language aiming at the gap between the modeling and imperative languages and the imperative languages. By providing the developers with the concepts known from the imperative languages at the model level, we enable easier preparation of component models. The theoretical framework of TBP provides the notion of correctness based on absence of communication errors and the re nement relation preserving the correctness in arbitrary environment. Thus, the analyses supported by the framework provide similar bene ts as the legacy modeling languages, however considering also the imperative language concepts.
|
|
|
Reviews of Individually Prepared Semisolid Preparations
Černá, Ivana ; Šnejdrová, Eva (advisor) ; Šklubalová, Zdeňka (referee)
The aim of the rigorous thesis was to evaluate the preparation of chosen semisolid dosage forms prepared at the pharmacy, optimize the composition and procedure, and revise technological regulations for compounding. Rheological behaviour of semisolid preparations, adhesive properties of the gels and dissolution time of gels intended for application into the oral cavity were studied. Viscosity was measured using digital Brookfield viscometer, or Ubbelohde capillary viscometer. There was no significant difference between the rheological behaviour of preparation prepared using Unguator,® or using mortar. Two different methods were used for testing of adhezivity on mucin substrate; flow-through method, and method of the adhesive material detachment of from the substrate using material testing machine Zwick/Roell. With regard to force and duration of adhesion the gels of methylcellulose were showed as the most suitable for application onto the mucus of the oral cavity. Gel intended for dissolution in the oral cavity were formed into the vaginal suppositories mould to specify the dosing. The pharmacopoeia test for disintegration of tablets and capsules was performed to determine the dissolution time of the globules. It was found, that the gels of agar are not suitable for this type of application due to...
|
|
|
Towards thread aware component behavior specifications
Poch, Tomáš ; Plášil, František (advisor) ; Černá, Ivana (referee) ; Hennicker, Rolf (referee)
The component based development is a well established methodology of software development. The industry, however does not take the advantage of component behavior modeling. Although the analyses of models guarantee notiobn of correctness in form of behavioral compatibility of component composition, the application in practice is limited by the expressiveness of the modeling languages as well as by the fact that the manual preparation of models is demanding and error prone task. To ease the application of behavioral modeling in practice, we propose Threaded Behavior Protocols (TBP) |a modeling language aiming at the gap between the modeling and imperative languages and the imperative languages. By providing the developers with the concepts known from the imperative languages at the model level, we enable easier preparation of component models. The theoretical framework of TBP provides the notion of correctness based on absence of communication errors and the re nement relation preserving the correctness in arbitrary environment. Thus, the analyses supported by the framework provide similar bene ts as the legacy modeling languages, however considering also the imperative language concepts.
|
|
|
Formal Verfication of Components in Java
Parízek, Pavel ; Plášil, František (advisor) ; Černá, Ivana (referee) ; Pasareanu, Corina (referee)
Formal veri cation of a hierarchical component application involves (i) checking of behavior compliance among sub-components of each composite component, and (ii) checking of implementation of each primitive component against its behavior speci cation and other properties like absence of concurrency errors. In this thesis, we focus on veri cation of primitive components implemented in Java against the properties of obeying a behavior speci cation de ned in behavior protocols (frame protocol) and absence of concurrency errors. We use the Java PathFinder model checker as a core veri cation tool. We propose a set of techniques that address the key issues of formal veri cation of real-life components in Java via model checking: support for high-level property of obeying a behavior speci cation, environment modeling and construction, and state explosion. The techniques include (1) an extension to Java PathFinder that allows checking of Java code against a frame protocol, (2) automated generation of component environment from a model in the form of a behavior protocol, (3) efficient construction of the model of environment's behavior, and (4) addressing state explosion in discovery of concurrency errors via reduction of the level of parallelism in a component environment on the basis of static analysis of Java...
|
|
|
Quantitative binding of different analogues of vancomycine to D-Ala-D-Ala using surface plasmon resonance
Černá, Ivana ; Szotáková, Barbora (advisor) ; Kubíček, Vladimír (referee)
Charles University in Prague Faculty of Pharmacy in Hradec Králové Department of Biochemical Sciences Candidate: Ivana Černá Consultant: Drª María José Hernáiz Gómez-Dégano Doc. Ing. Barbora Szotáková, PhD. Title: Quantitative binding of different analogues of vancomycine to D-Ala-D-Ala using surface plasmon resonance This diploma thesis discusses the interaction studies of different glycopeptide antibiotics: teicoplanin; MDL 63,246; mideplanin; BI 397 (dalbavancin); A 40926 and vancomycin with D-Ala-D-Ala dipeptide. Firstly, the HPLC analysis conditions for these antibiotics were defined and optimized in order to probe their purity. Then, the interaction studies were carried out, for that various self-assembled monolayers (SAM) were prepared based on different hydrophobicity and length of the chain. These SAMs were functionalized with the dipeptide D-Ala-D-Ala for the study of the binding with the antibiotics. The results suggest that the best way to prepare the SAM is incubation of the chip overnight in the ethanol solution of alcanothiol chain. The most applicable SAM for the study of interaction of antibiotic to D-Ala-D-Ala is formed by alcanothiol chain with a carbon chain of 8 carbons and a tetraethylene glycol chain ending in a carboxylic group. Over this surface we performed the study of...
|
|
|
Behavior Composition in Component Systems
Adámek, Jiří ; Plášil, František (advisor) ; Černá, Ivana (referee) ; Madelaine, Erik (referee)
In order to formally verify a component application, it is suitable to structure the formal specification of its behavior according to the application architecture. Such an approach eases the maintenance of the specification and allows utilizing efficient verification algorithms that are based on decomposition of the application into several communicating parts. How those parts cooperate is formally described via an operation that is called behavior composition. In this thesis we claim that in current software component systems behavior composition has typically two drawbacks: (1) it lacks support for composition error detection and (2) it does not address the problem of unbounded parallelism specification. While detection of composition errors allows checking design inconsistencies at a design time, unbounded parallelism specification is necessary for precise formal description of reentrant components that are used in practice very often. Therefore we introduce two new concepts - the consent operator and the behavior templates - in order to address both the issues (1) and (2). Our solutions are demonstrated on the SOFA component model [35], behavior protocols [32] are used as a behavior specification language.
|
guest ::
RSS feed.