Distributed state space reductions
Fundamentální problém formální verifikace, takzvaný problém stavové exploze, již byl řešen mnoha způsoby. Dvě skupiny přístupů jsou redukce stavových prostorů a použití paralelních nebo distribuovaných algoritmů. Zatímco se techniky v první skupině snaží zmenšit objem nutně vykonané práce (bezpečným...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2008.
|
| Témata: | |
| On-line přístup: | http://is.muni.cz/th/39589/fi_d/ |
| Shrnutí: | Fundamentální problém formální verifikace, takzvaný problém stavové exploze, již byl řešen mnoha způsoby. Dvě skupiny přístupů jsou redukce stavových prostorů a použití paralelních nebo distribuovaných algoritmů. Zatímco se techniky v první skupině snaží zmenšit objem nutně vykonané práce (bezpečným zmenšením odpovídajících stavových prostorů), techniky z druhé skupiny používají k řešení daného problému více zdrojů (počítačů ap.). Přestože jsou techniky z uvedených skupin často komplementární, kombinaci metod z první a druhé skupiny bylo zatím věnováno pouze málo pozornosti. Důvodem může být to, že používání redukcí stavových prostorů často zahrnuje řešení problémů které lze jen obtížně řešit paralelně. Předkládaná disertační práce se proto zaměřuje na kombinaci redukčních technik a verifikace v distribuovaném prostředí. Jmenovitě navrhuje efektivní distribuované algoritmy pro generování redukovaných stavových prostorů. Práce se zabývá třemi redukcemi: partial order reduction (redukce . As long as the state space explosion problem occurs in formal verification, plenty of attempts have been proposed to alleviate the problem. Two groups of such attempts are state space reductions and parallel/distributed verification. While the first group tries to shrink an amount of work necessary to be done (be reducing the corresponding state space), the second approach employs more resources to solve the problem. Despite complementarity of the approaches, only a little work has been done trying to combine them. This is probably reasoned by the fact that applying state space reductions often involves solving problems which are hard to be parallelised. The thesis focuses on a combination of reduction techniques and distributed verification, namely it proposes efficient distributed algorithms for generation of reduced state spaces. The thesis concerns about three state space reductions: partial order reduction (p.o.r.), tau-compression reduction and symmetry reduction. The chapter re. |
|---|---|
| Popis jednotky: | Vedoucí práce: Luboš Brim. |
| Fyzický popis: | viii,129 s. |