D 2003

Distributed Explicit Bounded LTL Model Checking

KRČÁL, Pavel

Základní údaje

Originální název

Distributed Explicit Bounded LTL Model Checking

Autoři

KRČÁL, Pavel

Vydání

89. vyd. Neuveden, Second International Workshop on Parallel and Distributed Model Checking, s. 30-47, 2003

Nakladatel

Elsevier

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

není předmětem státního či obchodního tajemství

Odkazy

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/03:00008587

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

Distributed Algorithms; LTL Model Checking; Bounded Model Checking

Štítky

Změněno: 26. 5. 2004 13:27, Mgr. Pavel Krčál

Anotace

V originále

Automated formal verification becomes a significant part of an industrial design process. Favourite formal verification method - model checking - is strongly limited by the size of the model of the verified system. It suffers from the so called state explosion problem. We propose to fight this problem by applying the idea of bounding the examined state space in explicit model checking. Moreover, we combine this approach with the distribution of the computation among the network of workstations. We consider several distributed bounded LTL model checking algorithms and carry out a series of experiments to evaluate them and to compare their behaviour.

Návaznosti

GA201/03/0509, projekt VaV
Název: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů
MSM 143300001, záměr
Název: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů