LTL ověřování modelu rozsáhlých systémů s využitím počítačových klastrů

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F06%3A00015451" target="_blank" >RIV/00216224:14330/06:00015451 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Cluster-Based LTL Model Checking of Large Systems

Popis výsledku v původním jazyce

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. Theautomata-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.

Název v anglickém jazyce

Cluster-Based LTL Model Checking of Large Systems

Popis výsledku anglicky

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. Theautomata-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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2006

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Formal Methods for Components and Objects

ISBN

978-3-540-36749-9

ISSN

—

e-ISSN

—

Počet stran výsledku

21

Strana od-do

—

Název nakladatele

Springer

Místo vydání

Berlin

Místo konání akce

Amsterdam

Datum konání akce

1. 1. 2006

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

00240360000013