Faculty of Information Technology, BUT

Publication Details

View Abstraction - A Tutorial

ABDULLA Parosh A., HAZIZA Frédéric and HOLÍK Lukáš. View Abstraction - A Tutorial. In: 2nd International Workshop on Synthesis of Complex Parameters. Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2015, pp. 1-15. ISBN 978-3-939897-82-8.
Czech title
Pohledová abstrakce - Tutoriál
Type
conference paper
Language
english
Authors
Abdulla Parosh A. (Uppsala)
Haziza Frédéric (Uppsala)
Holík Lukáš, Mgr., Ph.D. (DITS FIT BUT)
Keywords
parallelism
parameterised systems
view abstraction
verification
well structured transition systems
Abstract

We consider parameterized verification, i.e., proving correctness of a system with an unbounded number of processes. We describe the method of view abstraction whose aim is to provide a small model property, i.e., showing correctness by only inspecting instances of the system consisting of a small fixed number of processes. We illustrate the method through an application to the classical Burns mutual exclusion protocol. 

Annotation

We consider parameterized verification, i.e., proving correctness of a system with an unbounded number of processes. We describe the method of view abstraction whose aim is to provide a small model property, i.e., showing correctness by only inspecting instances of the system consisting of a small fixed number of processes. We illustrate the method through an application to the classical Burns mutual exclusion protocol. 

Published
2015
Pages
1-15
Proceedings
2nd International Workshop on Synthesis of Complex Parameters
Conference
2nd International Workshop on Synthesis of Complex Parameters , London, GB
ISBN
978-3-939897-82-8
Publisher
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Place
Dagstuhl, DE
DOI
BibTeX
@INPROCEEDINGS{FITPUB11059,
   author = "A. Parosh Abdulla and Fr\'{e}d\'{e}ric Haziza and Luk\'{a}\v{s} Hol\'{i}k",
   title = "View Abstraction - A Tutorial",
   pages = "1--15",
   booktitle = "2nd International Workshop on Synthesis of Complex Parameters",
   year = 2015,
   location = "Dagstuhl, DE",
   publisher = "Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
   ISBN = "978-3-939897-82-8",
   doi = "10.4230/OASIcs.SynCoP.2015.1",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11059"
}
Back to top