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://dx.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

• Original 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
• WWW: URL
• RIV identification code: RIV/00216224:14330/10:00065778
• Organization unit: Faculty of Informatics
• Doi: http://dx.doi.org/10.1007/s10009-010-0136-z
• Keywords in English: LTL Model Cecking; Parallel; Shared-Memory
• Tags: International impact, Reviewed

Abstract

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.

Abstract (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