BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. Parallel Partial Order Reduction with Topological Sort Proviso. In Software Engineering and Formal Methods (SEFM 2010). Los Alamos: IEEE Computer Society Press, 2010. s. 222-231, 10 s. ISBN 978-0-7695-4153-2.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Parallel Partial Order Reduction with Topological Sort Proviso
Název česky Paralelní redukce částečného uspořádání s využitím topologického třídění
Autoři BARNAT, Jiří (203 Česká republika, garant, domácí), Luboš BRIM (203 Česká republika, domácí) a Petr ROČKAI (703 Slovensko, domácí).
Vydání Los Alamos, Software Engineering and Formal Methods (SEFM 2010), od s. 222-231, 10 s. 2010.
Nakladatel IEEE Computer Society Press
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Itálie
Utajení není předmětem státního či obchodního tajemství
Forma vydání tištěná verze "print"
Kód RIV RIV/00216224:14330/10:00045912
Organizační jednotka Fakulta informatiky
ISBN 978-0-7695-4153-2
Klíčová slova česky LTL ověřování modelu; Redukce čístečného uspořádání; Paralelní a distribuované výpočty; DiVinE
Klíčová slova anglicky LTL Model Checking; Partial Order Reduction; Parallel and Distributed Processing; DiVinE
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Petr Ročkai, Ph.D., učo 139761. Změněno: 18. 2. 2013 12:44.
Anotace
Partial order reduction and distributed-memory processing are the two essential techniques to fight the wellknown state space explosion problem in explicit state model checking. Unfortunately, these two techniques have not been integrated yet to a satisfactory degree. The main source of difficulties is the cycle proviso that requires one fully expanded state on every cycle in the reduced state space graph. In this paper we suggest a new technique that guarantees correct construction of the reduced state space graph w.r.t. the cycle proviso. Our new technique is fully compatible with the parallel graph traversal procedure while at the same time it provides competitive reduction of the state space if compared to the serial case. The new technique has been implemented within the parallel and distributed-memory LTL model checker DIVINE and its performance is reported in this paper.
Anotace česky
Redukce částečného uspořádání a počítáni v distribuované paměti jsou dvě klíčové techniky pro boj se stavovou explozí v kontextu enumerativní verifikace. Hlavním výsledkem této práce je nový paralelní algoritmus pro výpočet množiny vrcholů pokrývající všechny cykly v grafu, který umožňuje uspokojivou integraci obou klíčových technik. Nová technika byla implementována v rámci nástroje DiVinE.
Návaznosti
GA201/09/1389, projekt VaVNázev: Verifikace a analýza velmi velkých počítačových systémů
Investor: Grantová agentura ČR, Standardní projekty
GP201/09/P497, projekt VaVNázev: Automatizovaná formální verifikace s využitím soudobého hardware
Investor: Grantová agentura ČR, Postdoktorské projekty
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
MUNI/A/0914/2009, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV)
Investor: Masarykova univerzita, Grantová agentura MU, Kategorie A - Specifický výzkum - Studentské výzkumné projekty
1M0545, projekt VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumná centra (Národní program výzkumu)
VytisknoutZobrazeno: 23. 1. 2020 00:44