Distributed Explicit Bounded LTL Model Checking

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

KRČÁL Pavel

Year of publication 2003
Type Article in Proceedings
Conference Second International Workshop on Parallel and Distributed Model Checking
MU Faculty or unit

Faculty of Informatics

Citation
Web http://www.elsevier.nl/gej-ng/31/29/23/141/47/27/89.1.005.ps
Field Informatics
Keywords Distributed Algorithms; LTL Model Checking; Bounded Model Checking
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.