Distributed Modular Model Checking (abstract)

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F02%3A00006592" target="_blank" >RIV/00216224:14330/02:00006592 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Distributed Modular Model Checking (abstract)

Popis výsledku v původním jazyce

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 partitionfunction 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ázev v anglickém jazyce

Distributed Modular Model Checking (abstract)

Popis výsledku anglicky

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 partitionfunction 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.

Druh

D - Stať ve sborníku

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

<a href="/cs/project/GA201%2F00%2F1023" target="_blank" >GA201/00/1023: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů</a><br>

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2002

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

The Seventeenth IEEE International Conference on Automated Software Engineering

ISBN

0-7695-1736-6

ISSN

—

e-ISSN

—

Počet stran výsledku

1

Strana od-do

312

Název nakladatele

IEEE Computer Society

Místo vydání

Los Alamitos

Místo konání akce

23 - 27 September 2002, Edinburgh, UK

Datum konání akce

1. 1. 2002

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—