Parameterized verification through view abstraction
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Parameterized verification through view abstraction
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
J<sub>imp</sub> - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GP13-37876P" target="_blank" >GP13-37876P: Verification of Infinite State Systems Based on Finite Automata</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2015
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
International Journal on Software Tools for Technology Transfer
ISSN
1433-2779
e-ISSN
1433-2787
Volume of the periodical
2016
Issue of the periodical within the volume
5
Country of publishing house
DE - GERMANY
Number of pages
22
Pages from-to
495-516
UT code for WoS article
000382011100003
EID of the result in the Scopus database
2-s2.0-84947922862