Distributed Explicit Bounded LTL Model Checking

Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

KRČÁL Pavel

Rok publikování 2003
Druh Článek ve sborníku
Konference Second International Workshop on Parallel and Distributed Model Checking
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www http://www.elsevier.nl/gej-ng/31/29/23/141/47/27/89.1.005.ps
Obor Informatika
Klíčová slova Distributed Algorithms; LTL Model Checking; Bounded Model Checking
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.