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.

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

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

---

Anotace

V originále

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.

Č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