DiVinE Library

BARNAT, Jiří; Luboš BRIM; Ivana ČERNÁ; Pavel MORAVEC; Pavel ŠIMEČEK a Jakub CHALOUPKA. DiVinE Library. 2006.

Základní údaje

Originální název

DiVinE Library

Název česky

Knihovna DiVinE

Autoři

BARNAT, Jiří; Luboš BRIM; Ivana ČERNÁ ORCID; Pavel MORAVEC; Pavel ŠIMEČEK a Jakub CHALOUPKA

Vydání

2006

---

Další údaje

Jazyk

angličtina

Typ výsledku

Software

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

URL

Kód RIV

RIV/00216224:14330/06:00024474

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

parallel verification; LTL model-checking

Technické parametry

L model checker využívající agregované výpočetní síly uzlů v klastru. Nástroj využívá rozhraní MPI. Verze 0.7.0.

Štítky

LTL model-checking, parallel verification

Příznaky

Mezinárodní význam

---

Anotace

V originále

A library designed to support fast implementation of LTL Model Checkers that employ aggregate computational power of many network nodes to complete the verification task. Several prototype LTL model checking tools are part of the library. Models to be verified must be given in newly designed modeling language DVE.

Česky

Knihovna určená pro výstavbu LTL Model Checkerů využívajících k verifikaci agregovaných výpočetních prostředků mnoha výpočetních uzlů v jednom clusteru. Knihovna podporuje implementuci nově navržených paralelních algoritmů pro detekci akceptujících cyklů v grafu. Součástí knihovny je implementace prototypových nástrojů pro již navržené algoritmy, které umožňují použití celého prostředí bez nutnosti instalace dalšího software. Verifikované modely musí být zadány v nově navrženém modelovacím jazyce DVE.

---

Návaznosti

GA201/06/1338, projekt VaV	Název: Automatizovaná verifikace softwaru Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru
MSM0021622419, záměr	Název: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1ET408050503, projekt VaV	Ná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ů