ProbDiVinE 2.0

Hlavní autoři: Jiří Appl, Jiří Barnat, Luboš Brim, Ivana Černá, Milan Češka, Jana Tůmová
Popis: Nástroj pro distribuovanou kvantitativní verifikaci vlastností lineárního času pravděpodobnostních modelů. V této verzi je podporován modelovací jazyk ProbDVE. Nástroj je postavený nad DiVinE 2.4.
Vlastník: Masarykova univerzita
Download: http://anna.fi.muni.cz/AS/probdivine-2.0.tar.gz
Licenční podmínky: GNU GPL
Rok: 2010
Projekty V/V: GAČR GA201/09/1389, Výzkumný záměr MSM0021622419

DiVinE 2.4

Hlavní autoři: Jiří Barnat, Luboš Brim, Petr Ročkai
Popis: Nástroj pro realizaci verifikace metodou ověřování modelu pro formule LTL (LTL Model Checking) v prostředí s distribuovanou pamětí s podporou redukce velikosti stavového prostoru metodou částečného uspořádání a s podporou ranné detekce chybného běhu. Nástroj je významným rozšířením předchozí verze verifikačního nástroje DiVinE 2.0.
Technické parametry: Nástroj je schopen efektivně využít cluster multi-core stanic. Verze 2.4.
Vlastník: Masarykova univerzita
Download: http://anna.fi.muni.cz/AS/divine-2.4.tar.gz
Licenční podmínky: GNU GPL
Rok: 2010
Projekty V/V: GAČR GA201/09/1389, Výzkumný záměr MSM0021622419, GAČR GP201/09/P497

CoIn-DiVinE

Hlavní autoři: Nikola Beneš, Ivana Černá, Milan Křivánek
Popis: CoIn-DiVinE je nástroj pro verifikaci interakcí v komponentovém systému, který je popsán pomocí formalismu automatů komponentové interakce (component-interaction automata). Nástroj je rozšířením verifikačního nástroje DiVinE 2.0 o nový vstupní jazyk CoIn a novou temporální logiku CI-LTL.
Vlastník: Masarykova univerzita
Download: http://anna.fi.muni.cz/AS/coin-divine-1.0.tar.gz
Licenční podmínky: GNU GPL
Rok: 2010
Projekty V/V: GAČR GA201/09/1389, GAČR GD102/09/H042

MWC-DiVinE

Hlavní autoři: Jiří Barnat, Luboš Brim, Petr Bauch, Milan Češka
Popis: MWC-DiVinE je nástroj pro kompoziční modelování a analýzu výkonu postavený na nástroji DiVinE pro ověřování modelu. MWC-DiVinE rozšiřuje jazyk DVE o možnost specifikovat spotřebu výpočetních zdrojů akcí systému a umožňuje analýzu výkonu s použitím algoritmů pro hledání optimální délky hrany v cyklech.
Vlastník: Masarykova univerzita
Download: http://anna.fi.muni.cz/AS/mwcdivine-1.0.tar.gz
Licenční podmínky: GNU GPL
Rok: 2010
Projekty V/V: GAČR GA201/09/1389, Výzkumný záměr MSM0021622419

DiVinE 2.0

Hlavní autoři: Jiří Barnat, Luboš Brim, Petr Ročkai, Milan Češka
Popis: Nová verze nástroje pro ověřování DVE modelů vůči lineárním vlastnostem zadaným pomocí Lineární temporální logiky. DiVinE 2.0 je sloučení a reimplementace předchozích verzí nástroje DiVinE, a to konkrétně DiVinE Cluster a DiVinE Multicore. Nástroj umožňuje pro verifikaci efektivně využít cluster vícejádrových stanic. Navíc oproti předchozím verzím nástroje přináší verze 2.0 následující vylepšení:
  • Grafické rozhraní simulátoru
  • Prototypové začlenění techniky POR
  • Win32 verze nástroje
  • Nový algoritmus verifikace umožňující on-the-fly verifikaci
Technické parametry: LTL model checker využívající cluster multi-core stanic. Verze DiVinE 2.0.
Vlastník: Masarykova univerzita
Download: http://www.fi.muni.cz/paradise/AS/divine-2.0.tar.gz
Licenční podmínky: GNU GPL
Rok: 2009
Projekty V/V: AVČR 1ET408050503, GAČR GA201/06/1338, Výzkumný záměr MSM0021622419, GAČR GP201/09/P497

DiVinE Cuda

Hlavní autoři: Jiří Barnat, Petr Bauch, Luboš Brim, Milan Češka, Tomáš Lamr
Popis: Nástroj pro ověřování DVE modelů vůči lineárním vlastnostem zadaným pomocí Lineární temporální logiky. Nástroj je specifický tím, že akceleruje svůj výpočet s použitím technologie CUDA od společnosti NVIDA.
Technické parametry: LTL model checker akcelerovaný grafickou kartou s podporou technologie CUDA. Verze 1.0. Vyžaduje instalovaný DiVinE Cluster.
Vlastník: Masarykova univerzita
Download: http://www.fi.muni.cz/paradise/AS/divine-cuda-1.0.tar.gz
Licenční podmínky: GNU GPL
Rok: 2009
Projekty V/V: AVČR 1ET408050503, GAČR GA201/06/1338, Výzkumný záměr MSM0021622419, GAČR GP201/09/P497

