Detailed Information on Publication Record
2005
DivSPIN - A SPIN compatible distributed model checker
BARNAT, Jiří, Vojtěch FOREJT, Martin LEUCKER and Michael WEBERBasic information
Original name
DivSPIN - A SPIN compatible distributed model checker
Name in Czech
DivSPIN - distribuovaný model checker kompatibilní se SPINem
Authors
BARNAT, Jiří (203 Czech Republic, guarantor), Vojtěch FOREJT (203 Czech Republic), Martin LEUCKER (276 Germany) and Michael WEBER (276 Germany)
Edition
Lisabon, Portugalsko, Proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC05), p. 95-100, 6 pp. 2005
Publisher
TU Munchen
Other information
Language
English
Type of outcome
Stať ve sborníku
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
Czech Republic
Confidentiality degree
není předmětem státního či obchodního tajemství
RIV identification code
RIV/00216224:14330/05:00013423
Organization unit
Faculty of Informatics
Keywords in English
distributed; parallel; model-checking; SPIN
Tags
Změněno: 10/1/2006 12:19, prof. RNDr. Jiří Barnat, Ph.D.
V originále
This paper describes the design and implementation ideas of an extension of the parallel and distributed model checker DiVinE to a SPIN compatible distributed model checker \Toolname. The goal of DivSPIN is to serve as user-friendly, ready-to-use system that takes up the recent theoretical and practical developments in the area of distributed model checkers and combines them with well settled operational procedures of sequential model checkers to show the benefits of parallel model checking for typical verification tasks. For this project, the research teams located at Masaryk University in Brno, Czech Republic, RWTH Aachen University, and TU Munich, Germany join their efforts.
In Czech
Tento článek popisuje návrh a myšlenky implementace, které rozšiřují paralelní a distribuovaný model checker DiVinE na distribuovaný model checker DivSPIN kompatibilní se SPINem. Cílem DivSPINu je sloužit jako uživatelsky přítulný a dostupný systém pro ověřování modelů, který využívá nejnovější teoretické a praktické poznatky z oblasti distribuovaného ověřování modelu. Tyto poznatky jsou v rámci prototypu DivSPIN kombinovány s postupy používanými při práci se sekvenčními model checkery, což umožňuje ukázat mnohé výhody paralelního a distribuovaného ověřování modelu při verifikaci typických úkolů. V tomto projektu spojily své síly výzkumné týmy z Masarykovy Univerzity v Brně, RWTH Univerzity v Aachenu a TU v Mnichově.
Links
| 1ET408050503, research and development project |
|