Partial Order Reduction in Model Checking of Object-Oriented Petri Nets

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F03%3APU42511" target="_blank" >RIV/00216305:26230/03:PU42511 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Partial Order Reduction in Model Checking of Object-Oriented Petri Nets

Popis výsledku v původním jazyce

In this paper, we discuss some on-the-fly methods for model checking over OOPNs, i.e. methods in which generation of state spaces is done simultaneously with (and is guided by) checking the appropriate property. A big challenge in finite-state model checking is the state space explosion problem, i.e. the exponential growth of state spaces. Fortunately, there have been proposed many advanced methods for reducing state spaces. One of the most successful methods (especially when dealing with software systeems) is the so-called partial-order reduction. We examine how this method can be used in the context of OOPNs, which bring in features like dynamic instantiation, late binding, garbage collection, etc.

Název v anglickém jazyce

Partial Order Reduction in Model Checking of Object-Oriented Petri Nets

Popis výsledku anglicky

In this paper, we discuss some on-the-fly methods for model checking over OOPNs, i.e. methods in which generation of state spaces is done simultaneously with (and is guided by) checking the appropriate property. A big challenge in finite-state model checking is the state space explosion problem, i.e. the exponential growth of state spaces. Fortunately, there have been proposed many advanced methods for reducing state spaces. One of the most successful methods (especially when dealing with software systeems) is the so-called partial-order reduction. We examine how this method can be used in the context of OOPNs, which bring in features like dynamic instantiation, late binding, garbage collection, etc.

Druh

D - Stať ve sborníku

CEP obor

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

OECD FORD obor

—

Projekt

<a href="/cs/project/GA102%2F00%2F1017" target="_blank" >GA102/00/1017: Modelování, verifikace a prototypování distribuovaných aplikací s využitím Petriho sítí</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2003

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

Cast and Complexity in Biological, Physical and Engineering Systems, Extended Abstracts, Eurocast 2003

ISBN

84-688-0820-2

ISSN

—

e-ISSN

—

Počet stran výsledku

3

Strana od-do

254-256

Název nakladatele

University of Las Palmas

Místo vydání

Las Palmas de Gran Canaria, Canary Islands

Místo konání akce

Las Palmas de Gran Canaria, Canary Islands, Spai

Datum konání akce

24. 2. 2003

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

WRD - Celosvětová akce

Kód UT WoS článku

—