BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties. Science of Computer Programming, Elsevier, 2012, roč. 77, č. 12, s. 1272-1288. ISSN 0167-6423. doi:10.1016/j.scico.2011.03.001.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties
Autoři BARNAT, Jiří (703 Slovensko, garant, domácí), Luboš BRIM (203 Česká republika, domácí) a Petr ROČKAI (703 Slovensko, domácí).
Vydání Science of Computer Programming, Elsevier, 2012, 0167-6423.
Další údaje
Originální jazyk angličtina
Typ výsledku Článek v odborném periodiku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Spojené státy americké
Utajení není předmětem státního či obchodního tajemství
WWW URL
Impakt faktor Impact factor: 0.568
Kód RIV RIV/00216224:14330/12:00057076
Organizační jednotka Fakulta informatiky
Doi http://dx.doi.org/10.1016/j.scico.2011.03.001
UT WoS 000308732800004
Klíčová slova anglicky Explicit Model Checking; Parallel; On-the-fly; Partial Order Reduction
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 23. 4. 2013 11:37.
Anotace
One of the most important open problems of parallel LTL model checking is to design an on-the-fly scalable parallel algorithm with linear time complexity. Such an algorithm would provide the same optimality we have in sequential LTL model checking. In this paper we give a partial solution to the problem: we propose an algorithm that has the required properties for a very rich subset of LTL properties, namely those expressible by weak Buchi automata. In addition to the previous version of the paper, we demonstrate how our new algorithm can be efficiently combined with a particular parallel technique for Partial Order Reduction and report on additional experiments.
Návaznosti
GA201/09/1389, projekt VaVNázev: Verifikace a analýza velmi velkých počítačových systémů
Investor: Grantová agentura ČR, Standardní projekty
GP201/09/P497, projekt VaVNázev: Automatizovaná formální verifikace s využitím soudobého hardware
Investor: Grantová agentura ČR, Postdoktorské projekty
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
MUNI/A/0057/2011, interní kód MUNázev: Posílení zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKONF)
Investor: Masarykova univerzita, Grantová agentura MU, Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0914/2009, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV)
Investor: Masarykova univerzita, Grantová agentura MU, Kategorie A - Specifický výzkum - Studentské výzkumné projekty
1ET400300504, projekt VaVNázev: Realistická aplikace formálních metod v komponentových systémech
Investor: Akademie věd ČR, Informační společnost (Národní program výzkumu)
1ET408050503, projekt VaVNázev: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Informační společnost (Národní program výzkumu)
VytisknoutZobrazeno: 26. 1. 2020 18:37