Parameterized verification through view abstraction

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F15%3APU122843" target="_blank" >RIV/00216305:26230/15:PU122843 - isvavai.cz</a>

Výsledek na webu

<a href="http://link.springer.com/article/10.1007%2Fs10009-015-0406-x" target="_blank" >http://link.springer.com/article/10.1007%2Fs10009-015-0406-x</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/s10009-015-0406-x" target="_blank" >10.1007/s10009-015-0406-x</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Parameterized verification through view abstraction

Popis výsledku v původním jazyce

We present a simple and efficient framework for automatic verification of systems with a parametric number of communicating processes. The processes may be organized in various topologies such as words, multisets, rings, or trees. Our method needs to inspect only a small number of processes in order to show correctness of the whole system. It relies on an abstraction function that views the system from the perspective of a fixed number of processes. The abstraction is used during the verification procedure in order to dynamically detect cut-off points beyond which the search of the state space need not continue. We show that the method is complete for a large class of well quasi-ordered systems including Petri nets. Our experimentation on a variety of benchmarks demonstrate that the method is highly efficient and that it works well even for classes of systems with undecidable verification problems. In particular, the method handles the fine-grained and full version of Szymanski's mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.

Název v anglickém jazyce

Parameterized verification through view abstraction

Popis výsledku anglicky

We present a simple and efficient framework for automatic verification of systems with a parametric number of communicating processes. The processes may be organized in various topologies such as words, multisets, rings, or trees. Our method needs to inspect only a small number of processes in order to show correctness of the whole system. It relies on an abstraction function that views the system from the perspective of a fixed number of processes. The abstraction is used during the verification procedure in order to dynamically detect cut-off points beyond which the search of the state space need not continue. We show that the method is complete for a large class of well quasi-ordered systems including Petri nets. Our experimentation on a variety of benchmarks demonstrate that the method is highly efficient and that it works well even for classes of systems with undecidable verification problems. In particular, the method handles the fine-grained and full version of Szymanski's mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GP13-37876P" target="_blank" >GP13-37876P: Verifikace nekonečně stavových systémů založená na konečných automatech</a><br>

Návaznosti

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

Rok uplatnění

2015

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 periodika

International Journal on Software Tools for Technology Transfer

ISSN

1433-2779

e-ISSN

1433-2787

Svazek periodika

2016

Číslo periodika v rámci svazku

5

Stát vydavatele periodika

DE - Spolková republika Německo

Počet stran výsledku

22

Strana od-do

495-516

Kód UT WoS článku

000382011100003

EID výsledku v databázi Scopus

2-s2.0-84947922862