Distributed breadth-first search LTL model checking

BARNAT, Jiří and Ivana ČERNÁ. Distributed breadth-first search LTL model checking. Formal Methods in System Design. Springer Netherlands, 2006, vol. 29, No 2, p. 117-134. ISSN 0925-9856.

Basic information

Original name

Distributed breadth-first search LTL model checking

Name in Czech

Distribuované ověřování modelu LTL s využitím prohledávání grafu do šířky

Authors

BARNAT, Jiří (203 Czech Republic, guarantor) and Ivana ČERNÁ (203 Czech Republic)

Edition

Formal Methods in System Design, Springer Netherlands, 2006, 0925-9856

---

Other information

Language

English

Type of outcome

Článek v odborném periodiku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Netherlands

Confidentiality degree

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

References:

URL

Impact factor

Impact factor: 0.900

RIV identification code

RIV/00216224:14330/06:00015452

Organization unit

Faculty of Informatics

UT WoS

000241173800002

Keywords in English

LTL model checking; Distributed memory; Breadth-first Search

Tags

Breadth-first Search, distributed memory, LTL model checking

Tags

International impact, Reviewed

---

Abstract

V originále

We propose a parallel distributed memory on-the-fly algorithm for enumerative LTL model checking. The algorithm is designed for networks of workstations communicating via MPI. The detection of cycles (faulty runs) effectively employs the so-called back-level edges. In particular, a parallel level synchronized breadth-first search of the graph is performed to discover all back-level edges, and for each level the back-level edges are checked in parallel by a nested search procedure to confirm or refute the presence of a cycle. Several improvements of the basic algorithm are presented and advantages and drawbacks of their application to distributed LTL model checking are discussed.

In Czech

Je zde navrhnut a experimentalně vyhodnocen algoritmus pro detekci akceptujicích cyklů v grafu, založený na tzv. back-level hranách. Algoritmus je dále rozšířen o několik nezbytných módů, které jsou nezbytné pro vytvoření skutečného verifikačního nástroje pro LTL ověřování modelů. Tento nástroj byl implementován a experimentálně vyhodnocen na několika směrodatných vstupech.

---

Links

GA201/06/1338, research and development project	Name: Automatizovaná verifikace softwaru Investor: Czech Science Foundation, Automated software verification
GD102/05/H050, research and development project	Name: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů Investor: Czech Science Foundation, Integrated approach to education of PhD students in the area of parallel and distributed systems
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
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