Ne (2991)
Použitá omezení
(3)
Počet nalezených dokumentů:
2991
Publikováno od
do
Automatická komprese vah neuronových sítí
Lorinc, Marián; Sekanina, Lukáš; Mrázek, Vojtěch
2024 - anglický
Konvolučné neurónové siete (CNN) od svojho vynájdenia zrevolucionizovali spôsob, akým sa realizujú úlohy z odvetvia počítačového videnia. Vynález CNN viedol k zníženiu pamäťovej náročnosti, keďže váhy boli nahradené konvolučnými filtrami obsahujúcimi menej trénovateľných váh. Avšak, toto zníženie bolo dosiahnuté na úkor zvýšenia požiadaviek na výpočtový výkon, ktorý je naviazaný na výpočet konvolúcie. Táto práca skúma hypotézu, či je možné sa vyhnúť načítavaniu váh a miesto toho ich vypočítať, čím sa ušetrí energia. Na otestovanie tejto hypotézy bol vyvinutý nový algoritmus kompresie váh využívajúci Kartézske genetické programovanie. Tento algoritmus hľadá najoptimálnejšiu funkciu kompresie váh s cieľom zvýšiť energetickú účinnosť. Experimenty vykonané na architektúrach LeNet-5 a MobileNetV2 ukázali, že algoritmus dokáže efektívne znížiť spotrebu energie pri zachovaní vysokej presnosti modelu. Výsledky ukázali, že určité vrstvy je možné doplniť vypočítanými váhami, čo potvrdzuje potenciál pre energeticky efektívne neurónové siete. Convolutional Neural Networks (CNNs) have revolutionised computer vision field since their introduction. By replacing weights with convolution filters containing trainable weights, CNNs significantly reduced memory usage. However, this reduction came at the cost of increased computational resource requirements, as convolution operations are more computation intensive. Despite this, memory usage remains more energy-intensive than computation. This thesis explores whether it is possible to avoid loading weights from memory and instead functionally calculate them, thereby saving energy. To test this hypothesis, a novel weight compression algorithm was developed using Cartesian Genetic Programming. This algorithm searches for the most optimal weight compression function, aiming to enhance energy efficiency without compromising the functionality of the neural network. Experiments conducted on the LeNet-5 and MobileNetV2 architectures demonstrated that the algorithm could effectively reduce energy consumption while maintaining high model accuracy. The results showed that certain layers could benefit from weight computation, validating the potential for energy-efficient neural network implementations.
Klíčová slova:
Convolutional Neural Networks; CNN; Evolutionary Algorithms; EA; Genetic Algorithms; GA; Cartesian Genetic Programming; CGP; Optimization; Compression; MobileNetV2; LeNet-5; Energy Efficiency; Weight Compression Algorithm; Deep Learning; Konvolučné neurónové siete; CNN; Evolučné algoritmy; EA; Genetické algoritmy; GA; Kartézske genetické programovanie; CGP; Optimalizácia; Kompresia; MobileNetV2; LeNet-5; Energetická účinnosť; Kompresia váh; Hlboké učenie
Plné texty jsou dostupné v digitálním repozitáři NUŠL
Automatická komprese vah neuronových sítí
Konvolučné neurónové siete (CNN) od svojho vynájdenia zrevolucionizovali spôsob, akým sa realizujú úlohy z odvetvia počítačového videnia. Vynález CNN viedol k zníženiu pamäťovej náročnosti, keďže váhy ...
Distribuovaný systém potlačení DoS útoků
Beneš, Dalibor; Žádník, Martin; Šišmiš, Lukáš
2024 - anglický
Ochrana před distribuovanými útoky odepření služby (DDoS) patří mezi klíčové oblastí síťové bezpečnosti. Jednou z možných forem ochrany je využití zařízení DCPro DDoS Protector vyvíjeného sdružením CESNET. Sdružení CESNET provozuje také systémy pro monitorování a analýzu síťového provozu IPFIXcol2 a NEMEA, a dále poskytuje možnost využít protokol pro monitorování sítě sFlow. Cílem této práce je navrhnout a uskutečnit integraci těchto systémů a vytvořit tak efektivní systém potlačení útoků odepření služby. Při vypracování tohoto cíle byl kladen důraz na efektivní využití stávajích řešení, znovupoužitelnost a možnosti budoucího rozšíření celé distribuované architektury. Protection against distributed denial of service (DDoS) attacks is one of the key areas of network security. One of the forms of defence is to use the DCPro DDoS Protector device developed by the CESNET association. The CESNET association also utilizes network monitoring and traffic analysis systems IPFIXcol2 and NEMEA, as well as the network monitoring protocol sFlow. The aim of this thesis was to propose and realize the integration of those systems, so that an effective distributed system for the mitigation of DDoS attacks could be created. During the work on this task, special focus was given to the effective utilization of existing solutions, reusability and the option for a future expansion of the distributed architecture.
Klíčová slova:
DCPro DDoS Protector; NEMEA; IPFIXcol; IPFIX; sFlow; NetFlow; CESNET; DoS; DDoS; network security; network data analysis; network monitoring; DDoS attack mitigation; DCPro DDoS Protector; NEMEA; IPFIXcol; IPFIX; sFlow; NetFlow; CESNET; DoS; DDoS; síťová bezpečnost; analýza síťových dat; monitorování sítě; potlačení DDoS útoků
Plné texty jsou dostupné v digitálním repozitáři NUŠL
Distribuovaný systém potlačení DoS útoků
Ochrana před distribuovanými útoky odepření služby (DDoS) patří mezi klíčové oblastí síťové bezpečnosti. Jednou z možných forem ochrany je využití zařízení DCPro DDoS Protector vyvíjeného sdružením ...
Robotický manipulátor s využitím RC komponentů a serv
Liška, Jakub; Nosko, Svetozár; Zemčík, Pavel
2024 - anglický
Cieľom tejto diplomovej práce bolo vytvorenie vlatného robotického manipulátoru, s pou-\\žitím RC(diaľkovo ovládaných) komponentov a servomotorov. V rámci riešenia bolo potre-\\bné robotický manipulátor vybaviť senzorikou, ktorá umožnuje detekciu kolízii s okolím a zabezpečuje tak bezpečnosť obsluhy v pracovnom priestore manipulátoru. Robotický manipilátor je taktiež vybavený absolútnimi enkódermi pre snímanie polohy jednotlivých kĺbov, akcelerometrom a senzormi pre meranie záťaží pôsobiacich na jednotlivé kĺby. O pohyb ramena sa starajú štandardné krokové motory. Samotné telo robotického manipulátoru bolo navrhnuté s ohľadom na jednotlivé komponenty a je možné ho vyrobiť pomocou 3D tlače. Súčastou riešenia je aj užívateľské rozhranie, pomocou ktorého je možné robotické rameno ovládať. The aim of this thesis was to create a valid robotic manipulator, using RC(radio control) components and servomotors. As part of the solution, it was necessary to equip the robotic manipulator with sensors that enable the detection of collisions with the environment and thus ensure the safety of the operator in the working area of the manipulator. The robotic manipulator is also equipped with absolute encoders for sensing the position of individual joints, an accelerometer and sensors for measuring the loads acting on individual joints. Standard stepper motors take care of the arm movement. The body of the robotic manipulator itself has been designed with the individual components in mind and can be fabricated using 3D printing. The solution also includes a user interface that can be used to control the robotic arm.
Klíčová slova:
robotic manipulator; robotic arm; collision detection; stepper motor; kinematics; 3D printing; off-shelf components; RC components; sensors; development boards; robotický manipulátor; robotické rameno; detekcia kolízii; krokový motor; kinematika; 3D tlač; off-shelf komponenty; RC komponenty; senzory; vývojové dosky
Plné texty jsou dostupné v digitálním repozitáři NUŠL
Robotický manipulátor s využitím RC komponentů a serv
Cieľom tejto diplomovej práce bolo vytvorenie vlatného robotického manipulátoru, s pou-\\žitím RC(diaľkovo ovládaných) komponentov a servomotorov. V rámci riešenia bolo potre-\\bné robotický ...
Bezpečnostní analýza vybraného Android TV Boxu
Švenk, Adam; Veigend, Petr; Tamaškovič, Marek
2024 - anglický
Popularita TV boxov so systémom Android v poslednom čase výrazne vzrástla. Okrem toho, že ponúkajú širokú škálu funkcií, je čoraz aktuálnejšia otázka, či sú dostatočne zabezpečené a chránené. Táto práca popisuje komplexnú bezpečnostnú analýzu vybraného Android TV boxu, ktorá zahŕňa hardvérové aj softvérové komponenty. Skúmaním zraniteľností prítomných v zariadení sa táto práca zameriava na identifikáciu potenciálnych rizík pre súkromie a bezpečnosť používateľov. Okrem toho navrhuje odporúčania na zmiernenie týchto zraniteľností. The popularity of Android TV boxes has increased significantly in recent times. In addition to offering a wide range of functionality, the question of whether they are adequately secured is becoming increasingly pertinent. This thesis performs a comprehensive security analysis of selected Android TV boxes, covering both the hardware and software components. By examining the vulnerabilities present in the device, this thesis aims to identify potential risks to user privacy and security. Additionally, it proposes recommendations to mitigate these vulnerabilities.
Klíčová slova:
security analysis; Android; Android TV; OWASP; vulnerability; firmware; reverse engineering; bezpečnostná analýza; Android; Android TV; OWASP; zraniteľnosť; firmvér; reverzné inžinierstvo
Plné texty jsou dostupné v digitálním repozitáři NUŠL
Bezpečnostní analýza vybraného Android TV Boxu
Popularita TV boxov so systémom Android v poslednom čase výrazne vzrástla. Okrem toho, že ponúkajú širokú škálu funkcií, je čoraz aktuálnejšia otázka, či sú dostatočne zabezpečené a chránené. Táto ...
Aligning pre-trained models for spoken language translation
Sedláček, Šimon; Beneš, Karel; Kesiraju, Santosh
2024 - anglický
Tato práce zkoumá nový end-to-end přístup k překladu mluveného jazyka (ST) využívající předtrénovaných modelů pro přepis řeči (ASR) a strojový překlad (MT), propojené malým spojovacím modulem (Q-Former, STE). Ten má za úkol překlenout mezeru mezi modalitami řeči a textu mapováním embedding reprezentací ASR enkodéru do latentního prostoru reprezentací MT modelu. Během trénování jsou zvolené ASR a MT model zmrazeny, laděny jsou pouze parametry spojovacího modulu. Trénování a evaluace jsou prováděny na datasetu How2, obsahujícím ST data z Angličtiny do Portugalštiny. V našich experimentech zjišťujeme, že většina sladěných systémů překonává referenční kaskádový ST systém, přičemž využívají stejné základní modely. Navíc, při zachování konstantní a ve srovnání malé (10M parametrů) velikosti spojovacího modulu, větší a silnější ASR a MT modely univerzálně zlepšují výsledky překladu. Zjišťujeme, že spojovací moduly mohou také sloužit jako doménové adaptéry pro zvolené základní systémy, kdy významně zlepšují výsledky překladu ve sladěném ST prostředí, a to i oproti holému MT výkonu daného MT modelu. Nakonec navrhujeme proceduru pro předtrénování spojovacího modulu s potenciálem snížit množství ST dat potřebných pro trénink obdobných sladěných systémů. In this work, we investigate a novel approach to end-to-end speech translation (ST) by leveraging pre-trained models for automatic speech recognition (ASR) and machine translation (MT) and connecting them with a small connector module (Q-Former, STE). The connector bridges the gap between the speech and text modalities, transforming the ASR encoder embeddings into the latent representation space of the MT encoder. During training, the foundation ASR and MT models are frozen, and only the connector parameters are tuned, optimizing for the ST objective. We train and evaluate our models on the How2 English to Portuguese ST dataset. In our experiments, aligned systems outperform our cascade ST baseline while utilizing the same foundation models. Additionally, while keeping the size of the connector module constant and small in comparison (10M parameters), increasing the size and capability of the ASR encoder and MT decoder universally improves translation results. We find that the connectors can also serve as domain adapters for the foundation models, significantly improving translation performance in the aligned ST setting, compared even to the base MT scenario. Lastly, we propose a pre-training procedure for the connector, with the potential for reducing the amount of ST data required for training similar aligned systems.
Klíčová slova:
spoken language translation; speech translation; model alignment; automatic speech recognition; machine translation; transfer learning; transformers; Q-Former; domain adaptation; překlad mluveného jazyka; překlad řeči; sladění modelů; automatické rozpoznávání řeči; strojový překlad; transfer learning; transformery; Q-Former; doménová adaptace
Plné texty jsou dostupné v digitálním repozitáři NUŠL
Aligning pre-trained models for spoken language translation
Tato práce zkoumá nový end-to-end přístup k překladu mluveného jazyka (ST) využívající předtrénovaných modelů pro přepis řeči (ASR) a strojový překlad (MT), propojené malým spojovacím modulem ...
Generování syntetického webového provozu
Koprda, Peter; Žádník, Martin; Hranický, Radek
2024 - anglický
Web crawlers, známi aj ako webové pavúky alebo roboty, zohrávajú kľúčovú úlohu pri vyhľadávaní informácií, optimalizácii pre vyhľadávače a indexovaní webových stránok. Weboví roboti sa však môžu používať aj pri penetračnom testovaní webových aplikácií. Automatizácia procesu odhaľovania zraniteľností, identifikácia skrytých koncových bodov a efektívne mapovanie štruktúry webovej aplikácie môžu zvýšiť účinnosť penetračného testovania. Táto práca sa zameriava na vytvorenie nástroja určeného na generovanie neľudskej (syntetickej) webovej prevádzky. Tento nástroj bude určený aj na automatizované penetračné testovanie webových aplikácií pomocou webových robotov s využitím syntetickej webovej prevádzky na rozšírenie možností testovania. Okrem toho sa tento nástroj bude používať na hodnotenie účinosti bezpečnostných systémov, ako sú IDS, IPS a webové aplikačné firewally (WAF). Web crawlers, also known as web spiders or bots, play a crucial role in information retrieval, search engine optimization, and website indexing. However, web robots can also be used in the penetration testing of web applications. Automating the vulnerability discovery process, identifying hidden endpoints, and effectively mapping the structure of a web application can improve the effectiveness of penetration testing. This work focuses on creating a tool designed for generating non-human (synthetic) web traffic. This tool will also be designed for automated penetration testing of web applications using web robots, using synthetic web traffic for enhanced testing capabilities. Additionally, this tool will be used for evaluating the effectiveness of security systems such as IDS, IPS, and web application firewalls (WAF).
Klíčová slova:
web crawler; web application; vulnerability; OWASP Top 10; penetration testing; web crawler; webová aplikácia; zraniteľnosť; OWASP Top 10; penetračné testovanie
Plné texty jsou dostupné v digitálním repozitáři NUŠL
Generování syntetického webového provozu
Web crawlers, známi aj ako webové pavúky alebo roboty, zohrávajú kľúčovú úlohu pri vyhľadávaní informácií, optimalizácii pre vyhľadávače a indexovaní webových stránok. Weboví roboti sa však môžu ...
Návrh superskalárního RISC-V procesoru
Salvet, Dominik; Šimek, Václav; Jaroš, Jiří
2024 - anglický
Tato práce se zabývá návrhem a implementací superskalární mikroarchitektury RISC-V procesoru zaměřené na prostředí s omezenými zdroji. Za tímto účelem mikroarchitektura definuje sedmistupňovou zřetězenou linku s dvojitým vydáváním instrukcí, které vykonává v pořadí. Je popsána v jazyce SystemVerilog a lze ji snadno simulovat na počítači. Pomocí připravených nástrojů pouští vytvořený model procesoru programy napsané v RISC-V jazyce symbolických adres zkompilované GCC. Na základě provedeného testování bez speciální asistence kompilátoru procesor provede v průměru 0,88 instrukcí za cyklus, čímž poskytuje o 22,6 % vyšší výkon než jeho skalární protějšek. Vzhledem k tomu, že se navržená mikroarchitektura také vyhýbá nadměrné specializaci, poskytuje dobrý základ, který lze dále rozšiřovat a optimalizovat na základě profilování očekávaných programů, což vede k optimálnímu výkonu a využití zdrojů. This thesis deals with designing and implementing a superscalar RISC-V processor microarchitecture focused on environments with constrained resources. For that, the microarchitecture exposes a dual-issue seven-stage pipeline with in-order instruction execution. It is described in SystemVerilog and can be easily simulated on a computer. Using prepared tools, the created processor model runs RISC-V assembly programs compiled by GCC. Based on conducted testing without special compiler assistance, the processor executes 0.88 instructions per cycle on average, providing 22.6 % higher performance than its scalar counterpart. Considering that the microarchitecture also avoids unnecessary specialization, it provides a good base that can be further extended and optimized based on the profiling of expected programs, leading to optimal performance and use of resources.
Klíčová slova:
Superscalar processor; RISC-V instruction set; instruction pipelining; in-order execution; dual-issue architecture; open-source hardware; SystemVerilog; simulation testbench; Superskalární procesor; instrukční sada RISC-V; zřetězené zpracování; vykonávání instrukcí v pořadí; dvojité vydávání instrukcí; otevřený hardware; SystemVerilog; simulační testbench
Plné texty jsou dostupné v digitálním repozitáři NUŠL
Návrh superskalárního RISC-V procesoru
Tato práce se zabývá návrhem a implementací superskalární mikroarchitektury RISC-V procesoru zaměřené na prostředí s omezenými zdroji. Za tímto účelem mikroarchitektura definuje sedmistupňovou ...
Využití zpětnovazebné učení a induktivní syntézy pro konstukci robustních kontroléru v POMDPs
Hudák, David; Holík, Lukáš; Češka, Milan
2024 - anglický
Jednou ze současných výzev při sekvenční rozhodováním je práce s neurčitostí, která je způsobena nepřesnými senzory či neúplnou informací o prostředích, ve kterých bychom chtěli dělat rozhodnutí. Tato neurčitost je formálně popsána takzvanými částečně pozorovatelnými Markovskými rozhodovacími procesy (POMDP), které oproti Markovským rozhodovacím procesům (MDP) nahrazují informaci o konkrétním stavu nepřesným pozorováním. Pro rozhodování v takových prostředích je nutno nějakým způsobem odhadovat současný stav a obecně tvorba optimálních politik v takových prostředích není rozhodnutelná. K vyrovnání se s touto výzvou existují dva zcela odlišné přístupy, kdy lze k problému přistupovat úplnými formálními metodami, a to buď s pomocí výpočtu beliefů či syntézou konečně stavových kontrolérů, nebo metodami založenými na nepřesné aproximaci současného stavu, reprezentované především hlubokým zpětnovazebným učením. Zatímco formální přístupy jsou schopné dělat verifikovatelná a robustní rozhodnutí pro malá prostředí, tak zpětnovazebné učení je schopné škálovat na reálné problémy. Tato práce se pak soustředí na spojení těchto dvou odlišných přístupů, kdy navrhuje různé metody jak pro interpretaci výsledku, tak pro vzájemné předávání nápověd. Experimenty v této práci ukazují, že z této symbiózy mohou těžit oba přístupy, ale také že zvolený přístup ke trénování agentů už sám o sobě řádově překonává současné systémy pro trénování agentů na podobných úlohách. A significant challenge in sequential decision-making involves dealing with uncertainty, which arises from inaccurate sensors or only a partial knowledge of the agent's environment. This uncertainty is formally described through the framework of partially observable Markov decision processes (POMDPs). Unlike Markov decision processes (MDP), POMDPs only provide limited information about the exact state through imprecise observations. Decision-making in such settings requires estimating the current state, and generally, achieving optimal decisions is not tractable. There are two primary strategies to address this issue. The first strategy involves formal methods that concentrate on computing belief MDPs or synthesizing finite state controllers, known for their robustness and verifiability. However, these methods often struggle with scalability and require to know the underlying model. Conversely, informal methods like reinforcement learning offer scalability but lack verifiability. This thesis aims to merge these approaches by developing and implementing various techniques for interpreting and integrating the results and communication strategies between both methods. In this thesis, our experiments show that this symbiosis can improve both approaches, and we also show that our implementation overcomes other RL implementations for similar tasks.
Klíčová slova:
Reinforcement learning; PAYNT; POMDP; interpretability; synthesis; PPO; sequential decision problems; finite state controllers; FSC; DQN; DDQN; Posilované učení; PAYNT; POMDP; interpretovatelnost; syntéza; PPO; sekvenční rozhodovací problémy; konečně stavové kontroléry; FSC; DQN; DDQN
Plné texty jsou dostupné v digitálním repozitáři NUŠL
Využití zpětnovazebné učení a induktivní syntézy pro konstukci robustních kontroléru v POMDPs
Jednou ze současných výzev při sekvenční rozhodováním je práce s neurčitostí, která je způsobena nepřesnými senzory či neúplnou informací o prostředích, ve kterých bychom chtěli dělat rozhodnutí. Tato ...
Vliv AI nástrojů na kvalitu a bezpečnost kódu
Vinarčík, Peter; Holop, Patrik; Malinka, Kamil
2024 - anglický
Táto práca predstavuje novovytvorenú aplikáciu, ktorá je schopná vykonávať large scale výskum pre hodnotenie bezpečnosti a kvality kódu generovaného AI. Tiež bol predstavený nový spôsob vyhodnocovania bezpečnosti kódu generovaného AI, za využitia MITRE's metodológie v kombinácii so SAST toolmi vykonávajúcimi statickú analýzu nad kódom. Aplikácia je navyše rozšírená o vylepšeného AI chatbota, ktorého výstup je obohatený o výsledky statickej analýzy v čase generovania. Užívateľ vloží dataset promptov do aplikácie, a v prípade, že bol pre určitý prompt vygenerovaný kód so zraniteľnosťou, je táto zraniteľnosť ohodnotená zavedenou metodológiou a užívateľ dostáva informáciu nie len o tom, že kód je zraniteľný, ale ako veľmi. Súčasťou riešenia je aj oproti existujúcim výskumom veľké, pilotné testovanie popularných AI ako ChatGPT-4 či Gemini, nad datasetom promptov s využitím novej aplikácie. Výsledky ukázali dominanciu ChatGPT-4 bežiacom na modeli GPT-4, oproti ostatným testovaným AI. This work presents a newly developed application that is able to perform fully automated large-scale research for evaluating the safety and quality of AI-generated code. Also, a new way of evaluating the safety of AI-generated code has been presented, utilizing MITRE's methodology in combination with SAST tools performing static analysis on the code. In addition, the application is enhanced with an improved AI chatbot whose output is enhanced with the results of static analysis at generation time. The user inputs a dataset of prompts into the application, and if code with a vulnerability has been generated for a particular prompt, that vulnerability is scored by the established methodology, and the user is informed not only that the code is vulnerable, but how vulnerable it is. As part of the solution, large-scale, pilot testing of popular AIs, such as ChatGPT-4 or Gemini, is performed over a dataset of prompts using the new application, in contrast to existing studies. The results showed the dominance of ChatGPT-4 running on the GPT-4 model, over the other AIs tested.
Klíčová slova:
generative AI; llm; security; cybersecurity; static analysis; sast; bandit; semgrep; codeql; chatgpt; gpt; gemini; copilot; generatívna umelá inteligencia; llm; bezpečnosť; kyberbezpečnosť; statická analýza; sast; bandit; semgrep; codeql; chatgpt; gpt; gemini; copilot
Plné texty jsou dostupné v digitálním repozitáři NUŠL
Vliv AI nástrojů na kvalitu a bezpečnost kódu
Táto práca predstavuje novovytvorenú aplikáciu, ktorá je schopná vykonávať large scale výskum pre hodnotenie bezpečnosti a kvality kódu generovaného AI. Tiež bol predstavený nový spôsob vyhodnocovania ...
Automaty ve verifikaci
Šmahlíková, Barbora; Holík, Lukáš; Lengál, Ondřej
2024 - anglický
Regulární model checking je technika pro verifikaci nekonečněstavových systémů založená na automatech. Konfigurace systému jsou dány konečným automatem a přechody mezi nimi konečným převodníkem. Algoritmus pro verifikaci libovolných vlastností parametrických systémů specifikovaných v temporální logice LTL(MSO) již existuje. V této práci představíme rozšíření tohoto algoritmu, které umožňuje verifikaci hypervlastností parametrických systémů, tedy vlastností, ve kterých lze explicitně kvantifikovat nad několika cestami v systému. Specifikujeme podmínky, které musí platit pro dvojici tzv. advice bitů (složené z konečného automatu a konečného převodníku), která slouží jako svěděk toho, že je daná vlastnost v systému splněna. Algoritmus představený v této práci je implementovaný v nástroji ParaHyper - jediném existujícím nástroji pro verifikaci hypervlastností parametrických systémů. Tento nástroj využívá SAT solveru pro generování automatů a převodníků. Pokud je nalezen takový pár, který vyhovuje podmínkám pro advice bity, vlastnost je v systému splněna. Bylo provedeno experimentální vyhodnocení představeného algoritmu a bylo zjištěno, že ParaHyper je schopen generovat advice bity pro formule s abecedou až o 4 symbolech, pokud mají automat i převodník nejvýše 2 stavy. Pokud jsou však automat i převodník zadány uživatelem, ParaHyper umí efektivně zkontrolovat, zda vyhovují podmínkám i v případě větších abeced a většího počtu stavů. Regular model checking is an automata-based technique used for verification of infinite-state systems. The configurations of a system are encoded as a finite automaton and transitions between these configurations as a finite transducer. A technique for verifying arbitrary properties of parameterized systems specified in a temporal logic LTL(MSO) has already been introduced. We present an extension of this algorithm allowing verification of hyperproperties of parameterized systems where an explicit quantification over multiple execution traces is allowed. We specify conditions that need to hold for a pair of advice bits (a finite automaton and a finite transducer) that serves as a witness of the fact that the property holds in the system. The technique presented in this work is implemented in our tool ParaHyper - the only existing tool for the verification of hyperproperties of parameterized systems. The tool uses a SAT solver to generate automata and transducers. If a pair satisfying the conditions for advice bits is found, the property holds in the system. We performed an experimental evaluation of our approach and found that ParaHyper is able to generate advice bits for formulae with an alphabet up to 4 symbols if both the automaton and the transducer have at most 2 states. When a candidate pair is given by the user, ParaHyper can, however, efficiently check if it satisfies the conditions for advice bits even for larger alphabets and greater number of states.
Klíčová slova:
regular model checking; hyperproperties; automata; verification; parameterized systems; regulární model checking; hypervlastnosti; automaty; verifikace; parametrizované systémy
Plné texty jsou dostupné v digitálním repozitáři NUŠL
Automaty ve verifikaci
Regulární model checking je technika pro verifikaci nekonečněstavových systémů založená na automatech. Konfigurace systému jsou dány konečným automatem a přechody mezi nimi konečným převodníkem. ...
NUŠL poskytuje centrální přístup k informacím o šedé literatuře vznikající v ČR v oblastech vědy, výzkumu a vzdělávání. Více informací o šedé literatuře a NUŠL najdete na webu služby.
Vaše náměty a připomínky posílejte na email nusl@techlib.cz
Provozovatel
Zahraniční báze