Přístupnostní navigace
E-application
Search Search Close
Publication detail
HOLÍK, L. ABDULLA, P. HAZIZA, F.
Original Title
All for the Price of Few (Parameterized Verification through View Abstraction)
Type
article in a collection out of WoS and Scopus
Language
English
Original Abstract
We present a simple and efficient framework for automatic verification of systems with parameteric number of communicating processes. The processes may be organized in various topologies such 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 subclass 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 problem.
Keywords
parameterized verification, communication protocols, well-quasi ordered systems, abstraction, cutoff
Authors
HOLÍK, L.; ABDULLA, P.; HAZIZA, F.
RIV year
2013
Released
21. 1. 2013
Publisher
Springer Verlag
Location
Berlin Heidelberg
ISBN
978-3-642-35872-2
Book
Proc. of VMCAI 2013
0302-9743
Periodical
Lecture Notes in Computer Science
Year of study
Number
7737
State
Federal Republic of Germany
Pages from
476
Pages to
495
Pages count
20
BibTex
@inproceedings{BUT103433, author="Lukáš {Holík} and Parosh {Abdulla} and Frédéric {Haziza}", title="All for the Price of Few (Parameterized Verification through View Abstraction)", booktitle="Proc. of VMCAI 2013", year="2013", journal="Lecture Notes in Computer Science", volume="2013", number="7737", pages="476--495", publisher="Springer Verlag", address="Berlin Heidelberg", isbn="978-3-642-35872-2", issn="0302-9743" }