Streaming state space: a method of distributed model verification

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F07%3A10084052" target="_blank" >RIV/00216208:11320/07:10084052 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Streaming state space: a method of distributed model verification

Popis výsledku v původním jazyce

We present an alternative to traditional approaches of parallel and distributed model verification. In contrast to methods based on partitioning the state space, we keep the states together, sorted and organized as a stream. The stream is passed across computational nodes in a logical circle where each node updates the states in the part of the stream it currently sees. The presented method relies on state locality, allows storing the state space at external storage devices, and scales well on a non-dedicated, non-uniform cluster of up to tens of nodes. We have implemented an experimental version of the algorithm and obtained very promising results in scalability in the number of processors and computational nodes used in a large real-life use case.

Název v anglickém jazyce

Streaming state space: a method of distributed model verification

Popis výsledku anglicky

We present an alternative to traditional approaches of parallel and distributed model verification. In contrast to methods based on partitioning the state space, we keep the states together, sorted and organized as a stream. The stream is passed across computational nodes in a logical circle where each node updates the states in the part of the stream it currently sees. The presented method relies on state locality, allows storing the state space at external storage devices, and scales well on a non-dedicated, non-uniform cluster of up to tens of nodes. We have implemented an experimental version of the algorithm and obtained very promising results in scalability in the number of processors and computational nodes used in a large real-life use case.

Druh

D - Stať ve sborníku

CEP obor

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

OECD FORD obor

—

Projekt

<a href="/cs/project/GA201%2F06%2F0770" target="_blank" >GA201/06/0770: Formální metody prakticky použitelné pro vývoj systémů složených ze softwarových komponent</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2007

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

First IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering

ISBN

978-0-7695-2856-4

ISSN

—

e-ISSN

—

Počet stran výsledku

10

Strana od-do

—

Název nakladatele

IEEE Computer Society Press

Místo vydání

Neuveden

Místo konání akce

Shanghai, China

Datum konání akce

6. 6. 2007

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

WRD - Celosvětová akce

Kód UT WoS článku

000247666400034