|
|
Automatizace verifikace pomocí neuronových sítí
Fajčík, Martin ; Husár, Adam (oponent) ; Zachariášová, Marcela (vedoucí práce)
Úlohou tejto práce je analýza a riešenie optimalizačných problémov vychádzajúcich z automatizácie funkčnej verifikácie hardvéru pomocou umelých neurónových sietí. Verifikácia ľubovoľného integrovaného obvodu (Design Under Verification, DUV) pomocou techniky verifikácie riadenej pokrytím (Coverage-Driven Verification) a metodiky UVM (Universal Verification Methodology) prebieha tak, že do DUV sú zasielané vstupné stimuly, pri ktorých verifikačné prostredie monitoruje percentuálne pokrytie DUV pomocou predom určenej špecifikácie sledovaných vlastností. Pokrytím v tomto kontexte myslíme merateľnú vlastnosť DUV, ako napríklad počet overených aritmetických operácií, či počet aktivovaných riadkov kódu. Na základe dosiahnutej veľkosti pokrytia a stanovenej špecifikácie je možné prehlásiť DUV za zverifikovaný. Súčasným trendom v automatizácii funkčnej verifikácie hardvéru je pseudonáhodné generovanie vstupných stimulov s obmedzeniami (constraints) pomocou techniky constrained-random stimulus generation. V tejto práci sa preto zaoberáme ovládaním pseudonáhodného generátoru stimulov (PNG), pričom obmedzenia pre generátor sú ovládané externým prostriedkom a to konkrétne neurónovou sieťou. Využívame tak vlastnosti neurónových sietí pre riešenie optimalizačných problémov vhodné pre prehľadávanie stavového priestoru pokrytia DUV. Riešenými optimalizačnými problémami sú priebežná úprava obmedzení PNG takým spôsobom, aby došlo k čo najrýchlejšiemu zverifikovaniu DUV a hľadanie najmenšej množiny stimulov takej, že táto množina zverifikuje DUV. Kvalitatívne vlastnosti navrhnutých riešení sú overené na 32-bitových aplikačne špecifických procesoroch (ASIPs) s názvom Codasip uRISC a Codix Cobalt.
|
|
|
Comparison of the determination of hormones (Follicle stimulating hormone, Luteinizing hormone, Prolactin, Testosterone, Progesteron) by two analytical systems. Converting accredited method and its verification.
Kucejová, Soňa ; Martínková, Markéta (vedoucí práce) ; Mrízová, Iveta (oponent)
Analytický systém ARCHITEC i2000SR bol verifikovaný podľa požiadaviek laboratória ÚLBLD VFN a 1. LF UK v Prahe. Ako výkonnostné parametre verifikácie analytických postupov pre testosterón, progesterón, luteinizačný hormón, folikuly stimulujúci hormón a prolaktín boli vyhodnotené opakovateľnosť, medziľahlá precíznosť a neistota merania. Namerané výsledky kontrolných vzoriek Lyphochek sa zhodovali s hodnotami, ktoré uviedol výrobca. Opakovateľnosť: variačné koeficienty testosterónu pre Lyphochek 1 6,81%, pre Lyphochek 3 6,40%, progesterónu 2,4% a 1,8%, luteinizačného hormónu 5,38% a 1,89%, folikuly stimulujúceho hormónu 5,12% a 3,24%, prolaktínu 1,45% a 1,83%. Medziľahlá precíznosť: variačné koeficienty testosterónu pre Lyphochek 1 6,02%, Lyphochek 2 3,60%, Lyphochek 3 3,07%, progesterónu 7,9%, 4,9% a 5,8%, luteinizačného hormónu 4,50%, 5,51% a 5,83%, folikuly stimulujúceho hormónu 4,00%, 3,72% a 4,87%, prolaktínu 4,60%, 4,20% a 5,00%. Neistota merania: testosterón 6,02%, progesterón 7,9%, luteinizačný hormón 5,83%, folikuly stimulujúci hormón 4,87%, prolaktín 5,00%. Analytický systém ARCHITECT i2000SR bol porovnaný s dovtedy používaným systémom ADVIA Centaur, aby sa zistilo či je možné previesť metódy Centaur Testosterón, Progesterón, Luteinizačný hormón, Folikuly stimulujúci hormón a Prolaktín na systém...
|
|
|
Visualization and verification of plans
Glinský, Radoslav ; Barták, Roman (vedoucí práce) ; Dvořák, Filip (oponent)
Názov: Vizualizácia a verifikácia plánov Autor: Radoslav Glinský Katedra: Katedra teoretickej informatiky a matematickej logiky Vedúci bakalárskej práce: Doc. RNDr. Roman Barták, Ph.D. Abstrakt: Analýza plánov je dôležitou sú as ou kompletných plánovacích systémov. Aby smeč ť umožnili užívate omľ orientovať sa aj vo vä ších plánoch, vytvorili sme program, ktorý pomáha s analýzou ač vizualizáciou plánov. Program sa volá VisPlan - Interactive Visualization and Verification of Plans. VisPlan je neoddelite nouľ sú as ouč ť bakalárskej práce, ke že prakticky implementuje jej vizualiza né aď č verifika né riešenia. VisPlan nachádza a zobrazuječ kauzálne väzby medzi akciami, identifikuje možné chyby v pláne (a tak overuje jeho korektnos ), zvýraz uje nájdenéť ň chyby v pláne a umož ujeň užívate om interaktívne modifikova plán, a teda opravi chyby v pláne alebo ho jednoducho vylepši .ľ ť ť ť K úľ ovč é slová: Plánovanie, Umelá inteligencia, PDDL, Verifikácia
|
host ::
RSS.