Enhancing Random Walk State Space Exploration

PELÁNEK, Radek, Tomáš HANŽL, Ivana ČERNÁ a Luboš BRIM. Enhancing Random Walk State Space Exploration. In Formal Methods for Industrial Critical Systems. Lisbon: ACM SIGSOFT, 2005, s. 98-105. ISBN 1-59593-148-1.

Základní údaje

• Originální název: Enhancing Random Walk State Space Exploration
• Název česky: Zlepšení prohledávání stavového prostoru náhodnou procházkou
• Autoři: PELÁNEK, Radek (203 Česká republika, garant), Tomáš HANŽL (203 Česká republika), Ivana ČERNÁ (203 Česká republika) a Luboš BRIM (203 Česká republika).
• Vydání: Lisbon, Formal Methods for Industrial Critical Systems, od s. 98-105, 8 s. 2005.
• Nakladatel: ACM SIGSOFT

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Stať ve sborníku
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Portugalsko
• Utajení: není předmětem státního či obchodního tajemství
• Kód RIV: RIV/00216224:14330/05:00012727
• Organizační jednotka: Fakulta informatiky
• ISBN: 1-59593-148-1
• Klíčová slova anglicky: random walk; state space exploration
• Štítky: random walk, state space exploration
• Příznaky: Recenzováno

Anotace

We study the behavior of the random walk method in the context of model checking and its capacity to explore a state space. We describe the methodology we have used for observing the random walk and report on the results obtained. We also describe many possible enhancements of the random walk and study their behavior and limits. Finally, we discuss some practically important but often neglected issues like counterexamples, coverage estimation, and setting of parameters. Similar methodology can be used for studying other state space exploration techniques like bit-state hashing, partial storage methods, or partial order reduction.

Anotace česky

Studujeme chování metody náhodné procházky v kontextu metody ověřování modelů a prohledávání stavového prostoru. Popisujeme metodologii, kterou jsme použili pro pozorování náhodných procházek na velkých grafech a kterou používáme pro shrnutí výsledků. Popisujeme také několik různých zlepšení náhodné procházky a studujeme jejich vlastnosti a limity. Na závěr diskutujeme několik důležitých, ale často opomíjených, témat, jako protipříklady, odhad pokrytí a nastavení parametrů. Podobná metodologie může být použita pro studium dalším metod prohledávání stavového prostoru jako například hašování stavů pomocí bitů, metody částečného ukládání, redukce částečných uspořádání.

Návaznosti

• GA201/03/0509, projekt VaV: Název: Automatizovaná verifikace paralelních a distribuovaných systémů

Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů

• GD102/05/H050, projekt VaV: Název: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů

Investor: Grantová agentura ČR, Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů

• 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ů