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, 2002. s. 262-267.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Using verified property to partition the state space in LTL model-checking
Autoři BARNAT, Jiří (203 Česká republika, garant).
Vydání Nantes, France, F. Cassez, C. Jard, F. Laroussinie, and M.D. Ryan (Eds.): Modelling and Verification of Parallel processes, s. 262-267, 2002.
Nakladatel IRCCyN, Ecole Centrale de Nantes
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Francie
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/02:00006604
Organizační jednotka Fakulta informatiky
Klíčová slova anglicky model-checking; distributed model-checking; verification
Štítky distributed model-checking, Model-Checking, verification
Změnil Změnil: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Změněno: 22. 11. 2006 16:01.
Anotace
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.
Návaznosti
GA201/00/1023, projekt VaVNázev: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů
Investor: Grantová agentura ČR, Standardní projekty
MSM 143300001, záměrNá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, Výzkumné záměry
VytisknoutZobrazeno: 28. 1. 2020 01:38