Hlavní stránka > Výsledky hledání: Yuldashev, Nodir
Hledej:
Tipy pro vyhledávaní :: Rozšířené hledání
Hledej ve sbírkách:
Seřadit podle: Zobrazit výsledky: Výstupní formát:
Národní úložiště šedé literatury Nalezeno 2 záznamů.  Hledání trvalo 0.02 vteřin. 
Using Java PathFinder for Construction of Abstractions of Java Programs
 Yuldashev, Nodir ; Parízek, Pavel (vedoucí práce) ; Poch, Tomáš (oponent)
S rostoucí složitostí moderních softwarových systémů se jejich verifikace stává velmi obtížnou úlohou. Techniky formální verifikace a analýzy slouží k nalezení chyb v kódu nebo pro prokázání, že kód splňuje určité vlastnosti. Populární technika automatické verifikace je model checking, který využívá procházení stavového prostoru. Nicméně model checking je náchylný k problému exponenciálního nárustu počtu stavů (state explosion) a proto nemůže být použit pro složité vícevláknové softwarové systémy. Obecné řešení tohoto problému (state explosion) spočívá ve vytvoření abstrakce cílového systému a následném použití tohoto modelu k verifikaci. V rámci diplomové práce jsme navrhli a implementovali nástroj pro konstrukci abstrakce Java komponent v jazyce behavior protocol, který využívá model checker Java PathFinder pro procházení stavového prostoru. Výsledky experimentů na několika netriviálních komponentách ukazují, že nástroj může být použit v praxi.
Úplný záznam
Using Java PathFinder for Construction of Abstractions of Java Programs
 Yuldashev, Nodir ; Poch, Tomáš (oponent) ; Parízek, Pavel (vedoucí práce)
S rostoucí složitostí moderních softwarových systémů se jejich verifikace stává velmi obtížnou úlohou. Techniky formální verifikace a analýzy slouží k nalezení chyb v kódu nebo pro prokázání, že kód splňuje určité vlastnosti. Populární technika automatické verifikace je model checking, který využívá procházení stavového prostoru. Nicméně model checking je náchylný k problému exponenciálního nárustu počtu stavů (state explosion) a proto nemůže být použit pro složité vícevláknové softwarové systémy. Obecné řešení tohoto problému (state explosion) spočívá ve vytvoření abstrakce cílového systému a následném použití tohoto modelu k verifikaci. V rámci diplomové práce jsme navrhli a implementovali nástroj pro konstrukci abstrakce Java komponent v jazyce behavior protocol, který využívá model checker Java PathFinder pro procházení stavového prostoru. Výsledky experimentů na několika netriviálních komponentách ukazují, že nástroj může být použit v praxi.
Úplný záznam

Chcete být upozorněni, pokud se objeví nové záznamy odpovídající tomuto dotazu?
Přihlásit se k odběru RSS.
Digitální repozitář :: Hledej :: Nový záznam :: Personalizace :: Nápověda
Powered by Invenio v1.1.2
Spravuje admin.invenio@techlib.cz
Tato stránka je dostupná také v následujících jazycích:
Česky  English