Cluster-Based LTL Model Checking of Large Systems
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. 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 | Nizozemské království |
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 VaV | Název: Automatizovaná verifikace softwaru |
Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru | |
GD102/05/H050, projekt VaV | Název: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů |
Investor: Grantová agentura ČR, Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů | |
MSM0021622419, záměr | Název: Vysoce paralelní a distribuované výpočetní systémy |
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy | |
1ET408050503, projekt VaV | Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů |
Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů | |
1M0545, projekt VaV | Název: Institut Teoretické Informatiky |
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky |
VytisknoutZobrazeno: 12. 10. 2024 19:48