| BARNAT, Jiří. Using verified property to partition the state space in LTL model-checking. In F. Cassez, C. Jard, F. Laroussinie, and M.D. Ryan (Eds.): Modelling and Verification of Parallel processes. Nantes, France: IRCCyN, Ecole Centrale de Nantes. s. 262-267. 2002. |
Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{406263,
author = {Barnat, Jiří},
address = {Nantes, France},
booktitle = {F. Cassez, C. Jard, F. Laroussinie, and M.D. Ryan (Eds.): Modelling and Verification of Parallel processes},
keywords = {model-checking; distributed model-checking; verification},
language = {eng},
location = {Nantes, France},
pages = {262-267},
publisher = {IRCCyN, Ecole Centrale de Nantes},
title = {Using verified property to partition the state space in LTL model-checking},
year = {2002}
}
TY - JOUR
ID - 406263
AU - Barnat, Jiří
PY - 2002
TI - Using verified property to partition the state space in LTL model-checking
PB - IRCCyN, Ecole Centrale de Nantes
CY - Nantes, France
KW - model-checking
KW - distributed model-checking
KW - verification
N2 - We propose a distributed algorithm for model-checking LTL formulas that works on a network of workstations and effectively uses the decomposition of the formula automaton to strongly connected components to achieve more efficient distribution of the verification problem. In particular, we explore the possibility of performing a distributed nested depth-first search algorithm.
ER -
BARNAT, Jiří. Using verified property to partition the state space in LTL model-checking. In \textit{F. Cassez, C. Jard, F. Laroussinie, and M.D. Ryan (Eds.): Modelling and Verification of Parallel processes}. Nantes, France: IRCCyN, Ecole Centrale de Nantes. s.~262-267. 2002.
|
