Result Details

View Abstraction - A Tutorial

HOLÍK, L.; HAZIZA, F.; ABDULLA, P. View Abstraction - A Tutorial. In 2nd International Workshop on Synthesis of Complex Parameters. OpenAccess Series in Informatics (OASIcs). OpenAccess Series in Informatics. Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2015. no. 1, p. 1-15. ISBN: 978-3-939897-82-8. ISSN: 2190-6807.
Type
conference paper
Language
English
Authors
Holík Lukáš, doc. Mgr., Ph.D., DITS (FIT)
Haziza Frédéric
Abdulla Parosh
Abstract

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

Keywords

parallelism
parameterised systems
view abstraction
verification
well structured transition systems

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
Journal
OpenAccess Series in Informatics (OASIcs), vol. 44, no. 1, ISSN 2190-6807
Proceedings
2nd International Workshop on Synthesis of Complex Parameters
Series
OpenAccess Series in Informatics
Conference
2nd International Workshop on Synthesis of Complex Parameters
ISBN
978-3-939897-82-8
Publisher
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Place
Dagstuhl
DOI
10.4230/OASIcs.SynCoP.2015.1
EID Scopus
2-s2.0-85092799549
BibTeX 
@inproceedings{BUT119935,
  author="Lukáš {Holík} and Frédéric {Haziza} and Parosh {Abdulla}",
  title="View Abstraction - A Tutorial",
  booktitle="2nd International Workshop on Synthesis of Complex Parameters",
  year="2015",
  series="OpenAccess Series in Informatics",
  journal="OpenAccess Series in Informatics (OASIcs)",
  volume="44",
  number="1",
  pages="1--15",
  publisher="Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
  address="Dagstuhl",
  doi="10.4230/OASIcs.SynCoP.2015.1",
  isbn="978-3-939897-82-8",
  issn="2190-6807"
}
Projects
Spolehlivost a bezpečnost v IT, BUT, Vnitřní projekty VUT, FIT-S-14-2486, start: 2014-01-01, end: 2016-12-31, completed
Verification of Infinite State Systems Based on Finite Automata, GACR, Postdoktorandské granty, GP13-37876P, start: 2013-02-01, end: 2015-12-31, completed
Departments
Department of Intelligent Systems (DITS)
Back to top