DiVinE Cluster

Hlavní autoři: Jiří Barnat, Luboš Brim, Ivana Černá, Pavel Šimeček, Milan češka
Popis: Nová generace nástroje DiVinE rozšiřující existující LTL Model Checker DiVinE. Významná rozšíření jsou zejména následující:
  • Částečná podpora modelovacího jazyka ProMeLa.
  • Rošíření škálovatelnosti a to na platformy o řádově větším počtu uzlů (stovky jader).
  • Akcelerace verifikačního procesu nahrazením interpretace modelů kompilovanou formou.
Technické parametry: LTL model checker využívající agregované výpočetní síly uzlů v klastru. Nástroj využívá rozhraní MPI. Verze 0.8.2.
Vlastník: Masarykova univerzita
Download: http://www.fi.muni.cz/paradise/AS/divine-cluster-0.8.2.tar.gz
Licenční podmínky: GNU GPL
Rok: 2008
Projekty V/V: AVČR 1ET408050503, GAČR GA201/06/1338, Výzkumný záměr MSM0021622419

ProbDiVinE-MC

Hlavní autoři: Jiří Barnat, Luboš Brim, Ivana Černá, Milan Češka, Jana Tůmová
Popis: Softvérový nástroj pro verifikaci kvantitativních aspektů pravděpodobnostních systémů pro paralelní hardvérové platformy se sdílenou pamětí. Systémy jsou specifikovány pomocí modelovacího jazyka ProbDVE. Vlastnosti specifikovány pomocí formulí lineární temporální logiky. Nástroj využívá volně dostupné softvérové produkty lpsolve a HOARD Library.
Technické parametry: Kvantitativní verifikace pravděpodobnostních systémů na platformách se sdílenou pamětí.
Vlastník: Masarykova univerzita
Download: http://www.fi.muni.cz/paradise/AS/probdivine-mc-1.2.tar.gz
Licenční podmínky: GNU GPL
Rok: 2008
Projekty V/V: AVČR 1ET408050503, GAČR GA201/06/1338, Výzkumný záměr MSM0021622419

ProbDiVinE

Hlavní autoři: Jiří Barnat, Luboš Brim, Ivana Černá, Milan Češka, Jana Tůmová
Popis: Softvérový nástroj pro verifikaci kvalitativních aspektů pravděpodobnostních systémů pro paralelní hardvérové platformy s distribuovanou pamětí. Systémy jsou specifikovány pomocí nově navrženého modelovacího jazyka ProbDVE. Vlastnosti specifikovány pomocí formulí lineární temporální logiky.
Technické parametry: Kvalitativní verifikace pravděpodobnostních systémů na platformách s distribuovanou pamětí, MPI/Linux, vyžaduje DiVinE Library.
Vlastník: Masarykova univerzita
Download: http://www.fi.muni.cz/paradise/AS/probdivine-1.1.tar.gz
Licenční podmínky: GNU GPL
Rok: 2007
Projekty V/V: AVČR 1ET408050503, GAČR GA201/06/1338, Výzkumný záměr MSM0021622419

DiVinE Multi-Core

Hlavní autoři: Jiří Barnat, Luboš Brim, Petr Ročkai
Popis: DiVinE Multi-Core je nástroj pro verifikaci LTL vlastností, který je schopný plně využít paralelní výkon soudobé více-jádrové architektury x86. Díky nově navrženým algoritmům a technické realizaci dosahuje tento nástroj škálovatelnosti na systémech s dvěmi až šestnácti jádry. Nástroj je plně funkční na 32 i 64 bitových platformách.

Technické parametry: LTL Model checker pro platformu více-jádrových stanic se sdílenou pamětí, vyžaduje Linux, verze 1.2.1.
Vlastník: Masarykova univerzita
Download: http://www.fi.muni.cz/paradise/AS/divine-mc-1.2.1.tar.gz
Licenční podmínky: GNU GPL
Rok: 2007
Projekty V/V: AVČR 1ET408050503, GAČR GA201/06/1338, Výzkumný záměr MSM0021622419

DiVinE Library

Hlavní autoři: Jiří Barnat, Luboš Brim, Ivana Černá, Pavel Moravec, Pavel Šimeček, Jakub Chaloupka
Popis: 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.

Technické parametry: Podpůrná knihovna pro tvorbu verifikačních nástrojů využívajících agregované výpočetní síly uzlů v klastru. Nástroj využívá rozhraní MPI. DiVinE Library verze 0.7.0.
Vlastník: Masarykova univerzita
Download: http://www.fi.muni.cz/paradise/AS/divine-0.7.0.tar.gz
Licenční podmínky: GNU GPL
Rok: 2006
Projekty V/V: AVČR 1ET408050503, GAČR GA201/06/1338, Výzkumný záměr MSM0021622419