Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{489717,
author = {Krčál, Pavel},
address = {Neuveden},
booktitle = {Second International Workshop on Parallel and Distributed Model Checking},
edition = {89},
keywords = {Distributed Algorithms; LTL Model Checking; Bounded Model Checking},
language = {eng},
location = {Neuveden},
pages = {30-47},
publisher = {Elsevier},
title = {Distributed Explicit Bounded LTL Model Checking},
url = {http://www.elsevier.nl/gej-ng/31/29/23/141/47/27/89.1.005.ps},
year = {2003}
}
TY - JOUR
ID - 489717
AU - Krčál, Pavel
PY - 2003
TI - Distributed Explicit Bounded LTL Model Checking
PB - Elsevier
CY - Neuveden
KW - Distributed Algorithms
KW - LTL Model Checking
KW - Bounded Model Checking
UR - http://www.elsevier.nl/gej-ng/31/29/23/141/47/27/89.1.005.ps
N2 - 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.
ER -
KRČÁL, Pavel. Distributed Explicit Bounded LTL Model Checking. In \textit{Second International Workshop on Parallel and Distributed Model Checking}. 89. vyd. Neuveden: Elsevier, 2003, s.~30-47.
|
