Program kolokvií s abstrakty pro semestr Jaro 2003

4. 3. 2003: Doc. Lubos Brim, CSc, FI MUNI Brno; Parallel and distributed model checking; Abstract: Model checking has already proved its usefulness in system verification. It is successfully applied to find subtle bugs in complex systems. However, it is limited to medium size systems because of its high space requirements. Many approaches to overcome this problem have been suggested. In recent years there has been a growing interest in parallelizing and/or distributing model checking with the aim to obtain greater space capacity and computation power. In the talk we will survey some of the approaches to distribution of model checking algorithms. We will consider enumerative algorithms that handle reachability, as well as LTL, CTL and Mu-calculus model checking.
18. 3. 2003: Prof. Miroslav Sveda, FIT, VUT Brno; Formal specifications reuse for design of embedded systems; Abstract: Formal methods appear too expensive for a widespread industrial utilization. Common paradigms dictate to employ reuse in this case. We will present reuse of behavioral specifications employing state or timed-state sequences, and their closed-form descriptions by finite-state or timed automata using two case studies based on real design projects: (1) petrol pumping station dispenser controller and (2) multiple lift control system. In the talk we will focus both on identification of reusable component specifications and on their retrieval, adaptation, and storage with case-based reasoning support.
25. 3. 2003: Doc. Antonin Kucera, FI, MU, Brno; Faktory a filtrace prechodovych systemu; Abstract: Semanticke ekvivalence procesu a modalni logiky procesu definuji dve na prvni pohled nesouvisejici techniky redukce stavoveho prostoru prechodovych systemu. Tou prvni je faktorizace stavoveho prostoru podle dane semanticke ekvivalence, tou druhou pak filtrace prechodoveho systemu podle dane formule modalni logiky. Ukazeme si, jak spolu tyto dve techniky souvisi a jaka dalsi pozorovani lze z teto souvislosti vyvodit. Prednaska nepredpoklada zadne specialni znalosti; vyjdeme ze zakladnich pojmu teorie automatu a formalni logiky. Zaverem naznacime mozna rozsireni prezentovanych vysledku.
1. 4. 2003: Prof. Milos Druckmuller, DrSc, VUT Brno; Vizualizace slunecni korony; Abstract: Zobrazení sluneční korony během úplného zatmění Slunce patří mezi technicky nejobtíľnějąí úkoly astronomické fotografie. Důvodem je extrémní rozdíl jasů mezi blízkými a vzdálenými částmi korony a velmi nízký kontrast koronálních struktur. Přednáąka se zabývá současnými moľnostmi zobrazení sluneční korony, které vyuľívají adaptivních filtrů.
8. 4. 2003: RNDr Petr Savicky CSc, UI AV CR, Praha; Rozhodovaci stromy a lesy pro analyzu dat; Abstract: Klasické statistické metody pro klasifikaci vícerozměrných dat vyľadují, aby data alespoň do určité míry splňovala předpoklady jako například gaussovský tvar jednotlivých tříd (LDA, QDA) nebo jejich lineární separovatelnost (logistická regrese). Pokud se data podstatným způsobem od těchto předpokladů odchylují a nepodaří se je transformovat tak, aby některý z těchto předpokladů splnila, pouľívají se neparametrické metody, jako například rozhodovací stromy, které patří do skupiny nejúspěąnějąích metod v této kategorii.
Přednáąka se bude věnovat experimentálním výsledkům, které se týkají rozhodovacích stromů ve dvou směrech:
Ukáľeme, ľe nahrazení běľně pouľívané heuristické minimalizace chyby na trénovací mnoľině (rekurzivní dělení) plnou optimalizací můľe vést jak ke zlepąení tak i ke zhorąení generalizační chyby v závislosti na konkrétní úloze. Otázka souvisí se základními principy strojového učení, protoľe minimalizace chyby modelu na trénovací mnoľině je základem převáľné větąiny metod analýzy dat.

