BARNAT, Jiří, Vojtěch FOREJT, Martin LEUCKER a Michael WEBER. DivSPIN - A SPIN compatible distributed model checker. In Proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC05). Lisabon, Portugalsko: TU Munchen, 2005, s. 95-100.
Další formáty:   BibTeX LaTeX RIS
Zá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ří (203 Česká republika, garant), Vojtěch FOREJT (203 Česká republika), Martin LEUCKER (276 Německo) a Michael WEBER (276 Německo).
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
Originální 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 distributed, Model-Checking, parallel, SPIN
Změnil Změnil: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Změněno: 10. 1. 2006 12:19.
Anotace
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.
Anotace č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 VaVNázev: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů
VytisknoutZobrazeno: 3. 5. 2024 06:20