|
|
Nástroj pro abstraktní regulární model checking
Chalk, Matěj ; Rogalewicz, Adam (oponent) ; Hruška, Martin (vedoucí práce)
Metody formální verifikace mohou poskytnout automatizované ověření korektnosti softwaru (stavěné na matematických základech), což je velmi důležité. Jednou z těchto metod je abstraktní regulární model checking, jenž používá konečné automaty a převodníky pro reprezentaci množiny dosažitelných konfigurací, respektive jednokrokového přechodu mezi těmito konfiguracemi. Přestože tato metoda řeší obecně nerozhodnutelné problémy, umožňuje terminaci v mnoha praktických případech a navíc výrazně zmírňuje problém stavové exploze. Tohoto dosahuje urychlením výpočtu dosažitelných stavů pomocí inkrementálního zjemňování abstrakcí, k odstranění neplatných protipříkladů vzniklých nadaproximací pak slouží technika zjemňování abstrakce založená na protipříkladech. Cílem této práce je vytvořit dobře navržený nástroj pro abstraktní regulární model checking, jenž byl dosud implementován pouze v prototypech. Nový nástroj bude systémy modelovat pomocí symbolických automatů a převodníků namísto jejich (méně stručných) klasických alternativ.
|
|
|
Improved Tools for Handling deltarpm Files
Chalk, Matěj ; Hruška, Martin (oponent) ; Vojnar, Tomáš (vedoucí práce)
RPM packages are used for software installation in Fedora. Every version of software packaged in this way corresponds to a separate RPM file. Updating software therefore entails downloading a large RPM file that is actually quite similar to the RPM already installed. An alternative for software updates is provided by DeltaRPM packages, which are special patch files that store the difference between two RPM files. An update then consists of downloading a much smaller file and applying this patch to the older version of the RPM. The deltarpm project defines the format of DeltaRPM files and supplies command-line tools for creating and applying them. However, this implementation is unsuitable for use as a library. The aim of this thesis is to create a new implementation of these tools, which is backwards compatible and provides a library for C developers that solves some of the weaknesses of the current implementation.
|
|
|
Nástroj pro abstraktní regulární model checking
Chalk, Matěj ; Rogalewicz, Adam (oponent) ; Hruška, Martin (vedoucí práce)
Metody formální verifikace mohou poskytnout automatizované ověření korektnosti softwaru (stavěné na matematických základech), což je velmi důležité. Jednou z těchto metod je abstraktní regulární model checking, jenž používá konečné automaty a převodníky pro reprezentaci množiny dosažitelných konfigurací, respektive jednokrokového přechodu mezi těmito konfiguracemi. Přestože tato metoda řeší obecně nerozhodnutelné problémy, umožňuje terminaci v mnoha praktických případech a navíc výrazně zmírňuje problém stavové exploze. Tohoto dosahuje urychlením výpočtu dosažitelných stavů pomocí inkrementálního zjemňování abstrakcí, k odstranění neplatných protipříkladů vzniklých nadaproximací pak slouží technika zjemňování abstrakce založená na protipříkladech. Cílem této práce je vytvořit dobře navržený nástroj pro abstraktní regulární model checking, jenž byl dosud implementován pouze v prototypech. Nový nástroj bude systémy modelovat pomocí symbolických automatů a převodníků namísto jejich (méně stručných) klasických alternativ.
|
|
|
Improved Tools for Handling deltarpm Files
Chalk, Matěj ; Hruška, Martin (oponent) ; Vojnar, Tomáš (vedoucí práce)
RPM packages are used for software installation in Fedora. Every version of software packaged in this way corresponds to a separate RPM file. Updating software therefore entails downloading a large RPM file that is actually quite similar to the RPM already installed. An alternative for software updates is provided by DeltaRPM packages, which are special patch files that store the difference between two RPM files. An update then consists of downloading a much smaller file and applying this patch to the older version of the RPM. The deltarpm project defines the format of DeltaRPM files and supplies command-line tools for creating and applying them. However, this implementation is unsuitable for use as a library. The aim of this thesis is to create a new implementation of these tools, which is backwards compatible and provides a library for C developers that solves some of the weaknesses of the current implementation.
|
host ::
RSS.