2005
DivSPIN - A SPIN compatible distributed model checker
BARNAT, Jiří; Vojtěch FOREJT; Martin LEUCKER a Michael WEBERZákladní údaje
Originální název
DivSPIN - A SPIN compatible distributed model checker
Název česky
DivSPIN - distribuovaný model checker kompatibilní se SPINem
Autoři
BARNAT, Jiří; Vojtěch FOREJT; Martin LEUCKER a Michael WEBER
Vydání
Lisabon, Portugalsko, Proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC05), od s. 95-100, 6 s. 2005
Nakladatel
TU Munchen
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Česká republika
Utajení
není předmětem státního či obchodního tajemství
Kód RIV
RIV/00216224:14330/05:00013423
Organizační jednotka
Fakulta informatiky
Klíčová slova anglicky
distributed; parallel; model-checking; SPIN
Štítky
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.
Česky
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ě.
Návaznosti
| 1ET408050503, projekt VaV |
|