BARNAT, Jiří, Luboš BRIM a Ivana ČERNÁ. Cluster-Based LTL Model Checking of Large Systems. In Formal Methods for Components and Objects. Berlin: Springer, 2006. s. 259-279, 21 s. ISBN 978-3-540-36749-9.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Cluster-Based LTL Model Checking of Large Systems
Název česky LTL ověřování modelu rozsáhlých systémů s využitím počítačových klastrů
Autoři BARNAT, Jiří (203 Česká republika), Luboš BRIM (203 Česká republika, garant) a Ivana ČERNÁ (203 Česká republika).
Vydání Berlin, Formal Methods for Components and Objects, od s. 259-279, 21 s. 2006.
Nakladatel Springer
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Nizozemsko
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/06:00015451
Organizační jednotka Fakulta informatiky
ISBN 978-3-540-36749-9
UT WoS 00240360000013
Klíčová slova anglicky distributed LTL model checking
Štítky distributed LTL model checking
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Změněno: 23. 6. 2009 09:57.
Anotace
In recent years a bundle of parallel and distributed algorithms for verification of finite state systems has appeared. We survey distributed memory enumerative LTL model checking algorithms designed for networks of workstations communicating via MPI. The automata-based approach to LTL model checking reduces the model checking problem to the accepting cycle detection problem. Contrary to sequential algorithms, distributed algorithms cannot rely on depth-first search postorder which is essential for efficient cycle detection. Therefore, they have to employ diverse conditions that characterize the existence of cycles in a graph in order to come up with an efficient and practical solution. We compare these algorithms both theoretically and experimentally and determine cases where particular algorithms can be useful.
Anotace česky
Přehledová práce shrnující výzkum v oblasti paralelního a distribuovaného ověřování modelu formulemi lineární temporální logiky. Jednotlivé algoritmy jsou teoreticky ale i experimentálně porovnány.
Návaznosti
GA201/06/1338, projekt VaVNázev: Automatizovaná verifikace softwaru
Investor: Grantová agentura ČR, Standardní projekty
GD102/05/H050, projekt VaVNázev: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Doktorské granty
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
1ET408050503, projekt VaVNázev: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Informační společnost (Národní program výzkumu)
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: 24. 1. 2020 11:50