View Abstraction - A Tutorial

Czech title

Pohledová abstrakce - Tutoriál

Type

conference paper

Language

english

Authors

Abdulla Parosh A. (Uppsala)
Haziza Frédéric (Uppsala)
Holík Lukáš, doc. 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

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 , London, GB

ISBN

978-3-939897-82-8

Publisher

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

Place

Dagstuhl, DE

DOI

10.4230/OASIcs.SynCoP.2015.1

EID Scopus

2-s2.0-85092799549

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",
   series = "OpenAccess Series in Informatics",
   journal = "OpenAccess Series in Informatics (OASIcs)",
   volume = 44,
   number = 1,
   year = 2015,
   location = "Dagstuhl, DE",
   publisher = "Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
   ISBN = "978-3-939897-82-8",
   ISSN = "2190-6807",
   doi = "10.4230/OASIcs.SynCoP.2015.1",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11059"
}