D 2002

Distributed Modular Model Checking (abstract)

CRHOVÁ, Jitka

Basic information

Original name

Distributed Modular Model Checking (abstract)

Authors

CRHOVÁ, Jitka (203 Czech Republic, guarantor)

Edition

Los Alamitos, The Seventeenth IEEE International Conference on Automated Software Engineering, p. 312-312, 2002

Publisher

IEEE Computer Society

Other information

Language

English

Type of outcome

Proceedings paper

Field of Study

20206 Computer hardware and architecture

Country of publisher

United States of America

Confidentiality degree

is not subject to a state or trade secret

RIV identification code

RIV/00216224:14330/02:00006592

Organization unit

Faculty of Informatics

ISBN

0-7695-1736-6

Keywords in English

formal methods; distributed model checking; modular model checking
Changed: 14/5/2003 14:10, Mgr. Jitka Žídková

Abstract

In the original language

A distributed model checking algorithm is presented. It is designed to be run on a network of workstations that communicate via message passing. The algorithm handles large state spaces by partitioning them into smaller units. Such a partition of state space into partial state spaces can be employed to perform several smaller verification problems independently on several computers increasing thus not only speeding up the verification, but most importantly the available memory. We also suggest partition function that can be used as input to the ditributed algorithm. For software systems a quite successful approach is to partition them following the syntactical structure of the program. Other state based temporal logics and various model checking algorithms can be adapted easily as well.

Links

GA201/00/1023, research and development project
Name: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů
Investor: Czech Science Foundation, Algorithms and tools for practical verification of concurrent systems.
MSM 143300001, plan (intention)
Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministry of Education, Youth and Sports of the CR, Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing