Ne (7321)
Počet nalezených dokumentů:
7321
Publikováno od
do
Bezpečnostní rizika senzorů v mobilních zařízeních
Henclová, Kateřina; Polčák, Libor; Hranický, Radek
2024 - anglický
Tato práce představuje hrozby pro mobilní bezpečnost a soukromí, které představují mobilní senzory. Představuje rozhraní Generic Sensor API, mobilní senzory a způsoby jejich zneužití. Pomocí mobilních senzorů, jako je akcelerometr, gyroskop a magnetometr, tato práce demonstruje takový útok na mobilní senzory v prohlížeči. Zvoleným útokem je rozpoznávání aktivity, které provádí predikci aktivit pomocí strojového učení se slibnými výsledky a předpovídá správnou třídu aktivit přibližně v 69% případů napříč všech tříd. Pozornost je věnována také rozšíření JShelter a tomu, zda poskytuje ochranu před nežádoucím odhalením senzorů. This work presents the threats to mobile security and privacy exposed by mobile sensors. It introduces the Generic Sensor API, the mobile sensors, and ways they can be misused. Using the mobile sensors like the accelerometer, gyroscope and magnetometer, this work demonstrates such an attack on mobile sensors in the browser. The chosen attack is activity recognition, which performs its activity prediction using machine learning with promising results, predicting the correct activity class approximately 69% of the time across all classes. Focus is also given to the JShelter extension, and whether it provides protection against unwanted sensor exposure.
Klíčová slova:
Mobile sensors; Cybersecurity; Privacy; JShelter; Generic Sensor API; JavaScript; Activity recognition; Machine learning; Accelerometer; Gyroscope; Magnetometer; Mobilní senzory; kyberbezpečnost; soukromí; JShelter; Generic Sensor API; JavaScript; rozpoznávání aktivity; strojové učení; akcelerometr; gyroskop; magnetometr
Plné texty jsou dostupné v digitálním repozitáři NUŠL
Bezpečnostní rizika senzorů v mobilních zařízeních
Tato práce představuje hrozby pro mobilní bezpečnost a soukromí, které představují mobilní senzory. Představuje rozhraní Generic Sensor API, mobilní senzory a způsoby jejich zneužití. Pomocí mobilních ...
Vliv výrazů obličeje na 3D rozpoznávání podle obličeje.
Kováč, Peter; Goldmann, Tomáš; Pleško, Filip
2024 - anglický
Bakalárska práca "Vplyv výrazov tváre na rozpoznávanie tváre v 3D" sa zameriava na štúdium vplyvu výrazov tváre na presnosť rozpoznávania tváre v 3D. Prvé kapitoly skúmajú rôzne techniky 3D modelovania a ich využitie vrátane 3D morfovateľných modelov (3DMM), modelov blendshape a metód založených na neurónových sieťach ako FLAME (Faces Learned with an Articulated Model and Expressions). Práca následne predstavuje nový prístup k rekonštrukcii 3D modelov tvárí z 2D obrázkov a navrhuje hodnotiaci rámec na meranie vplyvu zmien výrazov tváre na rozpoznávanie tváre v 3D. Experimentálne výsledky ukazujú, ako rôzne výrazy, ako napríklad hnev, radosť a strach, ovplyvňujú presnosť rozpoznávania. Zistenia tejto práce prispievajú k hlbšiemu pochopeniu úlohy výrazov tváre v rozpoznávaní tváre v 3D a navrhujú možné zlepšenia na zvýšenie presnosti rozpoznávacích systémov. The thesis "The impact of facial expressions on 3D face recognition" focuses on studying the effect of facial expressions on the accuracy of 3D face recognition. The first chapters explore various 3D modeling techniques and their applications, including 3D Morphable Models (3DMMs), blendshape models, and neural network-based methods like FLAME (Faces Learned with an Articulated Model and Expressions). The thesis then presents a new approach for reconstructing 3D face models from 2D images and proposes an evaluation framework to measure the impact of facial expression changes on 3D face recognition. Experimental results demonstrate how different expressions, such as anger, happiness, and fear, influence recognition accuracy. The findings of this work contribute to a deeper understanding of facial expressions’ role in 3D face recognition and propose potential improvements for enhancing recognition systems.
Klíčová slova:
3D face recognition; facial expressions; 3D Morphable Models; blendshape models; FLAME; DECA; landmark detection; 3D modeling; facial animation; 3D rozpoznávanie tvárí; výrazy tváre; 3D morfovateľné modely; modely blendshape; FLAME; DECA; detekcia bodov; 3D modelovanie; animácia tváre
Plné texty jsou dostupné v digitálním repozitáři NUŠL
Vliv výrazů obličeje na 3D rozpoznávání podle obličeje.
Bakalárska práca "Vplyv výrazov tváre na rozpoznávanie tváre v 3D" sa zameriava na štúdium vplyvu výrazov tváre na presnosť rozpoznávania tváre v 3D. Prvé kapitoly skúmajú rôzne techniky 3D ...
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ý ...
Řízení aktivních prvků LEGO Technic z prostředí EV3
Blaško, Daniel; Polčák, Libor; Hranický, Radek
2024 - anglický
LEGO Mindstorms je populárna rada programovateľných kociek s rozsiahlou sadou funkcií, ktorá už 25 rokov pomáha učiť deti základy robotiky a počítačových vied, a ktorá sa teší širokej komunitnej podpore. Cieľom tejto bakalárskej práce je vytvoriť hardvérové a softvérové riešenia, ktoré zlepšia kompatibilitu medzi kockou Mindstorms EV3 a ostatnými motorizovanými LEGO súčiastkami, s primárnym zameraním sa na produktovú radu Power Functions. V rámci tejto práce boli v rôznych iteráciách vytvorené radiče, ktoré rozširujú možnosti kocky EV3 ovládať motory, s použitím vlastných návrhov dizajnov plošných spojov a 3D tlačených puzdier. Okrem nich boli vyvinuté softvérové kódovacie bloky, ktoré umožňujú kocke komunikovať s týmito radičmi a ďalšími UART zariadeniami. LEGO Mindstorms is a popular series of programmable bricks with an advanced set of functionality, which has been helping children learn the basics of robotics and computer science for 25 years and which enjoys wide community support. The goal of this bachelor's thesis is to provide hardware and software solutions to enhance the compatibility between the LEGO Mindstorms EV3 intelligent brick and other motorized LEGO parts, primarily focusing on the Power Functions product line. In this thesis, I will create motor drivers in several iterations that broaden the capabilities of the EV3 brick to control a large number of motors, using my designs for printed circuit boards and 3D-printed enclosures. Additionally, I will develop software code blocks for the EV3 that allow it to communicate with the aforementioned drivers, as well as other UART devices.
Klíčová slova:
LEGO; LEGO Mindstorms EV3; EV3-G Blocks; LEGO Power Functions; microcontroller; Arduino; ESP; motor driver; I2C; UART; printed circuit board; LEGO; LEGO Mindstorms EV3; EV3-G Bloky; LEGO Power Functions; mikrokontrolér; Arduino; ESP; motorový radič; I2C; UART; plošný spoj
Plné texty jsou dostupné v digitálním repozitáři NUŠL
Řízení aktivních prvků LEGO Technic z prostředí EV3
LEGO Mindstorms je populárna rada programovateľných kociek s rozsiahlou sadou funkcií, ktorá už 25 rokov pomáha učiť deti základy robotiky a počítačových vied, a ktorá sa teší širokej komunitnej ...
Potlačení šumu v rentgenových snímcích s využitím hlubokého učení
Říhová, Barbora; Jakubíček, Roman; Zemek, Marek
2024 - anglický
Technologie zobrazování pomocí rentgenových paprsků je základem zkoumání vnitřní struktury velké škály objektů a výsledky mohou být právě kvůli šumu kompromitovány. Tato práce se zabývá odstraňováním šumu v rentgenových projekcích pomocí hlubokého učení, které má schopnost adaptovat se na konkrétní problém. Práce obsahuje teoretickou rešerši zaměřenou na oblasti produkce a detekce rentgenových paprsků, šumu v rentgenových snímcích a neuronových sítí. Speciální kapitola je věnována popisu vybraného řešení, které je provedeno pomocí tvorby datasetu složeného z části z modelovaných rentgenových projekcí s následně implementovaným šumem odpovídající modelu v reálných snímcích a částečně ze sérií rentgenových projekcí získaných ze zařízení Rigaku nano3DX. K implementaci byla vybrána architektura konvoluční neuronové sítě RIDNet, vzhledem k tomu, že poskytuje v oblasti redukce šumu dobré výsledky. Byly natrénovány tři modely s použitím různých částí datasetu. Nejlepší výkon byl pozorován u modelů, u kterých byla při trénování použita reálná data. Jejich účinnost je srovnatelná s tradičními metodami jako BM3D. X-ray imaging technology is the foundation for exploring the internal structure of a wide range of objects, however the results can be compromised by noise. This thesis is focused on the removal of noise in X-ray projections using deep learning, that has the capability to adapt to a specific task. The thesis contains a theoretical investigation focusing on the areas of X-ray production and detection, noise in X-ray images, and neural networks. A special chapter is devoted to the description of the chosen solution, which is performed by creating a dataset partially consisting of modeled X-ray projections with the subsequent incorporation of noise corresponding to noise model in real images and partly from X-ray projection series. The RIDNet convolutional neural network architecture was selected for implementation, since it shows good result for denoising task. Three models were trained using different parts of the dataset. The best performance was observed for models, that used real data for training. Their performance is comparable to traditional methods such as BM3D.
Klíčová slova:
X-ray imaging; deep learning; noise; denoising; convolutional neural networks; rentgenové zobrazování; hluboké učení; šum; odstraňování šumu; konvoluční neuronové sítě
Plné texty jsou dostupné v digitálním repozitáři NUŠL
Potlačení šumu v rentgenových snímcích s využitím hlubokého učení
Technologie zobrazování pomocí rentgenových paprsků je základem zkoumání vnitřní struktury velké škály objektů a výsledky mohou být právě kvůli šumu kompromitovány. Tato práce se zabývá odstraňováním ...
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 ...
Driver krokového motoru se zpětnou vazbou pro polohovací platformu
Doležel, Michael; Král, Vojtěch; Barcík, Peter
2024 - anglický
Tato bakalářská práce se zabývá návrhem a stavbou uzavřené regulační soustavy pro výšku a azimut optomechanické platformy. Cílem je porovnat rotační senzory a následně navrhnout kontroler pro krokový motor. Prototyp regulačního systému byl postaven s využitím platformy Arduino, řadiče krokového motoru DRV8825, krokového motoru NEMA-17 a hallového senzoru AEAT-9922 pro měření rotace. Prototyp dokáže otáčet krokovým motorem s rozlišením 0.056°, což je maximální přesnost řadiče DRV8825 při použití mikrokrokování 1/32. Deska finálního řadiče byla přepracována tak, aby zahrnovala rozhraní SPI-4 pro hallový senzor AEAT-9922. Deska obsahuje řadič krokového motoru L6470H s mikrokrokováním 1/128 a má rozlišení 0.014°. This bachelor's thesis deals with designing and building a closed-loop control system for the altitude and azimuth axis of an opto-mechanical platform. The goal is to compare rotation sensors, and then design a driver for the stepper motor. The control system prototype was built using the Arduino platform, DRV8825 motor driver, NEMA-17 stepper motor, and AEAT-9922 hall effect rotational sensor. The prototype can rotate the stepper motor with a resolution of 0.056° which is the maximal accuracy of the DRV8825 driver with 1/32 microstepping mode. The board of the final driver was redesigned to include the SPI-4 interface for the AEAT-9922 hall sensor. This driver includes an L6470H stepper motor driver with 1/128 microstepping mode. This final board has a resolution of 0.014°.
Klíčová slova:
AEAT-9922; Arduino; capacitive encoder; DRV8825; Hall-effect sensor; L6470H; magnetic encoder; microstepping; NEMA 17; optical encoder; Opto-mechanical platform; potentiometer; resolver; rotatory sensor; rotation; RS-485; SPI-4; stepper motor; STM32F303K6; AEAT-9922; Arduino; kapacitní enkodér; DRV8825; Hallův senzor; L6470H; magnetický enkodér; mikrokrokování; NEMA 17; optický enkodér; optomechanická platforma; potenciometr; resolver; rotační senzor; rotace; RS-485; SPI-4; krokový motor; STM32F303K6
Plné texty jsou dostupné v digitálním repozitáři NUŠL
Driver krokového motoru se zpětnou vazbou pro polohovací platformu
Tato bakalářská práce se zabývá návrhem a stavbou uzavřené regulační soustavy pro výšku a azimut optomechanické platformy. Cílem je porovnat rotační senzory a následně navrhnout kontroler pro krokový ...
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 ...
Nasazení a licencování aplikace na GitHub Packages
Misskii, Anton; Ilgner, Petr; Kohout, David
2024 - anglický
Práce se zaměřuje na platformu pro verzování GitHub, konkrétně na její službu GitHub Packages. Cílem je automatizovat proces sestavení ukázkové Java aplikace pomocí grafického rozhraní JavaFX a nástroje Maven na platformě GitHub. To zahrnuje nasazení na GitHub Packages a zajištění, aby bylo možné aplikaci efektivně aktualizovat. Kromě toho musí aplikace obsahovat systém pro verzování a licencování k ochraně softwaru. Dalším klíčovým cílem je popsání a implementace modulárního systému, který byl zaveden v Java 9, který nabízí rozšířené možnosti pro vývoj a distribuci aplikací. Implementací těchto systémů a nasazením aplikace na GitHub Packages projekt sleduje vytvoření komplexní metodologie pro vývoj moderních aplikací, integraci bezpečnostních systémů, udržování spolehlivého systému verzování aplikací a kontinuální doručování a distribuci aplikací prostřednictvím populárních služeb. The work focuses on the versioning platform GitHub, specifically its GitHub Packages service. The goal is to automate the build process of a demo JavaFX application using the JavaFX graphical interface and the Maven tool on the GitHub platform. This includes deployment on GitHub Packages and ensuring the application can be updated efficiently. Additionally, the application must incorporate a system for versioning and licensing to protect the software. Another key objective is to describe and implement the modular Java system introduced in Java 9, which offers enhanced possibilities for application development and distribution. By implementing these systems and deploying the application on GitHub Packages, the project aims to create a comprehensive methodology for developing modern applications, integrating security systems, maintaining a reliable application versioning system, and continuously delivering and distributing applications through popular services.
Klíčová slova:
Application delivering and distribution practices; Application versioning resolution; GitHub Actions; GitHub Packages; GitHub Services; Java Platform Module System; Licensing models; Praxe dodávání a distribuce aplikací; Řešení verzování aplikací; GitHub Actions; GitHub Packages; GitHub služby; Java Platform Module System; Licenční modely
Plné texty jsou dostupné v digitálním repozitáři NUŠL
Nasazení a licencování aplikace na GitHub Packages
Práce se zaměřuje na platformu pro verzování GitHub, konkrétně na její službu GitHub Packages. Cílem je automatizovat proces sestavení ukázkové Java aplikace pomocí grafického rozhraní JavaFX a ...
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