Publication Details
View Abstraction - A Tutorial
parallelism parameterised systems view abstraction verification well structured transition systems
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.
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.
@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"
}