BARNAT, Jiří, Luboš BRIM and Jitka STŘÍBRNÁ. Distributed LTL Model-Checking in SPIN. Brno: FI MU, 2000, 16 pp. Technical Reports. |
Other formats:
BibTeX
LaTeX
RIS
|
Basic information | |
---|---|
Original name | Distributed LTL Model-Checking in SPIN |
Name (in English) | Distributed LTL Model-Checking in SPIN |
Authors | BARNAT, Jiří (203 Czech Republic), Luboš BRIM (203 Czech Republic) and Jitka STŘÍBRNÁ (203 Czech Republic). |
Edition | Brno, 16 pp. Technical Reports, 2000. |
Publisher | FI MU |
Other information | |
---|---|
Original language | Czech |
Type of outcome | Book on a specialized topic |
Field of Study | 10201 Computer sciences, information science, bioinformatics |
Country of publisher | Czech Republic |
Confidentiality degree | is not subject to a state or trade secret |
WWW | URL |
RIV identification code | RIV/00216224:14330/00:00002823 |
Organization unit | Faculty of Informatics |
Keywords in English | model-checking; verification; verification tool |
Tags | Model-Checking, verification, verification tool |
Changed by | Changed by: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Changed: 26/5/2004 15:45. |
Abstract |
---|
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. |
Abstract (in English) |
---|
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. |
Links | |
---|---|
GA201/00/1023, research and development project | Name: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů |
Investor: Czech Science Foundation, Algorithms and tools for practical verification of concurrent systems. | |
MSM 143300001, plan (intention) | Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů |
Investor: Ministry of Education, Youth and Sports of the CR, Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing |
PrintDisplayed: 6/10/2024 09:05