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...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2012
|
| Témata: | |
| On-line přístup: | http://is.muni.cz/th/99067/fi_d/ |
| Shrnutí: | 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 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 |
|---|---|
| Popis jednotky: | Vedoucí práce: Luboš Brim |
| Fyzický popis: | vi, 113 s. |