D 2008

ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems

BARNAT, Jiří; Luboš BRIM; Ivana ČERNÁ; Milan ČEŠKA; Jana TŮMOVÁ et. al.

Základní údaje

Originální název

ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems

Název česky

ProbDiVinE-MC: Ověřování modelu LTL pravděpodobnostních systémů na vícejádrových strojích

Vydání

Washington, DC, USA, QEST '08: Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems, od s. 77-78, 2 s. 2008

Nakladatel

IEEE Computer Society

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Francie

Utajení

není předmětem státního či obchodního tajemství

Kód RIV

RIV/00216224:14330/08:00024323

Organizační jednotka

Fakulta informatiky

ISBN

978-0-7695-3360-5

UT WoS

000260248700010

Klíčová slova anglicky

LTL Model Checking; Multi-core CPU; Probabilistic systems

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 1. 6. 2009 21:02, prof. RNDr. Jiří Barnat, Ph.D.

Anotace

V originále

We present a new version of \probdivine\ -- a parallel tool for verification of probabilistic systems against properties formulated in linear temporal logic. Unlike the previous release, the new version of the tool allows for both quantitative and qualitative model-checking. It is also strictly multi-threaded, therefore, protects users from unwanted burden of parallel computing in a distributed-memory environment.

Česky

Je představena nová verze nástroje probdivine, který umožňuje verifikovat pravděpodobnostní systémy na vlastnosti specifokované pomocí LTL. Narozdíl od předchozí verze, nástroj umožňuje provádět kvalitativní i kvantitativní verifikaci pravděpodobnostních systémů a to na systémech osazených vícejadernými procesory.

Návaznosti

GA201/06/1338, projekt VaV
Název: Automatizovaná verifikace softwaru
Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru
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ů
1M0545, projekt VaV
Název: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky