| BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Pavel MORAVEC, Pavel ŠIMEČEK a Jakub CHALOUPKA. DiVinE Library. 2006. |
|
Další formáty:
BibTeX
LaTeX
RIS
|
| Základní údaje | |
|---|---|
| Originální název | DiVinE Library |
| Název česky | Knihovna DiVinE |
| Autoři | BARNAT, Jiří (203 Česká republika), Luboš BRIM (203 Česká republika, garant), Ivana ČERNÁ (203 Česká republika), Pavel MORAVEC (203 Česká republika), Pavel ŠIMEČEK (203 Česká republika) a Jakub CHALOUPKA (203 Česká republika). |
| Vydání | 2006. |
| Další údaje | |
|---|---|
| Originální 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í |
| WWW | 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 |
| Změnil | Změnil: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Změněno: 2. 6. 2009 11:35. |
| Anotace |
|---|
| 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. |
| Anotace č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ů | |
VytisknoutZobrazeno: 26. 4. 2024 07:33