D 2007

Scalable Multi-core LTL Model-Checking

BARNAT, Jiří, Luboš BRIM a Petr ROČKAI

Základní údaje

Originální název

Scalable Multi-core LTL Model-Checking

Název česky

Škálovatelné LTL ověřování modelu s využitím multi-core

Autoři

BARNAT, Jiří (203 Česká republika, garant), Luboš BRIM (203 Česká republika) a Petr ROČKAI (703 Slovensko)

Vydání

1. vyd. Berlin, Heidelberg, Model Checking Software, od s. 187-203, 17 s. 2007

Nakladatel

Springer-Verlag

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

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

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/07:00019427

Organizační jednotka

Fakulta informatiky

ISBN

978-3-540-73369-0

ISSN

UT WoS

000247906900013

Klíčová slova anglicky

Parallel LTL Model Checking; multi-core

Štítky

Příznaky

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

Anotace

ORIG CZ

V originále

Recent development in computer hardware has brought more wide-spread emergence of shared-memory, multi-core systems. These architectures offer opportunities to speed up various tasks; among others LTL model checking. In the paper we show a design for a parallel shared memory LTL model checker, that is based on a distributed memory algorithm. To achieve good scalability, we have devised and experimentally evaluated several implementation techniques, which we present in the paper.

Česky

Pokrok ve vývoji HW způsobil, že více jádrové systémy se sdílenou pamětí se staly běžně dostupné. Tyto architektury nabízejí jednotlivým aplikacím využít paralelismu a tak řešit úkoly v kratším čase. Jednou z možných aplikací je problém ověřování modelu s využitím LTL. V článku je popsáno několik obecných technik pro vývoj aplikací, které umožní aplikacím lépe využít možností paralelních architektur se sdílenou pamětí.

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