Scalable shared memory LTL model checking

BARNAT, Jiří; Luboš BRIM and Petr ROČKAI. Scalable shared memory LTL model checking. International Journal on Software Tools for Technology Transfer (STTT). Springer-Verlag GmbH, 2010, vol. 12, No 2, p. 139-153. ISSN 1433-2779. Available from: https://doi.org/10.1007/s10009-010-0136-z.

Basic information

Original name

Scalable shared memory LTL model checking

Authors

BARNAT, Jiří (203 Czech Republic, guarantor, belonging to the institution); Luboš BRIM (203 Czech Republic, belonging to the institution) and Petr ROČKAI (703 Slovakia, belonging to the institution)

Edition

International Journal on Software Tools for Technology Transfer (STTT), Springer-Verlag GmbH, 2010, 1433-2779

---

Other information

Language

English

Type of outcome

Article in a journal

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

is not subject to a state or trade secret

References:

URL

RIV identification code

RIV/00216224:14330/10:00065778

Organization unit

Faculty of Informatics

DOI

https://doi.org/10.1007/s10009-010-0136-z

Keywords in English

LTL Model Cecking; Parallel; Shared-Memory

Tags

International impact, Reviewed

---

Abstract

In the original language

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 - model checking and reachability analysis among others. In this paper, we present a design for a parallel shared memory LTL model checker that is based on a distributed memory algorithm. To improve the scalability of our tool, we have devised a number of implementation techniques which we present in this paper. We also report on a number of experi- ments we conoducted to analyze the behaviour of our tool under different conditions using various models. We demonstrate that our tool exhibits significant speedup in comparison to sequential tools, which improves the workflow of verification in general.

In Czech

Nedávný vývoj v oblasti počítačového HW vedl k masovému rozšíření vícekórových výpočetních systémů. Tyto systémy umožňují akceleraci různých úloh paralelizací. V článku je popsán návrh paralelního nástroje pro LTL ověřování modelu. Paralelní škálovatelnost nástroje je umocněna nově navrhnutými implementačními technikami. Nástroj byl pro účely článku experimentálně evaluován na několika modelech, zpráva o této evaluaci je součástí článku. Nástroj vykazuje vzhledem k své sekvenční verzi významné zrychlení procesu verifikace.

---

Links

GA201/09/1389, research and development project	Name: Verifikace a analýza velmi velkých počítačových systémů Investor: Czech Science Foundation, Verification and Analysis of Large-Scale Computer Systems
GP201/09/P497, research and development project	Name: Automatizovaná formální verifikace s využitím soudobého hardware Investor: Czech Science Foundation, Automated formal verification using modern hardware
MSM0021622419, plan (intention)	Name: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
MUNI/A/0914/2009, interní kód MU	Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Acronym: SV-FI MAV) Investor: Masaryk University, Category A
1ET408050503, research and development project	Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems
1M0545, research and development project	Name: Institut Teoretické Informatiky Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science