B 2000

Distributed LTL Model-Checking in SPIN

BARNAT, Jiří, Luboš BRIM a Jitka STŘÍBRNÁ

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 Česká republika), Luboš BRIM (203 Česká republika) a Jitka STŘÍBRNÁ (203 Česká republika)

Vydání

Brno, 16 s. Technical Reports, 2000

Nakladatel

FI MU

Další údaje

Jazyk

čeština

Typ výsledku

Odborná kniha

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

není předmětem státního či obchodního tajemství

Odkazy

Kód RIV

RIV/00216224:14330/00:00002823

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

model-checking; verification; verification tool

Štítky

Změněno: 26. 5. 2004 15:45, prof. RNDr. Jiří Barnat, Ph.D.

Anotace

ORIG EN

V originále

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.

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 VaV
Název: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů
Investor: Grantová agentura ČR, Algoritmy a nástroje pro praktickou verifikaci souběžných systémů
MSM 143300001, záměr
Ná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, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů