D 2002

Distributed Modular Model Checking (abstract)

CRHOVÁ, Jitka

Základní údaje

Originální název

Distributed Modular Model Checking (abstract)

Autoři

CRHOVÁ, Jitka (203 Česká republika, garant)

Vydání

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

Nakladatel

IEEE Computer Society

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

20206 Computer hardware and architecture

Stát vydavatele

Spojené státy

Utajení

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

Kód RIV

RIV/00216224:14330/02:00006592

Organizační jednotka

Fakulta informatiky

ISBN

0-7695-1736-6

Klíčová slova anglicky

formal methods; distributed model checking; modular model checking
Změněno: 14. 5. 2003 14:10, Mgr. Jitka Žídková

Anotace

V originále

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.

Návaznosti

GA201/00/1023, projekt VaV
Název: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů
Investor: Grantová agentura ČR, Algoritmy a nástroje pro praktickou verifikaci souběžných systémů
MSM 143300001, záměr
Název: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů