Publication Details

Parameterized verification through view abstraction

ABDULLA Parosh A., HAZIZA Frédéric and HOLÍK Lukáš. Parameterized verification through view abstraction. International Journal on Software Tools for Technology Transfer, vol. 2016, no. 5, 2015, pp. 495-516. ISSN 1433-2779. Available from: http://link.springer.com/article/10.1007%2Fs10009-015-0406-x
Czech title
Parametrická verifikace pomocí pohledové abstrakce
Type
journal article
Language
english
Authors
Abdulla Parosh A. (Uppsala)
Haziza Frédéric (Uppsala)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
URL
Keywords

Parameterized systems
Safety
Small model properties
View abstraction

Abstract

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.

Published
2015
Pages
495-516
Journal
International Journal on Software Tools for Technology Transfer, vol. 2016, no. 5, ISSN 1433-2779
Publisher
Springer Verlag
DOI
UT WoS
000382011100003
EID Scopus
BibTeX
@ARTICLE{FITPUB11340,
   author = "A. Parosh Abdulla and Fr\'{e}d\'{e}ric Haziza and Luk\'{a}\v{s} Hol\'{i}k",
   title = "Parameterized verification through view abstraction",
   pages = "495--516",
   journal = "International Journal on Software Tools for Technology Transfer",
   volume = 2016,
   number = 5,
   year = 2015,
   ISSN = "1433-2779",
   doi = "10.1007/s10009-015-0406-x",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11340"
}
Back to top