View Abstraction - A Tutorial

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F15%3APU117078" target="_blank" >RIV/00216305:26230/15:PU117078 - isvavai.cz</a>

Result on the web

<a href="http://dx.doi.org/10.4230/OASIcs.SynCoP.2015.1" target="_blank" >http://dx.doi.org/10.4230/OASIcs.SynCoP.2015.1</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.4230/OASIcs.SynCoP.2015.1" target="_blank" >10.4230/OASIcs.SynCoP.2015.1</a>

Result language

angličtina

Original language name

View Abstraction - A Tutorial

Original language description

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. 

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/GP13-37876P" target="_blank" >GP13-37876P: Verification of Infinite State Systems Based on Finite Automata</a><br>

Continuities

S - Specificky vyzkum na vysokych skolach

Publication year

2015

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

2nd International Workshop on Synthesis of Complex Parameters

ISBN

978-3-939897-82-8

ISSN

—

e-ISSN

—

Number of pages

15

Pages from-to

1-15

Publisher name

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

Place of publication

Dagstuhl

Event location

London

Event date

May 11, 2015

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—