Budou vysvětleny techniky, jak konstruovat klasifikátory tvořené větąím počtem stromů (klasifikační les) a budou ukázány výsledky srovnávací studie na simulovaných fyzikálních datech (rozliąování signálu a ąumu v nově budovaném gamma teleskopu MAGIC). Výhoda kombinovaných stromových klasifikátorů je na těchto datech zřetelná, a to i ve srovnání s metodami jiných typů.
15. 4. 2003: Prof. Roland Vollmar, University Karlsruhe; Informatics for visually ipaired people; Abstract: The Study Center for Blind and Visually Impaired Students at the University of Karlsruhe exists about ten years. It was founded with the aim to enable the study of Informatics (and other topics) to blind people, in accordance with the UNESCO Salamanca statement, that "every child has a fundamental right to education, and must be given an opportunity to achieve and maintain an acceptable level of learning".
During last ten years there were a lot of challenges but also some changes occurred, concerning the technical means to support our students and various presentations. In the talk our experiences will be described and analyzed.
22. 4. 2003: Prof. Frantisek Plasil, CSc, MFF UK, Praha; Getting ``whole picture'' behaviour from use cases; Abstract: Although widely used, traditional use case modeling does not provide explicit means to capture and test behavior compliance of the entities involved in a particular use case model. We introduce a simple formal model, called Generic UC View, which identifies important abstractions and relations upon them, which allow for reasoning on behavior compliance. We analyze textual UC modeling as an instance of Generic UC View and identify the missing relations. To provide a remedy, we introduce Pro-cases as another instance of Generic UC View, based on behavior protocols. Pro-cases feature all the relations required and provide for reasoning on behavioral compliance in component composition.
29. 4. 2003: Prof. Ludek Smolik, Uni Seigen; Nahodna cisla v kryptografii a jak na to; Abstract: Moderní kryptografické algoritmy se dnes testují v ąiroké odborné veřejnosti. Je to vąeobecně uznávaná praxe a tímto způsobem se zkoumá výkonnost a bezpečnost nových algoritmů. Nositelé tajemství jsou na druhé straně výhradně kryptografické klíče a patřičně opatrné je zacházení s nimi. Jedna z doslova klíčových otázek kryptografie je výroba zcela náhodných a nepředvídatelných klíčů nebo vąeobecněji náhodných čísel. Ne kaľdá dnes pouľitá metoda pro generování náhodných čísel je vhodná z pohledu poľadovaného stupně bezpečnosti. V přednáące bude představena metoda vyuľití nepředpověditelné povahy kvantových jevů jako kupř. okamľiku radioaktivního rozpadu. Kvantové jevy jsou dnes jediným známým a akceptovaným zdrojem pravé a ne-deterministické náhody a jsou vhodné pro realizaci zařízení na výrobu kryptografických klíčů nebo bitových posloupností nejvyąąího stupně důvěry.
6. 5. 2003: Dr. Ladislav Hluchy CSc, riaditel Ustavu informatiky SAV, Bratislava; Virtualna organizacia pre predpovedamie povodni; Abstract: Vyskyt povodni sposobuje mnozstvo materialnych skod ako aj straty na ludskych zivotoch. Zvlast nebezpecne su povodne, ktore sa objavia nahle, bez naleziteho varovania. Predpovedanie povodni je spojene s vypoctovo narocnym simulovanim meteorologickych, hydrologickych a hydraulickych problemov. Ustav informatiky SAV v ramci projektu "datA fusioN for Flood Analysis and decision Support-ANFAS, 5FP IST-1999-11676 (2000-03) riesil zlozite HPCN hydraulicke modelovanie zalozene na baze konecnych elementov a objemov. Hydraulicke modelovanie bolo validovane na casti povodia Vahu pri pouziti DTM a DSM modelov ziskanych pomocou LIDAR technologie. V sucasnosti UI SAV je zapojeny do projektu "Development of Grid Environment for Interactive Applications-CROSSGRID 5FP IST-2001-32243 (2002-05), v ramci ktoreho navrhol a implementoval kaskadnu simulaciu pozostavajucu z meteorologickeho predpovedania (velkost zrazok), hydrologickeho predpovedania (velkost prietokov) a hydraulickeho predpovedania (vyska a rychlost vody v zaplavenej oblasti). Hlavnym cielom tohto projektu je vybudovat virtualnu organizaciu prepajajucu jej relevantnych clenov. V mojom prispevku budu uvedene najdolezitejsie vysledky z oboch projektov.
13. 5. 2003: RNDr. Ivana Cerna CSc.; Model Checking: Approaches to the State Explosion Problem; Abstract: The demand of validation ensuring the correctness of the design is a major challenge in system development process and nowadays the need for effective verification techniques is critical. This need has given rise to what is commonly referred to as ``Formal Verification''. Specifically the model checking method has a number of advantageous over traditional approaches to this problem like simulation, testing, and deductive reasoning. Unfortunately, the model checking method has also a drawback: its performance is dependent on the size of the state space of the system and the number of states to explore can grow exponentially.
Alleviating the state explosion problem is a challenging area of research in model checking. We present an approach which makes use of a classification of properties to be verified and come up with two new distributed algorithms which effectively use the information about the type to speedup the verification process.
20. 5. 2003: Dr. Rudolf Hanka, Cambridge University, UK; Semantic context recognition for large scale medical image archive; Abstract: The demand for automatically recognising and retrieving medical images for screening, reference and management is growing faster than ever. This talk will describe an intelligent content-based image retrieval (CBIR) system that integrates both iconic and semantic content for histological image analysis. The system was jointly developed by the Medical Informatics Unit, Univ. of Cambridge and the Department of Computer Science, City University, Hong Kong. It combines low-level image processing technology with high-level semantic analysis of medical image content through different processing modules in the system architecture. Furthermore, as a by-product of semantic analysis, the system allows textual annotations to be generated for unknown images. As an image browser, apart from retrieving images by image example, the system also supports query by natural language.