Designing Data-Parallel Graph Algorithms for Model Checking

Ověřování modelů (model checking) je rozšířená technika automatické formální verifikace softwarových a hardwarových systémů. Cílem této techniky je pro daný formální popis systému (konečně stavový model) a požadovanou vlastnost systematicky analyzovat graf všech dosažitelných konfigurací a rozhodnou...

Celý popis

Uloženo v:
Podrobná bibliografie
Hlavní autor: Češka, Milan, 1946- (Autor práce)
Další autoři: Brim, Luboš, 1952- (Vedoucí práce)
Typ dokumentu: VŠ práce nebo rukopis
Jazyk:Angličtina
Vydáno: 2012
Témata:
algoritmy (programování)
grafové algoritmy
počítačové modelování
computer algorithms
algorithms
computer modeling
graph algorithms
disertace
On-line přístup:http://is.muni.cz/th/99067/fi_d/
Obálka
LEADER 05431ctm a22008417a 4500
001 MUB01000719363
003 CZ BrMU
005 20140314104703.0
008 120613s2012 xr ||||| |||||||||||eng d
STA |a POSLANO DO SKCR  |b 2020-04-29 
035 |a (ISMU-VSKP)158615 
040 |a BOD114  |b cze  |d BOD018 
072 7 |a 004  |x Počítačová věda. Výpočetní technika. Informační technologie  |2 Konspekt  |9 23 
080 |a 004.94  |2 MRF 
080 |a 519.178  |2 MRF 
080 |a 004.421  |2 MRF 
100 1 |a Češka, Milan,  |d 1946-  |7 xx0008432  |% UČO 99067  |4 dis 
242 1 0 |a Designing Data-Parallel Graph Algorithms for Model Checking  |y eng 
245 1 0 |a Designing Data-Parallel Graph Algorithms for Model Checking  |h [rukopis] /  |c Milan Češka 
260 |c 2012 
300 |a vi, 113 s. 
500 |a Vedoucí práce: Luboš Brim 
502 |a Dizertace (Ph.D.)--Masarykova univerzita, Fakulta informatiky, 2012 
520 2 |a Ověřování modelů (model checking) je rozšířená technika automatické formální verifikace softwarových a hardwarových systémů. Cílem této techniky je pro daný formální popis systému (konečně stavový model) a požadovanou vlastnost systematicky analyzovat graf všech dosažitelných konfigurací a rozhodnout, zda systém tuto vlastnost splňuje či ne. Proces ověřování modelů typicky trpí tzv. problémem stavové exploze, který způsobuje, že grafy, které je nutno analyzovat, jsou pro skutečné systémy příliš velké. Z tohoto důvodu je efektivita fundamentálních grafových algoritmů (prohledávání do šířky, hledání nejkratších cest, rozklad na silně souvislé komponenty, detekce akceptujících cyklů, atd.), které tvoří základní stavební kameny pro techniky ověřování modelů, velmi důležitá. Nicméně výkonnost sekvenčních implementací těchto algoritmů se ukazuje nedostatečná pro zpracování extrémně velkých grafů. Tato skutečnost mimo jiné vedla k návrhu a implementaci paralelních grafových algoritmů, které j  |% cze 
520 2 9 |a Model checking is a wide-spread technique for automated formal verification of software and hardware systems. For a given formal description (finite-state model) of a system and desired system property, the goal of the model checking procedure is to systematically analyze a graph of all reachable configurations in order to decide whether the model satisfies the property or not. The model checking techniques generally suffer from the so-called state space explosion problem that causes the graphs to be very large for realistic systems. Therefore, the performance of fundamental graph algorithms (breadth-first search, shortest path detection, strongly connected component decomposition, accepting cycle detection, etc.) that form building blocks of the model checking algorithms is crucial. However, sequential implementations of these algorithms become impractical for extremely large graphs to be processed. As a result, parallel graph algorithms have been devised to efficiently use computer c  |9 eng 
655 7 |a disertace  |7 fd132024  |2 czenas 
658 |a Informatika (čtyřleté)  |b Informatika  |c FI D-IN4 IN (IN)  |2 CZ-BrMU 
650 0 7 |a algoritmy (programování)  |7 ph131788  |2 czenas 
650 0 7 |a grafové algoritmy  |7 ph770865  |2 czenas 
650 0 7 |a počítačové modelování  |7 ph124513  |2 czenas 
650 0 9 |a computer algorithms  |2 eczenas 
650 0 9 |a algorithms  |2 eczenas 
650 0 9 |a computer modeling  |2 eczenas 
650 0 9 |a graph algorithms  |2 eczenas 
700 1 |a Brim, Luboš,  |d 1952-  |7 ola2003206256  |% UČO 197  |4 ths 
710 2 |a Masarykova univerzita.  |b Fakulta informatiky  |7 kn20010709274  |4 dgg 
856 4 1 |u http://is.muni.cz/th/99067/fi_d/ 
CAT |c 20120613  |l MUB01  |h 0422 
CAT |a POSPEL  |b 02  |c 20120626  |l MUB01  |h 0801 
CAT |a HANAV  |b 02  |c 20120719  |l MUB01  |h 1021 
CAT |a BATCH  |b 00  |c 20130304  |l MUB01  |h 1427 
CAT |a POSPEL  |b 02  |c 20130530  |l MUB01  |h 0738 
CAT |a POSPEL  |b 02  |c 20130605  |l MUB01  |h 0736 
CAT |a POSPEL  |b 02  |c 20130821  |l MUB01  |h 0955 
CAT |a VESELA  |b 02  |c 20140314  |l MUB01  |h 1047 
CAT |c 20140911  |l MUB01  |h 1608 
CAT |c 20140912  |l MUB01  |h 1102 
CAT |c 20150703  |l MUB01  |h 1205 
CAT |c 20150901  |l MUB01  |h 1448 
CAT |c 20150921  |l MUB01  |h 1410 
CAT |a VACOVAX  |b 02  |c 20151012  |l MUB01  |h 1020 
CAT |a BATCH  |b 00  |c 20151226  |l MUB01  |h 0242 
CAT |a CERVINKOVX  |b 02  |c 20161120  |l MUB01  |h 1024 
CAT |c 20170301  |l MUB01  |h 1214 
CAT |c 20200429  |l MUB01  |h 1339 
CAT |c 20210614  |l MUB01  |h 0959 
CAT |c 20210614  |l MUB01  |h 1948 
CAT |a BATCH  |b 00  |c 20210724  |l MUB01  |h 1214 
CAT |a REPISOVA  |b 02  |c 20211111  |l MUB01  |h 1525 
CAT |c 20220114  |l MUB01  |h 1647 
CAT |a POSPEL  |b 02  |c 20230919  |l MUB01  |h 2149 
CAT |a POSPEL  |b 02  |c 20230919  |l MUB01  |h 2149 
M53 0 |a formální verifikace 
M53 0 |a paralelní ověřování modelů 
M53 0 |a datově paralelní grafové algoritmy 
M53 0 |a grafické výpočetní jednotky; formal verification 
M53 0 |a parallel model checking 
M53 0 |a data-parallel graph algorithms 
M53 0 |a graphics processing units 
LOW |a POSLANO DO SKCR  |b 2020-04-29 
994 - 1 |l MUB01  |l MUB01  |m VYSPR  |1 FI  |a Fakulta informatiky  |3 Diz. práce 2012  |5 42005D2620  |8 20140313  |f 72  |f Týdenní  |r 20140313 
AVA |a INF50  |b FI  |d Diz. práce 2012  |e available  |t K dispozici  |f 1  |g 0  |h N  |i 0 

Podobné jednotky