BARNAT, Jiří, Luboš BRIM a Jitka STŘÍBRNÁ. Distributed LTL Model-Checking in SPIN. Brno: FI MU, 2000. 16 s. Technical Reports.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Distributed LTL Model-Checking in SPIN
Název anglicky Distributed LTL Model-Checking in SPIN
Autoři BARNAT, Jiří (203 Česko), Luboš BRIM (203 Česko) a Jitka STŘÍBRNÁ (203 Česko).
Vydání Brno, 16 s. Technical Reports, 2000.
Nakladatel FI MU
Další údaje
Originální jazyk čeština
Typ výsledku Odborná kniha
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Česko
Utajení není předmětem státního či obchodního tajemství
WWW URL
Kód RIV RIV/00216224:14330/00:00002823
Organizační jednotka Fakulta informatiky
Klíčová slova anglicky model-checking; verification; verification tool
Štítky Model-Checking, verification, verification tool
Změnil Změnil: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Změněno: 26. 5. 2004 15:45.
Anotace
In this paper we propose a distributed algorithm for model-checking LTL formulas in SPIN. In particular, we explores the possibility of performing nested depth first search algorithm in distributed SPIN. A distributed version of the algorithm is presented, and its complexity is discussed. Some preliminary experimental results are summarised.
Anotace anglicky
In this paper we propose a distributed algorithm for model-checking LTL formulas in SPIN. In particular, we explores the possibility of performing nested depth first search algorithm in distributed SPIN. A distributed version of the algorithm is presented, and its complexity is discussed. Some preliminary experimental results are summarised.
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: 5. 7. 2020 04:19